({ Home Grammar Facts Reasoning Knowledge base Software Download })

({ Clicking on a green or brown colored Method displays or hides the Application of that Method, and also displays or hides another Method or the Reason in that Paragraph. })

(^ Amalgamation ^)

[- Cross union -]

({ The thing whose features are all the unions of a feature of +a and a feature of +b will be called the cross union of +a and +b, and represented by +xu// +a +b. })

+Df +Xu [a [b [c = +ft// +c +xu// +a +b ]d ]f ( +ft// +d +a ( +ft// +f +b +sm// +c +un// +d +f
+Xu1 +Pr ) - +Xu = +ft// +c +xu// +a +b ]d ]f ( +ft// +d +a ( +ft// +f +b +sm// +c +un// +d +f

({ +xu// +a +b is symmetrical. })

+Xu2 +Pr ) - ( +Th ( +Am +Xu +sm// +xu// +a +b +xu// +b +a
+Xu3 +Pr ) - ( +Th ( +Am +Xu ) - +ft/ +b = +ft// +c +xu// +a +th/ +b ]d ( +ft// +d +a +sm// +c +un// +d +b
+Xu4 +Pr ) - ( +Th ( +Am +Xu ) - ( +ft/ +a +ft/ +b = +ft// +c +xu// +th/ +a +th/ +b +sm// +c +un// +a +b
+Xu5 +Pr ) - ( +Th ( +Am +Xu ) - ( +ft/ +a +ft/ +b +ft// +un// +a +b +xu// +th/ +a +th/ +b

({ The union of two features is a feature. })

+Un6 +Pr ) - ( +Th ( +Am +Xu ) - ( +ft/ +a +ft/ +b +ft/ +un// +a +b

({ The following Fact is called the associative property of unions. })

+Un7 +Pr ) - ( +Th ( +Am ( +Xu ( +ft/ +a ( +ft/ +b +ft/ +c +sm// +un// +a +un// +b +c +un// +un// +a +b +c

({ If +a and +b are features, then +th// +a +b is a feature. })

+Th21 +Pr ) - ( +Th ( +Am ( +Dv +Xu ) - ( +ft/ +a +ft/ +b +ft/ +th// +a +b

({ The thing whose features are +a, +b, and +c will be represented by +th/// +a +b +c. })

+Df +th/// +a +b +c +un// +th/ +a +th// +b +c
+Th22 +Pr ) - ( +Th ( +Am ( +Dv +Xu ) - ( +ft/ +a ( +ft/ +b +ft/ +c = +ft// +d +th/// +a +b +c ) +sm// +d +a ) +sm// +d +b +sm// +d +c
+Th23 +Pr ) - ( +Th ( +Am ( +Dv +Xu ) - ( +ft/ +a ( +ft/ +b +ft/ +c +ft/ +th/// +a +b +c
+Th24 +Pr ) - ( +Th ( +Am ( +Dv ( +Xu ( +ft/ +a ( +ft/ +b +ft/ +c +sm// +th/// +a +b +c +un// +th// +a +b +th/ +c

({ The thing whose features are +a, +b, +c, and +d will be represented by +th//// +a +b +c +d. })

+Df +th//// +a +b +c +d +un// +th// +a +b +th// +c +d
+Th25 +Pr ) - ( +Th ( +Am ( +Dv ( +Xu ( +ft/ +a ( +ft/ +b ( +ft/ +c +ft/ +d = +ft// +e +th//// +a +b +c +d ) +sm// +e +a ) +sm// +e +b ) +sm// +e +c +sm// +e +d
+Sm9 +Pr = +sm// +a +b [e = +ft// +e +a +ft// +e +b
+Th26 +Pr ) - ( +Th ( +Am ( +Dv ( +Xu ( +ft/ +a ( +ft/ +b +ft/ +d ) - +sm// +b +c +sm// +th//// +a +b +c +d +th/// +a +b +d
+Th27 +Pr ) - ( +Th ( +Am ( +Dv +Xu ) - ( +ft/ +a ( +ft/ +b ( +ft/ +c ( +ft/ +d +ft/ +e ) - +sm// +th// +th/ +a +th// +e +b +th// +th/ +c +th// +e +d ( +sm// +a +c +sm// +b +d
+Th28 +Pr ) - ( +Nf ( +Th ( +Am ( +Dv +Xu ) - +ft/ +b +ft/ +th// +0 +th/ +b

({ A link from +a to +b is a thing that has a first end at +a and a second end at +b. The following Definition gives an example. })

+Df +lk// +a +b +th// +th/ +a +th// +0 +th/ +b

({ The relation of being the same is transmitted for links. })

+Lk1 +Pr ) - ( +Nf ( +Th ( +Am ( +Dv ( +Xu ( +ft/ +a ( +ft/ +b +sm// +a +d +sm// +lk// +a +b +lk// +d +b
+Lk2 +Pr ) - ( +Nf ( +Th ( +Am ( +Dv ( +Xu ( +ft/ +a ( +ft/ +b +sm// +a +d +sm// +lk// +b +a +lk// +b +d

({ If +a and +b are features, then +lk// +a +b is a feature. })

+Lk3 +Pr ) - ( +Nf ( +Th ( +Am ( +Dv +Xu ) - ( +ft/ +a +ft/ +b +ft/ +lk// +a +b

({ If two links are the same, then the first end of one is the same as the first end of the other, and the second end of one is the same as the second end of the other. })

+Lk4 +Pr ) - ( +Nf ( +Th ( +Am ( +Dv +Xu ) - ( +ft/ +a ( +ft/ +b ( +ft/ +d +ft/ +f ) - +sm// +lk// +a +b +lk// +d +f ( +sm// +a +d +sm// +b +f

(_ PartialDifference _)

({ The English and Verish text on this website is licensed for use under the Free Software Foundation Free Documentation License, and the software is licensed for use under the Free Software Foundation General Public License. })

({ Page last updated 25 May 2018. Copyright (c) Chris Austin 1997 - 2018. Privacy policy })