let S be COM-Struct ; for F, G, H being MacroInstruction of S holds (F ';' G) ';' H = F ';' (G ';' H)
let F, G, H be MacroInstruction of S; (F ';' G) ';' H = F ';' (G ';' H)
per cases
( F = Stop S or G = Stop S or ( F <> Stop S & G <> Stop S ) )
;
suppose that A3:
F <> Stop S
and A4:
G <> Stop S
;
(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 ;
( 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 }
;
((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
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 A30:
k = (card F) - 1
;
((F ';' G) ';' H) . x = (F ';' (G ';' H)) . xA33:
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;
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
;
verum end; suppose that A48:
card F <= k
and A49:
k <= ((card F) + (card G)) - 3
;
((F ';' G) ';' H) . x = (F ';' (G ';' H)) . x
(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;
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;
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
;
verum end; suppose A70:
k = ((card F) + (card G)) - 2
;
((F ';' G) ';' H) . x = (F ';' (G ';' H)) . xthen 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
;
verum end; suppose A84:
((card F) + (card G)) - 2
< k
;
((F ';' G) ';' H) . x = (F ';' (G ';' H)) . xthen 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
;
verum end; end;
end; hence
(F ';' G) ';' H = F ';' (G ';' H)
by A7, A8, FUNCT_1:2;
verum end; end;