let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a <= 0 holds

DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (Initialized s)

let s be State of SCM+FSA; :: thesis: for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a <= 0 holds

DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (Initialized s)

let I be MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location st s . a <= 0 holds

DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (Initialized s)

let a be read-write Int-Location; :: thesis: ( s . a <= 0 implies DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (Initialized s) )

set D = Data-Locations ;

set Is = Initialized s;

set s1 = Initialize (Initialized s);

set P1 = P +* (while>0 (a,I));

A1: while>0 (a,I) c= P +* (while>0 (a,I)) by FUNCT_4:25;

set s2 = Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1);

set s4 = Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2);

set s5 = Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3);

set i = a >0_goto 3;

A2: 1 in dom (while>0 (a,I)) by SCMFSA_X:9;

A3: (P +* (while>0 (a,I))) . 1 = (while>0 (a,I)) . 1 by A2, A1, GRFUNC_1:2

.= goto 2 by SCMFSA_X:10 ;

IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;

then A4: IC (Initialize (Initialized s)) = IC (Start-At (0,SCM+FSA)) by FUNCT_4:13

.= 0 by FUNCOP_1:72 ;

0 in dom (while>0 (a,I)) by AFINSQ_1:65;

then A5: (P +* (while>0 (a,I))) . 0 = (while>0 (a,I)) . 0 by A1, GRFUNC_1:2

.= a >0_goto 3 by SCMFSA_X:10 ;

then A6: CurInstr ((P +* (while>0 (a,I))),(Initialize (Initialized s))) = a >0_goto 3 by A4, PBOOLE:143;

A7: Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(0 + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),0))) by EXTPRO_1:3

.= Following ((P +* (while>0 (a,I))),(Initialize (Initialized s)))

.= Exec ((a >0_goto 3),(Initialize (Initialized s))) by A4, A5, PBOOLE:143 ;

set loc5 = (card I) + 4;

A8: 2 in dom (while>0 (a,I)) by SCMFSA_X:7;

A9: (card I) + 4 in dom (while>0 (a,I)) by SCMFSA_X:8;

not a in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;

then A10: (Initialize (Initialized s)) . a = (Initialized s) . a by FUNCT_4:11;

assume s . a <= 0 ; :: thesis: DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (Initialized s)

then (Initialized s) . a <= 0 by SCMFSA_M:37;

then A11: IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)) = 0 + 1 by A4, A7, A10, SCMFSA_2:71;

A12: Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1))) by EXTPRO_1:3

.= Exec ((goto 2),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1))) by A11, A3, PBOOLE:143 ;

A13: (P +* (while>0 (a,I))) . 2 = (while>0 (a,I)) . 2 by A8, A1, GRFUNC_1:2

.= goto ((card I) + 4) by SCMFSA_X:17 ;

A14: (P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2))) by PBOOLE:143;

A15: Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(2 + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2))) by EXTPRO_1:3

.= Exec ((goto ((card I) + 4)),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2))) by A12, A13, A14, SCMFSA_2:69 ;

A16: (P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3))) by PBOOLE:143;

(P +* (while>0 (a,I))) . ((card I) + 4) = (while>0 (a,I)) . ((card I) + 4) by A9, A1, GRFUNC_1:2

.= halt SCM+FSA by SCMFSA_X:16 ;

then A17: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3))) = halt SCM+FSA by A15, A16, SCMFSA_2:69;

then A18: P +* (while>0 (a,I)) halts_on Initialize (Initialized s) by EXTPRO_1:29;

A19: (P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2))) by PBOOLE:143;

A20: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2))) = goto ((card I) + 4) by A12, A13, A19, SCMFSA_2:69;

A25: Initialized (Initialized s) = Initialize (Initialized (Initialized s)) by MEMSTR_0:44

.= Initialize (Initialized s) ;

A26: Initialize (Initialized s) = Initialized s by A25;

.= DataPart (Result ((P +* (while>0 (a,I))),(Initialized (Initialized s)))) by SCMFSA6B:def 1

.= DataPart (Result ((P +* (while>0 (a,I))),(Initialize (Initialized s)))) by A25

.= DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)) by A18, A24, EXTPRO_1:23

.= DataPart (Initialized s) by A27, A28, SCMFSA_M:2 ; :: thesis: verum

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a <= 0 holds

DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (Initialized s)

let s be State of SCM+FSA; :: thesis: for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a <= 0 holds

DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (Initialized s)

let I be MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location st s . a <= 0 holds

DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (Initialized s)

let a be read-write Int-Location; :: thesis: ( s . a <= 0 implies DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (Initialized s) )

set D = Data-Locations ;

set Is = Initialized s;

set s1 = Initialize (Initialized s);

set P1 = P +* (while>0 (a,I));

A1: while>0 (a,I) c= P +* (while>0 (a,I)) by FUNCT_4:25;

set s2 = Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1);

set s4 = Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2);

set s5 = Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3);

set i = a >0_goto 3;

A2: 1 in dom (while>0 (a,I)) by SCMFSA_X:9;

A3: (P +* (while>0 (a,I))) . 1 = (while>0 (a,I)) . 1 by A2, A1, GRFUNC_1:2

.= goto 2 by SCMFSA_X:10 ;

IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;

then A4: IC (Initialize (Initialized s)) = IC (Start-At (0,SCM+FSA)) by FUNCT_4:13

.= 0 by FUNCOP_1:72 ;

0 in dom (while>0 (a,I)) by AFINSQ_1:65;

then A5: (P +* (while>0 (a,I))) . 0 = (while>0 (a,I)) . 0 by A1, GRFUNC_1:2

