MyWikiBiz, Author Your Legacy — Sunday November 24, 2024
Jump to navigationJump to search
721 bytes removed
, 14:58, 12 September 2010
| Line 6: |
Line 6: |
| | | | |
| | =====1.3.12.1. Syntactic Transformation Rules===== | | =====1.3.12.1. Syntactic Transformation Rules===== |
| − |
| |
| − | ======Value Rules======
| |
| | | | |
| | <pre> | | <pre> |
| Line 145: |
Line 143: |
| | | | |
| | E1d. (( f , g ))$(u). :$1b | | E1d. (( f , g ))$(u). :$1b |
| − | </pre>
| |
| − |
| |
| − | ======Facts======
| |
| − |
| |
| − | Applying Rule 9, Rule 8, and the Logical Rules to the special case where S <=> (X = Y), one obtains the following general fact.
| |
| − |
| |
| − | <pre>
| |
| − | Fact 1
| |
| − |
| |
| − | If X,Y c U,
| |
| − |
| |
| − | then the following are equivalent:
| |
| − |
| |
| − | F1a. S <=> X = Y. :R9a
| |
| − |
| |
| − | ::
| |
| − |
| |
| − | F1b. S <=> {X} = {Y}. :R9b
| |
| − |
| |
| − | ::
| |
| − |
| |
| − | F1c. S <=> {X}(u) = {Y}(u), for all u C U. :R9c
| |
| − |
| |
| − | ::
| |
| − |
| |
| − | F1d. S <=> ConjUu ( {X}(u) = {Y}(u) ). :R9d
| |
| − |
| |
| − | :R8a
| |
| − |
| |
| − | ::
| |
| − |
| |
| − | F1e. [S] = [ ConjUu ( {X}(u) = {Y}(u) ) ]. :R8b
| |
| − |
| |
| − | :???
| |
| − |
| |
| − | ::
| |
| − |
| |
| − | F1f. [S] = ConjUu [ {X}(u) = {Y}(u) ]. :???
| |
| − |
| |
| − | ::
| |
| − |
| |
| − | F1g. [S] = ConjUu (( {X}(u) , {Y}(u) )). :$1a
| |
| − |
| |
| − | ::
| |
| − |
| |
| − | F1h. [S] = ConjUu (( {X} , {Y} ))$(u). :$1b
| |
| − |
| |
| − | ///
| |
| − |
| |
| − | {u C U : (f, g)$(u)}
| |
| − |
| |
| − | = {u C U : (f(u), g(u))}
| |
| − |
| |
| − | = {u C
| |
| − |
| |
| − | ///
| |
| | </pre> | | </pre> |
| | | | |
