let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt COM-Struct of N
for F, G, H being pre-Macro of S holds (F ';' G) ';' H = F ';' (G ';' H)
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt COM-Struct of N; :: thesis: for F, G, H being pre-Macro of S holds (F ';' G) ';' H = F ';' (G ';' H)
let F, G, H be pre-Macro of S; :: thesis: (F ';' G) ';' H = F ';' (G ';' H)

per cases ( F = Stop S or G = Stop S or ( F <> Stop S & G <> Stop S ) ) ;

suppose A1: F = Stop S ; :: thesis: (F ';' G) ';' H = F ';' (G ';' H)

hence (F ';' G) ';' H = G ';' H by Th110
.= F ';' (G ';' H) by A1, Th110 ;
:: thesis: verum

end;

suppose A2: G = Stop S ; :: thesis: (F ';' G) ';' H = F ';' (G ';' H)

hence (F ';' G) ';' H = F ';' H by Th5
.= F ';' (G ';' H) by A2, Th110 ;
:: thesis: verum

end;

suppose that A3: F <> Stop S and
A4: G <> Stop S ; :: thesis: (F ';' G) ';' H = F ';' (G ';' H)

set X = { k where k is Element of NAT : k < ((((card F) + (card G)) + (card H)) - 1) - 1 } ;
A5: card ((F ';' G) ';' H) = ((card (F ';' G)) + (card H)) - 1 by Th102
.= ((((card F) + (card G)) - 1) + (card H)) - 1 by Th102
.= ((((card F) + (card G)) + (card H)) - 1) - 1 ;
A6: card (F ';' (G ';' H)) = ((card F) + (card (G ';' H))) - 1 by Th102
.= ((card F) + (((card G) + (card H)) - 1)) - 1 by Th102
.= ((((card F) + (card G)) + (card H)) - 1) - 1 ;
A7: dom ((F ';' G) ';' H) = { k where k is Element of NAT : k < ((((card F) + (card G)) + (card H)) - 1) - 1 } by A5, AFINSQ_1:72;
A8: dom (F ';' (G ';' H)) = { k where k is Element of NAT : k < ((((card F) + (card G)) + (card H)) - 1) - 1 } by A6, AFINSQ_1:72;
for x being set st x in { k where k is Element of NAT : k < ((((card F) + (card G)) + (card H)) - 1) - 1 } holds
((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x

proof

let x be set ; :: thesis: ( x in { k where k is Element of NAT : k < ((((card F) + (card G)) + (card H)) - 1) - 1 } implies ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x )
assume x in { k where k is Element of NAT : k < ((((card F) + (card G)) + (card H)) - 1) - 1 } ; :: thesis: ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x
then consider k being Element of NAT such that
A9: x = k and
A10: k < ((((card F) + (card G)) + (card H)) - 1) - 1 ;
A11: dom (Shift ((IncAddr ((G ';' H),((card F) -' 1))),((card F) -' 1))) = { (m + ((card F) -' 1)) where m is Element of NAT : m in dom (IncAddr ((G ';' H),((card F) -' 1))) } by VALUED_1:def 12;
A12: dom (Shift ((IncAddr (H,((card (F ';' G)) -' 1))),((card (F ';' G)) -' 1))) = { (m + ((card (F ';' G)) -' 1)) where m is Element of NAT : m in dom (IncAddr (H,((card (F ';' G)) -' 1))) } by VALUED_1:def 12;
A13: dom (Shift ((IncAddr (H,((card G) -' 1))),((card G) -' 1))) = { (m + ((card G) -' 1)) where m is Element of NAT : m in dom (IncAddr (H,((card G) -' 1))) } by VALUED_1:def 12;
A14: (card (F ';' G)) -' 1 = (card (F ';' G)) - 1 by PRE_CIRC:25
.= (((card F) + (card G)) - 1) - 1 by Th102 ;
then (card (F ';' G)) -' 1 = ((card F) - 1) + ((card G) - 1) ;
then A15: (card (F ';' G)) -' 1 = ((card G) -' 1) + ((card F) - 1) by PRE_CIRC:25
.= ((card G) -' 1) + ((card F) -' 1) by PRE_CIRC:25 ;
A16: dom (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1))) = { (m + ((card F) -' 1)) where m is Element of NAT : m in dom (IncAddr (G,((card F) -' 1))) } by VALUED_1:def 12;
A17: (card F) -' 1 = (card F) - 1 by PRE_CIRC:25;
A18: (card G) -' 1 = (card G) - 1 by PRE_CIRC:25;
A19: for W being pre-Macro of S st W <> Stop S holds
2 <= card W

proof

let W be pre-Macro of S; :: thesis: ( W <> Stop S implies 2 <= card W )
assume A20: W <> Stop S ; :: thesis: 2 <= card W
assume 2 > card W ; :: thesis: contradiction
then 1 + 1 > card W ;
then card W <= 1 by NAT_1:13;
hence contradiction by A20, Th89, NAT_1:26; :: thesis: verum

end;

then 2 <= card F by A3;
then A21: 1 <= card F by XXREAL_0:2;
A22: 2 <= card G by A4, A19;

per cases ( k < (card F) - 1 or k = (card F) - 1 or ( card F <= k & k <= ((card F) + (card G)) - 3 ) or k = ((card F) + (card G)) - 2 or ((card F) + (card G)) - 2 < k ) by A21, A22, Lm2;

suppose A23: k < (card F) - 1 ; :: thesis: ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x

A24: CutLastLoc F c= CutLastLoc (F ';' G) by Th104;

A25: now

assume x in dom (Shift ((IncAddr ((G ';' H),((card F) -' 1))),((card F) -' 1))) ; :: thesis: contradiction
then consider m being Element of NAT such that
A26: x = m + ((card F) -' 1) and
m in dom (IncAddr ((G ';' H),((card F) -' 1))) by A11;
k = m + ((card F) - 1) by A9, A26, PRE_CIRC:25;
then m + ((card F) - 1) < (card F) -' 1 by A23, PRE_CIRC:25;
then m + ((card F) -' 1) < (card F) -' 1 by PRE_CIRC:25;
hence contradiction by NAT_1:11; :: thesis: verum

end;

A27: now

assume x in dom (Shift ((IncAddr (H,((card (F ';' G)) -' 1))),((card (F ';' G)) -' 1))) ; :: thesis: contradiction
then consider m being Element of NAT such that
A28: x = m + ((card (F ';' G)) -' 1) and
m in dom (IncAddr (H,((card (F ';' G)) -' 1))) by A12;
(m + ((card G) -' 1)) + ((card F) -' 1) < (card F) -' 1 by A23, A9, A15, A28, PRE_CIRC:25;
hence contradiction by NAT_1:11; :: thesis: verum

end;

k < card (CutLastLoc F) by A23, VALUED_1:39;
then A29: x in dom (CutLastLoc F) by A9, AFINSQ_1:70;
thus ((F ';' G) ';' H) . x = (CutLastLoc (F ';' G)) . x by A27, FUNCT_4:12
.= (CutLastLoc F) . x by A24, A29, GRFUNC_1:8
.= (F ';' (G ';' H)) . x by A25, FUNCT_4:12 ; :: thesis: verum

end;

suppose A30: k = (card F) - 1 ; :: thesis: ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x

A31: now

assume x in dom (Shift ((IncAddr (H,((card (F ';' G)) -' 1))),((card (F ';' G)) -' 1))) ; :: thesis: contradiction
then consider m being Element of NAT such that
A32: x = m + ((card (F ';' G)) -' 1) and
m in dom (IncAddr (H,((card (F ';' G)) -' 1))) by A12;
(m + ((card G) -' 1)) + ((card F) -' 1) = (card F) -' 1 by A30, A15, A32, A9, PRE_CIRC:25;
then (card G) -' 1 = 0 ;
then (card G) - 1 = 0 by PRE_CIRC:25;
hence contradiction by A4, Th89; :: thesis: verum

end;

A33: 0 in dom (IncAddr ((G ';' H),((card F) -' 1))) by AFINSQ_1:69;
A34: 0 in dom (IncAddr (G,((card F) -' 1))) by AFINSQ_1:69;
A35: 0 in dom G by AFINSQ_1:69;
A36: 0 in dom (G ';' H) by AFINSQ_1:69;
k = 0 + ((card F) -' 1) by A30, PRE_CIRC:25;
then A37: x in dom (Shift ((IncAddr ((G ';' H),((card F) -' 1))),((card F) -' 1))) by A9, A11, A33;
A38: k = (card F) -' 1 by A30, PRE_CIRC:25;
A39: x = 0 + k by A9;
0 in dom (IncAddr (G,((card F) -' 1))) by AFINSQ_1:69;
then A40: x in dom (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1))) by A16, A38, A39;
then x in (dom (CutLastLoc F)) \/ (dom (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1)))) by XBOOLE_0:def 3;
then A41: x in dom (F ';' G) by FUNCT_4:def 1;

now

A42: dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G)))) = {(LastLoc (F ';' G))} by FUNCOP_1:19
.= {((card (F ';' G)) -' 1)} by AFINSQ_1:74 ;
assume x in dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G)))) ; :: thesis: contradiction
then x = (card (F ';' G)) -' 1 by A42, TARSKI:def 1;
then (card G) - 1 = 0 by A38, A9, A15, PRE_CIRC:25;
hence contradiction by A4, Th89; :: thesis: verum

end;

then A43: x in (dom (F ';' G)) \ (dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G))))) by A41, XBOOLE_0:def 5;
1 <= card G by NAT_1:14;
then card G > 1 by A4, Th89, XXREAL_0:1;
then A44: (card G) - 1 > 1 - 1 by XREAL_1:11;
then (card G) -' 1 > 1 - 1 by PRE_CIRC:25;
then A45: not 0 in dom (Shift ((IncAddr (H,((card G) -' 1))),((card G) -' 1))) by VALUED_1:30;
card (CutLastLoc G) <> {} by A44, VALUED_1:39;
then A46: 0 in dom (CutLastLoc G) by AFINSQ_1:69, CARD_1:47;
A47: G /. 0 = G . 0 by A35, PARTFUN1:def 8
.= (CutLastLoc G) . 0 by A46, GRFUNC_1:8
.= (G ';' H) . 0 by A45, FUNCT_4:12
.= (G ';' H) /. 0 by A36, PARTFUN1:def 8 ;
thus ((F ';' G) ';' H) . x = ((F ';' G) \ ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G))))) . x by A31, FUNCT_4:12
.= ((CutLastLoc F) +* (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1)))) . x by A43, GRFUNC_1:93
.= (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1))) . x by A40, FUNCT_4:14
.= (IncAddr (G,((card F) -' 1))) . 0 by A34, A38, A39, VALUED_1:def 12
.= IncAddr (((G ';' H) /. 0),((card F) -' 1)) by A35, A47, Def15
.= (IncAddr ((G ';' H),((card F) -' 1))) . 0 by A36, Def15
.= (Shift ((IncAddr ((G ';' H),((card F) -' 1))),((card F) -' 1))) . x by A33, A38, A39, VALUED_1:def 12
.= (F ';' (G ';' H)) . x by A37, FUNCT_4:14 ; :: thesis: verum

end;

suppose that A48: card F <= k and
A49: k <= ((card F) + (card G)) - 3 ; :: thesis: ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x

A50: now

assume x in dom (Shift ((IncAddr (H,((card (F ';' G)) -' 1))),((card (F ';' G)) -' 1))) ; :: thesis: contradiction
then consider m being Element of NAT such that
A51: x = m + ((card (F ';' G)) -' 1) and
m in dom (IncAddr (H,((card (F ';' G)) -' 1))) by A12;
m + (((card G) -' 1) + ((card F) -' 1)) <= (- 1) + (((card G) -' 1) + ((card F) -' 1)) by A9, A15, A17, A18, A49, A51;
then m <= - 1 by XREAL_1:8;
hence contradiction ; :: thesis: verum

end;

(card F) -' 1 <= card F by NAT_D:35;
then A52: x = (k -' ((card F) -' 1)) + ((card F) -' 1) by A9, A48, XREAL_1:237, XXREAL_0:2;
A53: (card F) - (card F) <= k - (card F) by A48, XREAL_1:11;
(card F) - 1 < (card F) - 0 by XREAL_1:17;
then k - ((card F) - 1) >= 0 by A53, XREAL_1:17;
then A54: k - ((card F) -' 1) >= 0 by PRE_CIRC:25;
A55: ((card F) + (card G)) - 3 < (((card F) + (card G)) - 3) + 1 by XREAL_1:31;
then A56: k < ((card G) - 1) + ((card F) - 1) by A49, XXREAL_0:2;
(k - ((card F) - 1)) + ((card F) - 1) < ((card G) - 1) + ((card F) - 1) by A49, A55, XXREAL_0:2;
then k - ((card F) - 1) < (card G) - 1 by XREAL_1:9;
then k - ((card F) -' 1) < (card G) - 1 by PRE_CIRC:25;
then k -' ((card F) -' 1) < (card G) - 1 by A54, XREAL_0:def 2;
then k -' ((card F) -' 1) < card (CutLastLoc G) by VALUED_1:39;
then A57: k -' ((card F) -' 1) in dom (CutLastLoc G) by AFINSQ_1:70;
then k -' ((card F) -' 1) in (dom (CutLastLoc G)) \/ (dom (Shift ((IncAddr (H,((card G) -' 1))),((card G) -' 1)))) by XBOOLE_0:def 3;
then A58: k -' ((card F) -' 1) in dom (G ';' H) by FUNCT_4:def 1;
then A59: k -' ((card F) -' 1) in dom (IncAddr ((G ';' H),((card F) -' 1))) by Def15;
then A60: x in dom (Shift ((IncAddr ((G ';' H),((card F) -' 1))),((card F) -' 1))) by A11, A52;
((card G) + (card F)) - 2 < ((card F) + (card G)) - 1 by XREAL_1:17;
then k < ((card F) + (card G)) - 1 by A56, XXREAL_0:2;
then k < card (F ';' G) by Th102;
then A61: x in dom (F ';' G) by A9, AFINSQ_1:70;

now

assume x in dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G)))) ; :: thesis: contradiction
then x in {(LastLoc (F ';' G))} by FUNCOP_1:19;
then x = LastLoc (F ';' G) by TARSKI:def 1
.= (card (F ';' G)) -' 1 by AFINSQ_1:74 ;
then k = ((card G) - 1) + ((card F) - 1) by A9, A15, A18, PRE_CIRC:25;
hence contradiction by A49, A55; :: thesis: verum

end;

then A62: x in (dom (F ';' G)) \ (dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G))))) by A61, XBOOLE_0:def 5;
A63: dom (CutLastLoc G) c= dom G by GRFUNC_1:8;
then k -' ((card F) -' 1) in dom G by A57;
then A64: k -' ((card F) -' 1) in dom (IncAddr (G,((card F) -' 1))) by Def15;
then A65: x in dom (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1))) by A16, A52;

A66: now

assume k -' ((card F) -' 1) in dom (Shift ((IncAddr (H,((card G) -' 1))),((card G) -' 1))) ; :: thesis: contradiction
then consider m being Element of NAT such that
A67: k -' ((card F) -' 1) = m + ((card G) -' 1) and
m in dom (IncAddr (H,((card G) -' 1))) by A13;
A68: m = (k -' ((card F) -' 1)) - ((card G) -' 1) by A67
.= (k - ((card F) -' 1)) - ((card G) -' 1) by A54, XREAL_0:def 2
.= (k - ((card F) - 1)) - ((card G) -' 1) by PRE_CIRC:25
.= (k - ((card F) - 1)) - ((card G) - 1) by PRE_CIRC:25
.= k - (((card F) + (card G)) - 2) ;
k - (((card F) + (card G)) - 2) <= (((card F) + (card G)) - 3) - (((card F) + (card G)) - 2) by A49, XREAL_1:11;
hence contradiction by A68, Lm1; :: thesis: verum

end;

A69: (G ';' H) /. (k -' ((card F) -' 1)) = ((CutLastLoc G) +* (Shift ((IncAddr (H,((card G) -' 1))),((card G) -' 1)))) . (k -' ((card F) -' 1)) by A58, PARTFUN1:def 8
.= (CutLastLoc G) . (k -' ((card F) -' 1)) by A66, FUNCT_4:12
.= G . (k -' ((card F) -' 1)) by A57, GRFUNC_1:8 ;
thus ((F ';' G) ';' H) . x = ((F ';' G) \ ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G))))) . x by A50, FUNCT_4:12
.= ((CutLastLoc F) +* (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1)))) . x by A62, GRFUNC_1:93
.= (Shift ((IncAddr (G,((card F) -' 1))),((card F) -' 1))) . x by A65, FUNCT_4:14
.= (IncAddr (G,((card F) -' 1))) . (k -' ((card F) -' 1)) by A52, A64, VALUED_1:def 12
.= IncAddr ((G /. (k -' ((card F) -' 1))),((card F) -' 1)) by A57, A63, Def15
.= IncAddr (((G ';' H) /. (k -' ((card F) -' 1))),((card F) -' 1)) by A57, A63, A69, PARTFUN1:def 8
.= (IncAddr ((G ';' H),((card F) -' 1))) . (k -' ((card F) -' 1)) by A58, Def15
.= (Shift ((IncAddr ((G ';' H),((card F) -' 1))),((card F) -' 1))) . x by A52, A59, VALUED_1:def 12
.= (F ';' (G ';' H)) . x by A60, FUNCT_4:14 ; :: thesis: verum

end;

suppose A70: k = ((card F) + (card G)) - 2 ; :: thesis: ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x

then A71: x = (k -' ((card (F ';' G)) -' 1)) + ((card (F ';' G)) -' 1) by A9, A14, XREAL_1:237;
k - ((card (F ';' G)) -' 1) = 0 by A14, A70;
then A72: k -' ((card (F ';' G)) -' 1) = 0 by XREAL_0:def 2;
then A73: k -' ((card (F ';' G)) -' 1) in dom (IncAddr (H,((card (F ';' G)) -' 1))) by AFINSQ_1:69;
then A74: x in dom (Shift ((IncAddr (H,((card (F ';' G)) -' 1))),((card (F ';' G)) -' 1))) by A12, A71;
A75: x = ((card G) -' 1) + ((card F) -' 1) by A9, A17, A18, A70;
((card G) - 1) + 0 < ((card G) - 1) + (card H) by XREAL_1:8;
then (card G) -' 1 < ((card G) + (card H)) - 1 by PRE_CIRC:25;
then (card G) -' 1 < card (G ';' H) by Th102;
then A76: (card G) -' 1 in dom (G ';' H) by AFINSQ_1:70;
then A77: (card G) -' 1 in dom (IncAddr ((G ';' H),((card F) -' 1))) by Def15;
then A78: x in dom (Shift ((IncAddr ((G ';' H),((card F) -' 1))),((card F) -' 1))) by A11, A75;
A79: 0 in dom H by AFINSQ_1:69;
A80: (G ';' H) /. ((card G) -' 1) = (G ';' H) . ((card G) -' 1) by A76, PARTFUN1:def 8;
A81: 0 in dom (IncAddr (H,((card G) -' 1))) by AFINSQ_1:69;
then A82: (IncAddr (H,((card G) -' 1))) /. 0 = (IncAddr (H,((card G) -' 1))) . 0 by PARTFUN1:def 8
.= IncAddr ((H /. 0),((card G) -' 1)) by A79, Def15 ;
(G ';' H) /. ((card G) -' 1) = (G ';' H) . (LastLoc G) by A80, AFINSQ_1:74
.= (IncAddr (H,((card G) -' 1))) . 0 by Th55
.= (IncAddr (H,((card G) -' 1))) /. 0 by A81, PARTFUN1:def 8 ;
then A83: IncAddr (((G ';' H) /. ((card G) -' 1)),((card F) -' 1)) = IncAddr ((H /. 0),((card (F ';' G)) -' 1)) by A15, A82, Th37;
thus ((F ';' G) ';' H) . x = (Shift ((IncAddr (H,((card (F ';' G)) -' 1))),((card (F ';' G)) -' 1))) . x by A74, FUNCT_4:14
.= (IncAddr (H,((card (F ';' G)) -' 1))) . (k -' ((card (F ';' G)) -' 1)) by A71, A73, VALUED_1:def 12
.= IncAddr ((H /. 0),((card (F ';' G)) -' 1)) by A72, A79, Def15
.= (IncAddr ((G ';' H),((card F) -' 1))) . ((card G) -' 1) by A76, A83, Def15
.= (Shift ((IncAddr ((G ';' H),((card F) -' 1))),((card F) -' 1))) . x by A75, A77, VALUED_1:def 12
.= (F ';' (G ';' H)) . x by A78, FUNCT_4:14 ; :: thesis: verum

end;

suppose A84: ((card F) + (card G)) - 2 < k ; :: thesis: ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x

then A85: x = (k -' ((card (F ';' G)) -' 1)) + ((card (F ';' G)) -' 1) by A9, A14, XREAL_1:237;
k + 0 < (((card F) + (card G)) - (1 + 1)) + (card H) by A10;
then k - (((card F) + (card G)) - (1 + 1)) < (card H) - 0 by XREAL_1:23;
then k -' ((card (F ';' G)) -' 1) < card H by A14, XREAL_0:def 2;
then A86: k -' ((card (F ';' G)) -' 1) in dom H by AFINSQ_1:70;
then A87: k -' ((card (F ';' G)) -' 1) in dom (IncAddr (H,((card (F ';' G)) -' 1))) by Def15;
then A88: x in dom (Shift ((IncAddr (H,((card (F ';' G)) -' 1))),((card (F ';' G)) -' 1))) by A12, A85;
A89: (card F) -' 1 <= ((card G) -' 1) + ((card F) -' 1) by NAT_1:11;
then A90: k >= (card F) -' 1 by A14, A15, A84, XXREAL_0:2;
A91: x = (k -' ((card F) -' 1)) + ((card F) -' 1) by A9, A14, A15, A84, A89, XREAL_1:237, XXREAL_0:2;
A92: k - ((card F) -' 1) >= 0 by A90, XREAL_1:50;
A93: k - ((card F) -' 1) < (((((card F) + (card G)) + (card H)) - 1) - 1) - ((card F) -' 1) by A10, XREAL_1:11;
then A94: k -' ((card F) -' 1) < ((((card F) + (card G)) + (card H)) - (card F)) - 1 by A17, A92, XREAL_0:def 2;
k -' ((card F) -' 1) < ((((card F) - (card F)) + (card G)) + (card H)) - 1 by A17, A92, A93, XREAL_0:def 2;
then k -' ((card F) -' 1) < card (G ';' H) by Th102;
then A95: k -' ((card F) -' 1) in dom (G ';' H) by AFINSQ_1:70;
then k -' ((card F) -' 1) in dom (IncAddr ((G ';' H),((card F) -' 1))) by Def15;
then A96: x in dom (Shift ((IncAddr ((G ';' H),((card F) -' 1))),((card F) -' 1))) by A11, A91;
A97: k -' ((card F) -' 1) in dom (IncAddr ((G ';' H),((card F) -' 1))) by A95, Def15;
A98: k - ((card F) -' 1) >= ((card (F ';' G)) -' 1) - ((card F) -' 1) by A14, A84, XREAL_1:11;
then A99: k -' ((card F) -' 1) >= (((card F) -' 1) + ((card G) -' 1)) - ((card F) -' 1) by A14, A15, A84, A89, XREAL_1:235, XXREAL_0:2;
A100: k -' ((card F) -' 1) >= (card G) -' 1 by A14, A15, A84, A89, A98, XREAL_1:235, XXREAL_0:2;
A101: k -' ((card F) -' 1) = ((k -' ((card F) -' 1)) -' ((card G) -' 1)) + ((card G) -' 1) by A99, XREAL_1:237;
(k -' ((card F) -' 1)) - ((card G) -' 1) < (((card G) + (card H)) - 1) - ((card G) - 1) by A18, A94, XREAL_1:11;
then (k -' ((card F) -' 1)) -' ((card G) -' 1) < ((card H) + ((card G) - 1)) - ((card G) - 1) by A100, XREAL_1:235;
then (k -' ((card F) -' 1)) -' ((card G) -' 1) in dom H by AFINSQ_1:70;
then A102: (k -' ((card F) -' 1)) -' ((card G) -' 1) in dom (IncAddr (H,((card G) -' 1))) by Def15;
then A103: k -' ((card F) -' 1) in dom (Shift ((IncAddr (H,((card G) -' 1))),((card G) -' 1))) by A13, A101;
A104: (k -' ((card F) -' 1)) -' ((card G) -' 1) = (k -' ((card F) -' 1)) - ((card G) -' 1) by A99, XREAL_1:235
.= (k - ((card F) -' 1)) - ((card G) -' 1) by A14, A15, A84, A89, XREAL_1:235, XXREAL_0:2
.= k - (((card F) -' 1) + ((card G) -' 1))
.= k -' ((card (F ';' G)) -' 1) by A14, A15, A84, XREAL_1:235 ;
A105: (G ';' H) /. (k -' ((card F) -' 1)) = ((CutLastLoc G) +* (Shift ((IncAddr (H,((card G) -' 1))),((card G) -' 1)))) . (k -' ((card F) -' 1)) by A95, PARTFUN1:def 8
.= (Shift ((IncAddr (H,((card G) -' 1))),((card G) -' 1))) . (k -' ((card F) -' 1)) by A103, FUNCT_4:14
.= (IncAddr (H,((card G) -' 1))) . (k -' ((card (F ';' G)) -' 1)) by A101, A102, A104, VALUED_1:def 12
.= IncAddr ((H /. (k -' ((card (F ';' G)) -' 1))),((card G) -' 1)) by A86, Def15 ;
thus ((F ';' G) ';' H) . x = (Shift ((IncAddr (H,((card (F ';' G)) -' 1))),((card (F ';' G)) -' 1))) . x by A88, FUNCT_4:14
.= (IncAddr (H,((card (F ';' G)) -' 1))) . (k -' ((card (F ';' G)) -' 1)) by A85, A87, VALUED_1:def 12
.= IncAddr ((H /. (k -' ((card (F ';' G)) -' 1))),((card (F ';' G)) -' 1)) by A86, Def15
.= IncAddr (((G ';' H) /. (k -' ((card F) -' 1))),((card F) -' 1)) by A15, A105, Th37
.= (IncAddr ((G ';' H),((card F) -' 1))) . (k -' ((card F) -' 1)) by A95, Def15
.= (Shift ((IncAddr ((G ';' H),((card F) -' 1))),((card F) -' 1))) . x by A91, A97, VALUED_1:def 12
.= (F ';' (G ';' H)) . x by A96, FUNCT_4:14 ; :: thesis: verum

end;

end;

end;

hence (F ';' G) ';' H = F ';' (G ';' H) by A7, A8, FUNCT_1:9; :: thesis: verum

end;

end;