.= a >0_goto 3 by SCMFSA_X:10 ;

then A6: CurInstr ((P +* (while>0 (a,I))),(Initialize (Initialized s))) = a >0_goto 3 by A4, PBOOLE:143;

A7: Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(0 + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),0))) by EXTPRO_1:3

.= Following ((P +* (while>0 (a,I))),(Initialize (Initialized s)))

.= Exec ((a >0_goto 3),(Initialize (Initialized s))) by A4, A5, PBOOLE:143 ;

set loc5 = (card I) + 4;

A8: 2 in dom (while>0 (a,I)) by SCMFSA_X:7;

A9: (card I) + 4 in dom (while>0 (a,I)) by SCMFSA_X:8;

not a in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;

then A10: (Initialize (Initialized s)) . a = (Initialized s) . a by FUNCT_4:11;

assume s . a <= 0 ; :: thesis: DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (Initialized s)

then (Initialized s) . a <= 0 by SCMFSA_M:37;

then A11: IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)) = 0 + 1 by A4, A7, A10, SCMFSA_2:71;

A12: Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1))) by EXTPRO_1:3

.= Exec ((goto 2),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1))) by A11, A3, PBOOLE:143 ;

A13: (P +* (while>0 (a,I))) . 2 = (while>0 (a,I)) . 2 by A8, A1, GRFUNC_1:2

.= goto ((card I) + 4) by SCMFSA_X:17 ;

A14: (P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2))) by PBOOLE:143;

A15: Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(2 + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2))) by EXTPRO_1:3

.= Exec ((goto ((card I) + 4)),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2))) by A12, A13, A14, SCMFSA_2:69 ;

A16: (P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3))) by PBOOLE:143;

(P +* (while>0 (a,I))) . ((card I) + 4) = (while>0 (a,I)) . ((card I) + 4) by A9, A1, GRFUNC_1:2

.= halt SCM+FSA by SCMFSA_X:16 ;

then A17: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3))) = halt SCM+FSA by A15, A16, SCMFSA_2:69;

then A18: P +* (while>0 (a,I)) halts_on Initialize (Initialized s) by EXTPRO_1:29;

A19: (P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2))) by PBOOLE:143;

A20: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2))) = goto ((card I) + 4) by A12, A13, A19, SCMFSA_2:69;

now :: thesis: for k being Nat st CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),k))) = halt SCM+FSA holds

2 + 1 <= k

then A24:
LifeSpan ((P +* (while>0 (a,I))),(Initialize (Initialized s))) = 3
by A17, A18, EXTPRO_1:def 15;2 + 1 <= k

let k be Nat; :: thesis: ( CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),k))) = halt SCM+FSA implies 2 + 1 <= k )

assume A21: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),k))) = halt SCM+FSA ; :: thesis: 2 + 1 <= k

A22: k <> 0 by A21, A6;

A23: k <> 1 by A11, A3, A21, PBOOLE:143;

k <> 2 by A20, A21;

then k <> 0 & ... & k <> 2 by A22, A23;

then 2 < k ;

hence 2 + 1 <= k by INT_1:7; :: thesis: verum

end;assume A21: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),k))) = halt SCM+FSA ; :: thesis: 2 + 1 <= k

A22: k <> 0 by A21, A6;

A23: k <> 1 by A11, A3, A21, PBOOLE:143;

k <> 2 by A20, A21;

then k <> 0 & ... & k <> 2 by A22, A23;

then 2 < k ;

hence 2 + 1 <= k by INT_1:7; :: thesis: verum

A25: Initialized (Initialized s) = Initialize (Initialized (Initialized s)) by MEMSTR_0:44

.= Initialize (Initialized s) ;

A26: Initialize (Initialized s) = Initialized s by A25;

A27: now :: thesis: for a being Int-Location holds (Initialized s) . a = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)) . a

let a be Int-Location; :: thesis: (Initialized s) . a = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)) . a

thus (Initialized s) . a = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)) . a by A7, A26, SCMFSA_2:71

.= (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2)) . a by A12, SCMFSA_2:69

.= (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)) . a by A15, SCMFSA_2:69 ; :: thesis: verum

end;thus (Initialized s) . a = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)) . a by A7, A26, SCMFSA_2:71

.= (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2)) . a by A12, SCMFSA_2:69

.= (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)) . a by A15, SCMFSA_2:69 ; :: thesis: verum

A28: now :: thesis: for f being FinSeq-Location holds (Initialized s) . f = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)) . f

thus DataPart (IExec ((while>0 (a,I)),P,s)) =
DataPart (IExec ((while>0 (a,I)),P,(Initialized s)))
by SCMFSA8C:3
let f be FinSeq-Location ; :: thesis: (Initialized s) . f = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)) . f

thus (Initialized s) . f = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)) . f by A7, A26, SCMFSA_2:71

.= (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2)) . f by A12, SCMFSA_2:69

.= (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)) . f by A15, SCMFSA_2:69 ; :: thesis: verum

end;thus (Initialized s) . f = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)) . f by A7, A26, SCMFSA_2:71

.= (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2)) . f by A12, SCMFSA_2:69

.= (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)) . f by A15, SCMFSA_2:69 ; :: thesis: verum

.= DataPart (Result ((P +* (while>0 (a,I))),(Initialized (Initialized s)))) by SCMFSA6B:def 1

.= DataPart (Result ((P +* (while>0 (a,I))),(Initialize (Initialized s)))) by A25

.= DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)) by A18, A24, EXTPRO_1:23

.= DataPart (Initialized s) by A27, A28, SCMFSA_M:2 ; :: thesis: verum