let S be COM-Struct ; :: thesis: for F, G, H being MacroInstruction of S holds (F ';' G) ';' H = F ';' (G ';' H)
let F, G, H be MacroInstruction 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 = ((Stop S) ';' G) ';' H
.= F ';' (G ';' H) by A1 ;
:: thesis: verum
end;
suppose A2: G = Stop S ; :: thesis: (F ';' G) ';' H = F ';' (G ';' H)
hence (F ';' G) ';' H = (F ';' (Stop S)) ';' H
.= F ';' (G ';' H) by A2 ;
:: 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 Th11
.= ((((card F) + (card G)) - 1) + (card H)) - 1 by Th11
.= ((((card F) + (card G)) + (card H)) - 1) - 1 ;
A6: card (F ';' (G ';' H)) = ((card F) + (card (G ';' H))) - 1 by Th11
.= ((card F) + (((card G) + (card H)) - 1)) - 1 by Th11
.= ((((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:68;
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:68;
for x being object 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 object ; :: 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 (Reloc ((G ';' H),((card F) -' 1))) = { (m + ((card F) -' 1)) where m is Nat : m in dom (IncAddr ((G ';' H),((card F) -' 1))) } by VALUED_1:def 12;
A12: dom (Reloc (H,((card (F ';' G)) -' 1))) = { (m + ((card (F ';' G)) -' 1)) where m is Nat : m in dom (IncAddr (H,((card (F ';' G)) -' 1))) } by VALUED_1:def 12;
A13: dom (Reloc (H,((card G) -' 1))) = { (m + ((card G) -' 1)) where m is 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:20
.= (((card F) + (card G)) - 1) - 1 by Th11 ;
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:20
.= ((card G) -' 1) + ((card F) -' 1) by PRE_CIRC:20 ;
A16: dom (Reloc (G,((card F) -' 1))) = { (m + ((card F) -' 1)) where m is Nat : m in dom (IncAddr (G,((card F) -' 1))) } by VALUED_1:def 12;
A17: (card F) -' 1 = (card F) - 1 by PRE_CIRC:20;
A18: (card G) -' 1 = (card G) - 1 by PRE_CIRC:20;
A19: for W being MacroInstruction of S st W <> Stop S holds
2 <= card W
proof
let W be MacroInstruction 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, Th6, NAT_1:25; :: 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, Lm5;
suppose A23: k < (card F) - 1 ; :: thesis: ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x
A24: CutLastLoc F c= CutLastLoc (F ';' G) by Th13;
A25: now :: thesis: not x in dom (Reloc ((G ';' H),((card F) -' 1)))
assume x in dom (Reloc ((G ';' H),((card F) -' 1))) ; :: thesis: contradiction
then consider m being 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:20;
then m + ((card F) - 1) < (card F) -' 1 by A23, PRE_CIRC:20;
then m + ((card F) -' 1) < (card F) -' 1 by PRE_CIRC:20;
hence contradiction by NAT_1:11; :: thesis: verum
end;
A27: now :: thesis: not x in dom (Reloc (H,((card (F ';' G)) -' 1)))
assume x in dom (Reloc (H,((card (F ';' G)) -' 1))) ; :: thesis: contradiction
then consider m being 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:20;
hence contradiction by NAT_1:11; :: thesis: verum
end;
k < card (CutLastLoc F) by A23, VALUED_1:38;
then A29: x in dom (CutLastLoc F) by A9, AFINSQ_1:66;
thus ((F ';' G) ';' H) . x = (CutLastLoc (F ';' G)) . x by A27, FUNCT_4:11
.= (CutLastLoc F) . x by A24, A29, GRFUNC_1:2
.= (F ';' (G ';' H)) . x by A25, FUNCT_4:11 ; :: thesis: verum
end;
suppose A30: k = (card F) - 1 ; :: thesis: ((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x
A31: now :: thesis: not x in dom (Reloc (H,((card (F ';' G)) -' 1)))
assume x in dom (Reloc (H,((card (F ';' G)) -' 1))) ; :: thesis: contradiction
then consider m being 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:20;
then (card G) -' 1 = 0 ;
then (card G) - 1 = 0 by PRE_CIRC:20;
hence contradiction by A4, Th6; :: thesis: verum
end;
A33: 0 in dom (IncAddr ((G ';' H),((card F) -' 1))) by AFINSQ_1:65;
A34: 0 in dom (IncAddr (G,((card F) -' 1))) by AFINSQ_1:65;
A35: 0 in dom G by AFINSQ_1:65;
A36: 0 in dom (G ';' H) by AFINSQ_1:65;
k = 0 + ((card F) -' 1) by A30, PRE_CIRC:20;
then A37: x in dom (Reloc ((G ';' H),((card F) -' 1))) by A9, A11, A33;
A38: k = (card F) -' 1 by A30, PRE_CIRC:20;
A39: x = 0 + k by A9;
0 in dom (IncAddr (G,((card F) -' 1))) by AFINSQ_1:65;
then A40: x in dom (Reloc (G,((card F) -' 1))) by A16, A38, A39;
then x in (dom (CutLastLoc F)) \/ (dom (Reloc (G,((card F) -' 1)))) by XBOOLE_0:def 3;
then A41: x in dom (F ';' G) by FUNCT_4:def 1;
now :: thesis: not x in dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G))))
A42: dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G)))) = {(LastLoc (F ';' G))}
.= {((card (F ';' G)) -' 1)} by AFINSQ_1:70 ;
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:20;
hence contradiction by A4, Th6; :: 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, Th6, XXREAL_0:1;
then A44: (card G) - 1 > 1 - 1 by XREAL_1:9;
then (card G) -' 1 > 1 - 1 by PRE_CIRC:20;
then A45: not 0 in dom (Reloc (H,((card G) -' 1))) by VALUED_1:29;
card (CutLastLoc G) <> {} by A44, VALUED_1:38;
then A46: 0 in dom (CutLastLoc G) by AFINSQ_1:65, CARD_1:27;
A47: G /. 0 = G . 0 by A35, PARTFUN1:def 6
.= (CutLastLoc G) . 0 by A46, GRFUNC_1:2
.= (G ';' H) . 0 by A45, FUNCT_4:11
.= (G ';' H) /. 0 by A36, PARTFUN1:def 6 ;
thus ((F ';' G) ';' H) . x = ((F ';' G) \ ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G))))) . x by A31, FUNCT_4:11
.= ((CutLastLoc F) +* (Reloc (G,((card F) -' 1)))) . x by A43, GRFUNC_1:32
.= (Reloc (G,((card F) -' 1))) . x by A40, FUNCT_4:13
.= (IncAddr (G,((card F) -' 1))) . 0 by A34, A38, A39, VALUED_1:def 12
.= IncAddr (((G ';' H) /. 0),((card F) -' 1)) by A35, A47, Def9
.= (IncAddr ((G ';' H),((card F) -' 1))) . 0 by A36, Def9
.= (Reloc ((G ';' H),((card F) -' 1))) . x by A33, A38, A39, VALUED_1:def 12
.= (F ';' (G ';' H)) . x by A37, FUNCT_4:13 ; :: 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 :: thesis: not x in dom (Reloc (H,((card (F ';' G)) -' 1)))
assume x in dom (Reloc (H,((card (F ';' G)) -' 1))) ; :: thesis: contradiction
then consider m being 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;
hence contradiction by XREAL_1:6; :: 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:235, XXREAL_0:2;
A53: (card F) - (card F) <= k - (card F) by A48, XREAL_1:9;
(card F) - 1 < (card F) - 0 by XREAL_1:15;
then k - ((card F) - 1) >= 0 by A53, XREAL_1:15;
then A54: k - ((card F) -' 1) >= 0 by PRE_CIRC:20;
A55: ((card F) + (card G)) - 3 < (((card F) + (card G)) - 3) + 1 by XREAL_1:29;
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:7;
then k - ((card F) -' 1) < (card G) - 1 by PRE_CIRC:20;
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:38;
then A57: k -' ((card F) -' 1) in dom (CutLastLoc G) by AFINSQ_1:66;
then k -' ((card F) -' 1) in (dom (CutLastLoc G)) \/ (dom (Reloc (H,((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 Def9;
then A60: x in dom (Reloc ((G ';' H),((card F) -' 1))) by A11, A52;
((card G) + (card F)) - 2 < ((card F) + (card G)) - 1 by XREAL_1:15;
then k < ((card F) + (card G)) - 1 by A56, XXREAL_0:2;
then k < card (F ';' G) by Th11;
then A61: x in dom (F ';' G) by A9, AFINSQ_1:66;
now :: thesis: not x in dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G))))
assume x in dom ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G)))) ; :: thesis: contradiction
then x in {(LastLoc (F ';' G))} ;
then x = LastLoc (F ';' G) by TARSKI:def 1
.= (card (F ';' G)) -' 1 by AFINSQ_1:70 ;
then k = ((card G) - 1) + ((card F) - 1) by A9, A15, A18, PRE_CIRC:20;
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:2;
then k -' ((card F) -' 1) in dom G by A57;
then A64: k -' ((card F) -' 1) in dom (IncAddr (G,((card F) -' 1))) by Def9;
then A65: x in dom (Reloc (G,((card F) -' 1))) by A16, A52;
A66: now :: thesis: not k -' ((card F) -' 1) in dom (Reloc (H,((card G) -' 1)))
assume k -' ((card F) -' 1) in dom (Reloc (H,((card G) -' 1))) ; :: thesis: contradiction
then consider m being 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:20
.= (k - ((card F) - 1)) - ((card G) - 1) by PRE_CIRC:20
.= 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:9;
hence contradiction by A68, Lm4; :: thesis: verum
end;
A69: (G ';' H) /. (k -' ((card F) -' 1)) = ((CutLastLoc G) +* (Reloc (H,((card G) -' 1)))) . (k -' ((card F) -' 1)) by A58, PARTFUN1:def 6
.= (CutLastLoc G) . (k -' ((card F) -' 1)) by A66, FUNCT_4:11
.= G . (k -' ((card F) -' 1)) by A57, GRFUNC_1:2 ;
thus ((F ';' G) ';' H) . x = ((F ';' G) \ ((LastLoc (F ';' G)) .--> ((F ';' G) . (LastLoc (F ';' G))))) . x by A50, FUNCT_4:11
.= ((CutLastLoc F) +* (Reloc (G,((card F) -' 1)))) . x by A62, GRFUNC_1:32
.= (Reloc (G,((card F) -' 1))) . x by A65, FUNCT_4:13
.= (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, Def9
.= IncAddr (((G ';' H) /. (k -' ((card F) -' 1))),((card F) -' 1)) by A57, A63, A69, PARTFUN1:def 6
.= (IncAddr ((G ';' H),((card F) -' 1))) . (k -' ((card F) -' 1)) by A58, Def9
.= (Reloc ((G ';' H),((card F) -' 1))) . x by A52, A59, VALUED_1:def 12
.= (F ';' (G ';' H)) . x by A60, FUNCT_4:13 ; :: 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:235;
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:65;
then A74: x in dom (Reloc (H,((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:6;
then (card G) -' 1 < ((card G) + (card H)) - 1 by PRE_CIRC:20;
then (card G) -' 1 < card (G ';' H) by Th11;
then A76: (card G) -' 1 in dom (G ';' H) by AFINSQ_1:66;
then A77: (card G) -' 1 in dom (IncAddr ((G ';' H),((card F) -' 1))) by Def9;
then A78: x in dom (Reloc ((G ';' H),((card F) -' 1))) by A11, A75;
A79: 0 in dom H by AFINSQ_1:65;
A80: (G ';' H) /. ((card G) -' 1) = (G ';' H) . ((card G) -' 1) by A76, PARTFUN1:def 6;
A81: 0 in dom (IncAddr (H,((card G) -' 1))) by AFINSQ_1:65;
then A82: (IncAddr (H,((card G) -' 1))) /. 0 = (IncAddr (H,((card G) -' 1))) . 0 by PARTFUN1:def 6
.= IncAddr ((H /. 0),((card G) -' 1)) by A79, Def9 ;
(G ';' H) /. ((card G) -' 1) = (G ';' H) . (LastLoc G) by A80, AFINSQ_1:70
.= (IncAddr (H,((card G) -' 1))) . 0 by Th14
.= (IncAddr (H,((card G) -' 1))) /. 0 by A81, PARTFUN1:def 6 ;
then A83: IncAddr (((G ';' H) /. ((card G) -' 1)),((card F) -' 1)) = IncAddr ((H /. 0),((card (F ';' G)) -' 1)) by A15, A82, COMPOS_0:7;
thus ((F ';' G) ';' H) . x = (Reloc (H,((card (F ';' G)) -' 1))) . x by A74, FUNCT_4:13
.= (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, Def9
.= (IncAddr ((G ';' H),((card F) -' 1))) . ((card G) -' 1) by A76, A83, Def9
.= (Reloc ((G ';' H),((card F) -' 1))) . x by A75, A77, VALUED_1:def 12
.= (F ';' (G ';' H)) . x by A78, FUNCT_4:13 ; :: 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:235;
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:21;
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:66;
then A87: k -' ((card (F ';' G)) -' 1) in dom (IncAddr (H,((card (F ';' G)) -' 1))) by Def9;
then A88: x in dom (Reloc (H,((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:235, XXREAL_0:2;
A92: k - ((card F) -' 1) >= 0 by A90, XREAL_1:48;
A93: k - ((card F) -' 1) < (((((card F) + (card G)) + (card H)) - 1) - 1) - ((card F) -' 1) by A10, XREAL_1:9;
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 Th11;
then A95: k -' ((card F) -' 1) in dom (G ';' H) by AFINSQ_1:66;
then k -' ((card F) -' 1) in dom (IncAddr ((G ';' H),((card F) -' 1))) by Def9;
then A96: x in dom (Reloc ((G ';' H),((card F) -' 1))) by A11, A91;
A97: k -' ((card F) -' 1) in dom (IncAddr ((G ';' H),((card F) -' 1))) by A95, Def9;
A98: k - ((card F) -' 1) >= ((card (F ';' G)) -' 1) - ((card F) -' 1) by A14, A84, XREAL_1:9;
then A99: k -' ((card F) -' 1) >= (((card F) -' 1) + ((card G) -' 1)) - ((card F) -' 1) by A14, A15, A84, A89, XREAL_1:233, XXREAL_0:2;
A100: k -' ((card F) -' 1) >= (card G) -' 1 by A14, A15, A84, A89, A98, XREAL_1:233, XXREAL_0:2;
A101: k -' ((card F) -' 1) = ((k -' ((card F) -' 1)) -' ((card G) -' 1)) + ((card G) -' 1) by A99, XREAL_1:235;
(k -' ((card F) -' 1)) - ((card G) -' 1) < (((card G) + (card H)) - 1) - ((card G) - 1) by A18, A94, XREAL_1:9;
then (k -' ((card F) -' 1)) -' ((card G) -' 1) < ((card H) + ((card G) - 1)) - ((card G) - 1) by A100, XREAL_1:233;
then (k -' ((card F) -' 1)) -' ((card G) -' 1) in dom H by AFINSQ_1:66;
then A102: (k -' ((card F) -' 1)) -' ((card G) -' 1) in dom (IncAddr (H,((card G) -' 1))) by Def9;
then A103: k -' ((card F) -' 1) in dom (Reloc (H,((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:233
.= (k - ((card F) -' 1)) - ((card G) -' 1) by A14, A15, A84, A89, XREAL_1:233, XXREAL_0:2
.= k - (((card F) -' 1) + ((card G) -' 1))
.= k -' ((card (F ';' G)) -' 1) by A14, A15, A84, XREAL_1:233 ;
A105: (G ';' H) /. (k -' ((card F) -' 1)) = ((CutLastLoc G) +* (Reloc (H,((card G) -' 1)))) . (k -' ((card F) -' 1)) by A95, PARTFUN1:def 6
.= (Reloc (H,((card G) -' 1))) . (k -' ((card F) -' 1)) by A103, FUNCT_4:13
.= (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, Def9 ;
thus ((F ';' G) ';' H) . x = (Reloc (H,((card (F ';' G)) -' 1))) . x by A88, FUNCT_4:13
.= (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, Def9
.= IncAddr (((G ';' H) /. (k -' ((card F) -' 1))),((card F) -' 1)) by A15, A105, COMPOS_0:7
.= (IncAddr ((G ';' H),((card F) -' 1))) . (k -' ((card F) -' 1)) by A95, Def9
.= (Reloc ((G ';' H),((card F) -' 1))) . x by A91, A97, VALUED_1:def 12
.= (F ';' (G ';' H)) . x by A96, FUNCT_4:13 ; :: thesis: verum
end;
end;
end;
hence (F ';' G) ';' H = F ';' (G ';' H) by A7, A8, FUNCT_1:2; :: thesis: verum
end;
end;