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