let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for a being read-write Int-Location
for I being Program of SCM+FSA st Initialize (while>0 (a,I)) c= s & 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 State of SCM+FSA; :: thesis: for a being read-write Int-Location
for I being Program of SCM+FSA st Initialize (while>0 (a,I)) c= s & 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 st Initialize (while>0 (a,I)) c= s & 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: ( Initialize (while>0 (a,I)) c= s & 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: Initialize (while>0 (a,I)) c= s and
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:79;
set i = a >0_goto 4;
set s1 = s +* (Initialize (while>0 (a,I)));
set p1 = p +* (while>0 (a,I));
A5: while>0 (a,I) c= p +* (while>0 (a,I)) by FUNCT_4:26;
A6: IC in dom (Initialize (while>0 (a,I))) by COMPOS_1:141;
not a in dom (Initialize (while>0 (a,I))) by SCMFSA6B:12;
then A7: (s +* (Initialize (while>0 (a,I)))) . a = s . a by FUNCT_4:12;
A8: 1 in dom (while>0 (a,I)) by SCMFSA_9:10;
A9: (p +* (while>0 (a,I))) . 1 = (p +* (while>0 (a,I))) . 1
.= (while>0 (a,I)) . 1 by A8, FUNCT_4:14
.= (while>0 (a,I)) . 1
.= goto 2 by SCMFSA_9:11 ;
A10: IC (s +* (Initialize (while>0 (a,I)))) = IC (Initialize (while>0 (a,I))) by A6, FUNCT_4:14
.= 0 by COMPOS_1:142 ;
A11: (p +* (while>0 (a,I))) /. (IC (s +* (Initialize (while>0 (a,I))))) = (p +* (while>0 (a,I))) . (IC (s +* (Initialize (while>0 (a,I))))) by PBOOLE:158;
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:14
.= (while>0 (a,I)) . 0
.= a >0_goto 4 by SCMFSA_9:11 ;
then A12: CurInstr ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I))))) = a >0_goto 4 by A10, A11;
A13: Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(0 + 1)) = Following ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),0))) by EXTPRO_1:4
.= Following ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I))))) by EXTPRO_1:3
.= Exec ((a >0_goto 4),(s +* (Initialize (while>0 (a,I))))) by A12 ;
set loc5 = (card I) + 5;
set s5 = Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),4);
set p5 = p +* (while>0 (a,I));
set s4 = Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),3);
set p4 = p +* (while>0 (a,I));
set s3 = Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),2);
set p3 = p +* (while>0 (a,I));
set s2 = Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1);
A14: 2 in dom (while>0 (a,I)) by SCMFSA_9:37;
A15: (p +* (while>0 (a,I))) . 2 = (p +* (while>0 (a,I))) . 2
.= (while>0 (a,I)) . 2 by A14, FUNCT_4:14
.= (while>0 (a,I)) . 2
.= goto 3 by SCMFSA_9:41 ;
A16: 3 in dom (while>0 (a,I)) by SCMFSA_9:37;
A17: (p +* (while>0 (a,I))) . 3 = (p +* (while>0 (a,I))) . 3
.= (while>0 (a,I)) . 3 by A16, FUNCT_4:14
.= (while>0 (a,I)) . 3
.= goto ((card I) + 5) by SCMFSA_9:40 ;
A18: (card I) + 5 in dom (while>0 (a,I)) by SCMFSA_9:38;
A19: (p +* (while>0 (a,I))) . ((card I) + 5) = (p +* (while>0 (a,I))) . ((card I) + 5)
.= (while>0 (a,I)) . ((card I) + 5) by A18, A5, GRFUNC_1:8
.= halt SCM+FSA by SCMFSA_9:39 ;
A20: ( ( for c being Int-Location holds (Exec ((goto ((card I) + 5)),(Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),3)))) . c = (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),3)) . c ) & ( for f being FinSeq-Location holds (Exec ((goto ((card I) + 5)),(Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),3)))) . f = (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),3)) . f ) ) by SCMFSA_2:95;
A21: ( ( for c being Int-Location holds (Exec ((goto 2),(Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1)))) . c = (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1)) . c ) & ( for f being FinSeq-Location holds (Exec ((goto 2),(Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1)))) . f = (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1)) . f ) ) by SCMFSA_2:95;
A22: (p +* (while>0 (a,I))) /. (IC (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1))) = (p +* (while>0 (a,I))) . (IC (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1))) by PBOOLE:158;
IC (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1)) = (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1)) . (IC )
.= succ 0 by A3, A10, A13, A7, SCMFSA_2:97
.= 0 + 1 ;
then A23: CurInstr ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1))) = goto 2 by A9, A22;
A24: Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(1 + 1)) = Following ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1))) by EXTPRO_1:4
.= Exec ((goto 2),(Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1))) by A23 ;
A25: (p +* (while>0 (a,I))) /. (IC (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),2))) = (p +* (while>0 (a,I))) . (IC (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),2))) by PBOOLE:158;
IC (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),2)) = (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),2)) . (IC )
.= 2 by A24, SCMFSA_2:95 ;
then A26: CurInstr ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),2))) = goto 3 by A15, A25;
A27: Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(2 + 1)) = Following ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),2))) by EXTPRO_1:4
.= Exec ((goto 3),(Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),2))) by A26 ;
A28: (p +* (while>0 (a,I))) /. (IC (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),3))) = (p +* (while>0 (a,I))) . (IC (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),3))) by PBOOLE:158;
IC (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),3)) = (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),3)) . (IC )
.= 3 by A27, SCMFSA_2:95 ;
then A29: CurInstr ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),3))) = goto ((card I) + 5) by A17, A28;
A30: Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(3 + 1)) = Following ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),3))) by EXTPRO_1:4
.= Exec ((goto ((card I) + 5)),(Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),3))) by A29 ;
A31: (p +* (while>0 (a,I))) /. (IC (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),4))) = (p +* (while>0 (a,I))) . (IC (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),4))) by PBOOLE:158;
IC (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),4)) = (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),4)) . (IC )
.= (card I) + 5 by A30, SCMFSA_2:95 ;
then A32: CurInstr ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),4))) = halt SCM+FSA by A19, A31;
then A33: p +* (while>0 (a,I)) halts_on s +* (Initialize (while>0 (a,I))) by EXTPRO_1:30;
A34: s = s +* (Initialize (while>0 (a,I))) by A1, FUNCT_4:79;

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:28;

