let p be Instruction-Sequence of SCM+FSA; :: thesis: for a being read-write Int-Location
for I being Program 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) = 4 & ( for k being Element of NAT holds DataPart (Comput (p,s,k)) = DataPart s ) )
let a be read-write Int-Location ; :: thesis: for I being Program 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) = 4 & ( for k being Element of NAT holds DataPart (Comput (p,s,k)) = DataPart s ) )
let I be Program 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) = 4 & ( for k being Element of 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) = 4 & ( for k being Element of NAT holds DataPart (Comput (p,s,k)) = DataPart s ) ) )
assume that
A2: while>0 (a,I) c= p and
A3: s . a <= 0 ; :: thesis: ( LifeSpan (p,s) = 4 & ( for k being Element of 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 4;
set p1 = p +* (while>0 (a,I));
A5: while>0 (a,I) c= p +* (while>0 (a,I)) by FUNCT_4:25;
B6: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
A8: 1 in dom (while>0 (a,I)) by SCMFSA_9:10;
A9: (p +* (while>0 (a,I))) . 1 = (while>0 (a,I)) . 1 by A8, FUNCT_4:13
.= goto 2 by SCMFSA_9:11 ;
s = Initialize s by MEMSTR_0:44;
then A10: IC s = IC (Start-At (0,SCM+FSA)) by B6, FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
A11: (p +* (while>0 (a,I))) /. (IC s) = (p +* (while>0 (a,I))) . (IC s) by PBOOLE:143;
0 in dom (while>0 (a,I)) by SCMFSA_9:10;
then (p +* (while>0 (a,I))) . 0 = (while>0 (a,I)) . 0 by FUNCT_4:13
.= a >0_goto 4 by SCMFSA_9:11 ;
then A12: CurInstr ((p +* (while>0 (a,I))),s) = a >0_goto 4 by A10, A11;
A13: Comput ((p +* (while>0 (a,I))),s,(0 + 1)) = Following ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),s,0))) by EXTPRO_1:3
.= Following ((p +* (while>0 (a,I))),s) by EXTPRO_1:2
.= Exec ((a >0_goto 4),s) by A12 ;
set loc5 = (card I) + 5;
set s5 = Comput ((p +* (while>0 (a,I))),s,4);
set s4 = Comput ((p +* (while>0 (a,I))),s,3);
set s3 = Comput ((p +* (while>0 (a,I))),s,2);
set s2 = Comput ((p +* (while>0 (a,I))),s,1);
A14: 2 in dom (while>0 (a,I)) by SCMFSA_9:32;
A15: (p +* (while>0 (a,I))) . 2 = (while>0 (a,I)) . 2 by A14, FUNCT_4:13
.= goto 3 by SCMFSA_9:36 ;
A16: 3 in dom (while>0 (a,I)) by SCMFSA_9:32;
A17: (p +* (while>0 (a,I))) . 3 = (while>0 (a,I)) . 3 by A16, FUNCT_4:13
.= goto ((card I) + 5) by SCMFSA_9:35 ;
A18: (card I) + 5 in dom (while>0 (a,I)) by SCMFSA_9:33;
A19: (p +* (while>0 (a,I))) . ((card I) + 5) = (while>0 (a,I)) . ((card I) + 5) by A18, A5, GRFUNC_1:2
.= halt SCM+FSA by SCMFSA_9:34 ;
A20: ( ( for c being Int-Location holds (Exec ((goto ((card I) + 5)),(Comput ((p +* (while>0 (a,I))),s,3)))) . c = (Comput ((p +* (while>0 (a,I))),s,3)) . c ) & ( for f being FinSeq-Location holds (Exec ((goto ((card I) + 5)),(Comput ((p +* (while>0 (a,I))),s,3)))) . f = (Comput ((p +* (while>0 (a,I))),s,3)) . f ) ) by SCMFSA_2:69;
A21: ( ( for c being Int-Location holds (Exec ((goto 2),(Comput ((p +* (while>0 (a,I))),s,1)))) . c = (Comput ((p +* (while>0 (a,I))),s,1)) . c ) & ( for f being FinSeq-Location holds (Exec ((goto 2),(Comput ((p +* (while>0 (a,I))),s,1)))) . f = (Comput ((p +* (while>0 (a,I))),s,1)) . f ) ) by SCMFSA_2:69;
A22: (p +* (while>0 (a,I))) /. (IC (Comput ((p +* (while>0 (a,I))),s,1))) = (p +* (while>0 (a,I))) . (IC (Comput ((p +* (while>0 (a,I))),s,1))) by PBOOLE:143;
IC (Comput ((p +* (while>0 (a,I))),s,1)) = succ 0 by A3, A10, A13, SCMFSA_2:71
.= 0 + 1 ;
then A23: CurInstr ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),s,1))) = goto 2 by A9, A22;
A24: Comput ((p +* (while>0 (a,I))),s,(1 + 1)) = Following ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),s,1))) by EXTPRO_1:3
.= Exec ((goto 2),(Comput ((p +* (while>0 (a,I))),s,1))) by A23 ;
A25: (p +* (while>0 (a,I))) /. (IC (Comput ((p +* (while>0 (a,I))),s,2))) = (p +* (while>0 (a,I))) . (IC (Comput ((p +* (while>0 (a,I))),s,2))) by PBOOLE:143;
IC (Comput ((p +* (while>0 (a,I))),s,2)) = 2 by A24, SCMFSA_2:69;
then A26: CurInstr ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),s,2))) = goto 3 by A15, A25;
A27: Comput ((p +* (while>0 (a,I))),s,(2 + 1)) = Following ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),s,2))) by EXTPRO_1:3
.= Exec ((goto 3),(Comput ((p +* (while>0 (a,I))),s,2))) by A26 ;
A28: (p +* (while>0 (a,I))) /. (IC (Comput ((p +* (while>0 (a,I))),s,3))) = (p +* (while>0 (a,I))) . (IC (Comput ((p +* (while>0 (a,I))),s,3))) by PBOOLE:143;
IC (Comput ((p +* (while>0 (a,I))),s,3)) = 3 by A27, SCMFSA_2:69;
then A29: CurInstr ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),s,3))) = goto ((card I) + 5) by A17, A28;
A30: Comput ((p +* (while>0 (a,I))),s,(3 + 1)) = Following ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),s,3))) by EXTPRO_1:3
.= Exec ((goto ((card I) + 5)),(Comput ((p +* (while>0 (a,I))),s,3))) by A29 ;
A31: (p +* (while>0 (a,I))) /. (IC (Comput ((p +* (while>0 (a,I))),s,4))) = (p +* (while>0 (a,I))) . (IC (Comput ((p +* (while>0 (a,I))),s,4))) by PBOOLE:143;
IC (Comput ((p +* (while>0 (a,I))),s,4)) = (card I) + 5 by A30, SCMFSA_2:69;
then A32: CurInstr ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),s,4))) = halt SCM+FSA by A19, A31;
then A33: p +* (while>0 (a,I)) halts_on s by EXTPRO_1:29;
now
let k be Element of NAT ; :: thesis: ( CurInstr (p,(Comput (p,s,k))) = halt SCM+FSA implies not 4 > k )
assume A35: CurInstr (p,(Comput (p,s,k))) = halt SCM+FSA ; :: thesis: not 4 > k
assume 4 > k ; :: thesis: contradiction
then 3 + 1 > k ;
then A36: k <= 3 by NAT_1:13;
per cases ( k = 0 or k = 1 or k = 2 or k = 3 ) by A36, NAT_1:27;
end;
end;
hence A37: LifeSpan (p,s) = 4 by A32, A33, A4, EXTPRO_1:def 15; :: thesis: for k being Element of NAT holds DataPart (Comput (p,s,k)) = DataPart s
A38: ( ( for c being Int-Location holds (Exec ((a >0_goto 4),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((a >0_goto 4),s)) . f = s . f ) ) by SCMFSA_2:71;
then A39: DataPart (Comput (p,s,1)) = DataPart s by A13, A4, SCMFSA6A:7;
then A40: DataPart (Comput (p,s,2)) = DataPart s by A24, A21, A4, SCMFSA6A:7;
A41: ( ( for c being Int-Location holds (Exec ((goto 3),(Comput ((p +* (while>0 (a,I))),s,2)))) . c = (Comput ((p +* (while>0 (a,I))),s,2)) . c ) & ( for f being FinSeq-Location holds (Exec ((goto 3),(Comput ((p +* (while>0 (a,I))),s,2)))) . f = (Comput ((p +* (while>0 (a,I))),s,2)) . f ) ) by SCMFSA_2:69;
then DataPart (Comput (p,s,3)) = DataPart s by A27, A40, A4, SCMFSA6A:7;
then A42: DataPart (Comput (p,s,4)) = DataPart s by A30, A20, A4, SCMFSA6A:7;
let k be Element of NAT ; :: thesis: DataPart (Comput (p,s,k)) = DataPart s
( k <= 3 or 3 < k ) ;
then A43: ( k = 0 or k = 1 or k = 2 or k = 3 or 3 + 1 <= k ) by NAT_1:13, NAT_1:27;
per cases ( k = 0 or k = 1 or k = 2 or k = 3 or 4 <= k ) by A43;
suppose k = 0 ; :: thesis: DataPart (Comput (p,s,k)) = DataPart s
hence DataPart (Comput (p,s,k)) = DataPart s by EXTPRO_1:2; :: thesis: verum
end;
suppose k = 1 ; :: thesis: DataPart (Comput (p,s,k)) = DataPart s
hence DataPart (Comput (p,s,k)) = DataPart s by A13, A38, A4, SCMFSA6A:7; :: thesis: verum
end;
suppose k = 2 ; :: thesis: DataPart (Comput (p,s,k)) = DataPart s
hence DataPart (Comput (p,s,k)) = DataPart s by A24, A21, A39, A4, SCMFSA6A:7; :: thesis: verum
end;
suppose k = 3 ; :: thesis: DataPart (Comput (p,s,k)) = DataPart s
hence DataPart (Comput (p,s,k)) = DataPart s by A27, A41, A40, A4, SCMFSA6A:7; :: thesis: verum
end;
suppose 4 <= k ; :: thesis: DataPart (Comput (p,s,k)) = DataPart s
then CurInstr (p,(Comput (p,s,k))) = halt SCM+FSA by A33, A37, A4, EXTPRO_1:36;
hence DataPart (Comput (p,s,k)) = DataPart s by A37, A42, EXTPRO_1:24; :: thesis: verum
end;
end;