let p be Instruction-Sequence of SCM+FSA; :: thesis: for a being read-write Int-Location
for I being MacroInstruction of SCM+FSA
for s being 0 -started State of SCM+FSA st while>0 (a,I) c= p & s . a <= 0 holds
( LifeSpan (p,s) = 3 & ( for k being Nat holds DataPart (Comput (p,s,k)) = DataPart s ) )
let a be read-write Int-Location; :: thesis: for I being MacroInstruction of SCM+FSA
for s being 0 -started State of SCM+FSA st while>0 (a,I) c= p & s . a <= 0 holds
( LifeSpan (p,s) = 3 & ( for k being Nat holds DataPart (Comput (p,s,k)) = DataPart s ) )
let I be MacroInstruction of SCM+FSA ; :: thesis: for s being 0 -started State of SCM+FSA st while>0 (a,I) c= p & s . a <= 0 holds
( LifeSpan (p,s) = 3 & ( for k being Nat holds DataPart (Comput (p,s,k)) = DataPart s ) )
let s be 0 -started State of SCM+FSA; :: thesis: ( while>0 (a,I) c= p & s . a <= 0 implies ( LifeSpan (p,s) = 3 & ( for k being Nat holds DataPart (Comput (p,s,k)) = DataPart s ) ) )
A1: Start-At (0,SCM+FSA) c= s by MEMSTR_0:29;
assume that
A2: while>0 (a,I) c= p and
A3: s . a <= 0 ; :: thesis: ( LifeSpan (p,s) = 3 & ( for k being Nat holds DataPart (Comput (p,s,k)) = DataPart s ) )
A4: p +* (while>0 (a,I)) = p by A2, FUNCT_4:98;
set i = a >0_goto 3;
set s1 = Initialize s;
set p1 = p +* (while>0 (a,I));
A5: while>0 (a,I) c= p +* (while>0 (a,I)) by FUNCT_4:25;
A6: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
not a in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;
then A7: (Initialize s) . a = s . a by FUNCT_4:11;
A8: 1 in dom (while>0 (a,I)) by SCMFSA_X:9;
A9: (p +* (while>0 (a,I))) . 1 = (while>0 (a,I)) . 1 by A8, FUNCT_4:13
.= goto 2 by SCMFSA_X:10 ;
A10: IC (Initialize s) = IC (Start-At (0,SCM+FSA)) by A6, FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
A11: (p +* (while>0 (a,I))) /. (IC (Initialize s)) = (p +* (while>0 (a,I))) . (IC (Initialize s)) by PBOOLE:143;
0 in dom (while>0 (a,I)) by AFINSQ_1:65;
then (p +* (while>0 (a,I))) . 0 = (while>0 (a,I)) . 0 by FUNCT_4:13
.= a >0_goto 3 by SCMFSA_X:10 ;
then A12: CurInstr ((p +* (while>0 (a,I))),(Initialize s)) = a >0_goto 3 by A10, A11;
A13: Comput ((p +* (while>0 (a,I))),(Initialize s),(0 + 1)) = Following ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(Initialize s),0))) by EXTPRO_1:3
.= Exec ((a >0_goto 3),(Initialize s)) by A12 ;
set loc5 = (card I) + 4;
set s5 = Comput ((p +* (while>0 (a,I))),(Initialize s),3);
set p5 = p +* (while>0 (a,I));
set s4 = Comput ((p +* (while>0 (a,I))),(Initialize s),2);
set p4 = p +* (while>0 (a,I));
set s2 = Comput ((p +* (while>0 (a,I))),(Initialize s),1);
A14: 2 in dom (while>0 (a,I)) by SCMFSA_X:7;
A15: (p +* (while>0 (a,I))) . 2 = (while>0 (a,I)) . 2 by A14, FUNCT_4:13
.= goto ((card I) + 4) by SCMFSA_X:17 ;
A16: (card I) + 4 in dom (while>0 (a,I)) by SCMFSA_X:8;
A17: (p +* (while>0 (a,I))) . ((card I) + 4) = (while>0 (a,I)) . ((card I) + 4) by A16, A5, GRFUNC_1:2
.= halt SCM+FSA by SCMFSA_X:16 ;
A18: ( ( for c being Int-Location holds (Exec ((goto ((card I) + 4)),(Comput ((p +* (while>0 (a,I))),(Initialize s),2)))) . c = (Comput ((p +* (while>0 (a,I))),(Initialize s),2)) . c ) & ( for f being FinSeq-Location holds (Exec ((goto ((card I) + 4)),(Comput ((p +* (while>0 (a,I))),(Initialize s),2)))) . f = (Comput ((p +* (while>0 (a,I))),(Initialize s),2)) . f ) ) by SCMFSA_2:69;
A19: ( ( for c being Int-Location holds (Exec ((goto 2),(Comput ((p +* (while>0 (a,I))),(Initialize s),1)))) . c = (Comput ((p +* (while>0 (a,I))),(Initialize s),1)) . c ) & ( for f being FinSeq-Location holds (Exec ((goto 2),(Comput ((p +* (while>0 (a,I))),(Initialize s),1)))) . f = (Comput ((p +* (while>0 (a,I))),(Initialize s),1)) . f ) ) by SCMFSA_2:69;
A20: (p +* (while>0 (a,I))) /. (IC (Comput ((p +* (while>0 (a,I))),(Initialize s),1))) = (p +* (while>0 (a,I))) . (IC (Comput ((p +* (while>0 (a,I))),(Initialize s),1))) by PBOOLE:143;
IC (Comput ((p +* (while>0 (a,I))),(Initialize s),1)) = 0 + 1 by A3, A10, A13, A7, SCMFSA_2:71;
then A21: CurInstr ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(Initialize s),1))) = goto 2 by A9, A20;
A22: Comput ((p +* (while>0 (a,I))),(Initialize s),(1 + 1)) = Following ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(Initialize s),1))) by EXTPRO_1:3
.= Exec ((goto 2),(Comput ((p +* (while>0 (a,I))),(Initialize s),1))) by A21 ;
A23: (p +* (while>0 (a,I))) /. (IC (Comput ((p +* (while>0 (a,I))),(Initialize s),2))) = (p +* (while>0 (a,I))) . (IC (Comput ((p +* (while>0 (a,I))),(Initialize s),2))) by PBOOLE:143;
IC (Comput ((p +* (while>0 (a,I))),(Initialize s),2)) = 2 by A22, SCMFSA_2:69;
then A24: CurInstr ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(Initialize s),2))) = goto ((card I) + 4) by A15, A23;
A25: Comput ((p +* (while>0 (a,I))),(Initialize s),(2 + 1)) = Following ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(Initialize s),2))) by EXTPRO_1:3
.= Exec ((goto ((card I) + 4)),(Comput ((p +* (while>0 (a,I))),(Initialize s),2))) by A24 ;
A26: (p +* (while>0 (a,I))) /. (IC (Comput ((p +* (while>0 (a,I))),(Initialize s),3))) = (p +* (while>0 (a,I))) . (IC (Comput ((p +* (while>0 (a,I))),(Initialize s),3))) by PBOOLE:143;
IC (Comput ((p +* (while>0 (a,I))),(Initialize s),3)) = (card I) + 4 by A25, SCMFSA_2:69;
then A27: CurInstr ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(Initialize s),3))) = halt SCM+FSA by A17, A26;
then A28: p +* (while>0 (a,I)) halts_on Initialize s by EXTPRO_1:29;
A29: s = Initialize s by A1, FUNCT_4:98;
hence A31: LifeSpan (p,s) = 3 by A29, A27, A28, A4, EXTPRO_1:def 15; :: thesis: for k being Nat holds DataPart (Comput (p,s,k)) = DataPart s
A32: ( ( for c being Int-Location holds (Exec ((a >0_goto 3),(Initialize s))) . c = (Initialize s) . c ) & ( for f being FinSeq-Location holds (Exec ((a >0_goto 3),(Initialize s))) . f = (Initialize s) . f ) ) by SCMFSA_2:71;
then A33: DataPart (Comput (p,s,1)) = DataPart s by A29, A13, A4, SCMFSA_M:2;
then DataPart (Comput (p,s,2)) = DataPart s by A29, A22, A19, A4, SCMFSA_M:2;
then A34: DataPart (Comput (p,s,3)) = DataPart s by A29, A25, A18, A4, SCMFSA_M:2;
let k be Nat; :: thesis: DataPart (Comput (p,s,k)) = DataPart s
( k <= 2 or 2 < k ) ;
then A35: ( not not k = 0 & ... & not k = 2 or 2 + 1 <= k ) by NAT_1:13;