suppose k = 0 ; :: thesis: contradiction

then Comput (p,s,k) = s by EXTPRO_1:3;
hence contradiction by A34, A12, A35, SCMFSA_2:49, SCMFSA_2:124, A4; :: thesis: verum

end;

suppose k = 1 ; :: thesis: contradiction

hence contradiction by A34, A23, A35, SCMFSA_2:47, SCMFSA_2:124, A4; :: thesis: verum

end;

suppose k = 2 ; :: thesis: contradiction

hence contradiction by A34, A26, A35, SCMFSA_2:47, SCMFSA_2:124, A4; :: thesis: verum

end;

suppose k = 3 ; :: thesis: contradiction

hence contradiction by A34, A29, A35, SCMFSA_2:47, SCMFSA_2:124, A4; :: thesis: verum

end;

end;

end;

hence A37: LifeSpan (p,s) = 4 by A34, A32, A33, EXTPRO_1:def 14, A4; :: 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 +* (Initialize (while>0 (a,I)))))) . c = (s +* (Initialize (while>0 (a,I)))) . c ) & ( for f being FinSeq-Location holds (Exec ((a >0_goto 4),(s +* (Initialize (while>0 (a,I)))))) . f = (s +* (Initialize (while>0 (a,I)))) . f ) ) by SCMFSA_2:97;
then A39: DataPart (Comput (p,s,1)) = DataPart s by A34, A13, SCMFSA6A:38, A4;
then A40: DataPart (Comput (p,s,2)) = DataPart s by A34, A24, A21, SCMFSA6A:38, A4;
A41: ( ( for c being Int-Location holds (Exec ((goto 3),(Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),2)))) . c = (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),2)) . c ) & ( for f being FinSeq-Location holds (Exec ((goto 3),(Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),2)))) . f = (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),2)) . f ) ) by SCMFSA_2:95;
then DataPart (Comput (p,s,3)) = DataPart s by A34, A27, A40, SCMFSA6A:38, A4;
then A42: DataPart (Comput (p,s,4)) = DataPart s by A34, A30, A20, SCMFSA6A:38, A4;
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:28;

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:3; :: thesis: verum

end;

suppose k = 1 ; :: thesis: DataPart (Comput (p,s,k)) = DataPart s

hence DataPart (Comput (p,s,k)) = DataPart s by A34, A13, A38, SCMFSA6A:38, A4; :: thesis: verum

end;

suppose k = 2 ; :: thesis: DataPart (Comput (p,s,k)) = DataPart s

hence DataPart (Comput (p,s,k)) = DataPart s by A34, A24, A21, A39, SCMFSA6A:38, A4; :: thesis: verum

end;

suppose k = 3 ; :: thesis: DataPart (Comput (p,s,k)) = DataPart s

hence DataPart (Comput (p,s,k)) = DataPart s by A34, A27, A41, A40, SCMFSA6A:38, A4; :: 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 A34, A33, A37, SCMFSA8A:4, A4;
hence DataPart (Comput (p,s,k)) = DataPart s by A37, A42, EXTPRO_1:24; :: thesis: verum

end;

end;