let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for I being Program of SCM+FSA st (while>0 (a,I)) +* (Start-At (0,SCM+FSA)) c= s & s . a <= 0 holds
( LifeSpan ((ProgramPart s),s) = 4 & ( for k being Element of NAT holds DataPart (Comput ((ProgramPart s),s,k)) = DataPart s ) )
let a be read-write Int-Location ; :: thesis: for I being Program of SCM+FSA st (while>0 (a,I)) +* (Start-At (0,SCM+FSA)) c= s & s . a <= 0 holds
( LifeSpan ((ProgramPart s),s) = 4 & ( for k being Element of NAT holds DataPart (Comput ((ProgramPart s),s,k)) = DataPart s ) )
let I be Program of SCM+FSA; :: thesis: ( (while>0 (a,I)) +* (Start-At (0,SCM+FSA)) c= s & s . a <= 0 implies ( LifeSpan ((ProgramPart s),s) = 4 & ( for k being Element of NAT holds DataPart (Comput ((ProgramPart s),s,k)) = DataPart s ) ) )
assume that
A1: (while>0 (a,I)) +* (Start-At (0,SCM+FSA)) c= s and
A2: s . a <= 0 ; :: thesis: ( LifeSpan ((ProgramPart s),s) = 4 & ( for k being Element of NAT holds DataPart (Comput ((ProgramPart s),s,k)) = DataPart s ) )
set i = a >0_goto 4;
set s1 = s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)));
A3: IC SCM+FSA in dom ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by COMPOS_1:141;
while>0 (a,I) c= (while>0 (a,I)) +* (Start-At (0,SCM+FSA)) by SCMFSA8A:9;
then A4: dom (while>0 (a,I)) c= dom ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by GRFUNC_1:8;
not a in dom ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by SCMFSA6B:12;
then A5: (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . a = s . a by FUNCT_4:12;
A6: 1 in dom (while>0 (a,I)) by SCMFSA_9:10;
A7: (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)) . 1 = (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . 1 by AMI_1:54
.= ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) . 1 by A4, A6, FUNCT_4:14
.= (while>0 (a,I)) . 1 by A6, SCMFSA6B:7
.= goto 2 by SCMFSA_9:11 ;
A8: IC (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = IC ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by A3, FUNCT_4:14
.= 0 by COMPOS_1:142 ;
Y: (ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))) /. (IC (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))) = (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . (IC (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))) by COMPOS_1:38;
A9: 0 in dom (while>0 (a,I)) by SCMFSA_9:10;
then (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . 0 = ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) . 0 by A4, FUNCT_4:14
.= (while>0 (a,I)) . 0 by A9, SCMFSA6B:7
.= a >0_goto 4 by SCMFSA_9:11 ;
then A10: CurInstr ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))) = a >0_goto 4 by A8, Y;
A11: Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(0 + 1)) = Following ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),0))) by EXTPRO_1:4
.= Following ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))) by EXTPRO_1:3
.= Exec ((a >0_goto 4),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))) by A10 ;
set loc5 = (card I) + 5;
set s5 = Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4);
set s4 = Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3);
set s3 = Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2);
set s2 = Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1);
A12: 2 in dom (while>0 (a,I)) by SCMFSA_9:37;
A13: (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2)) . 2 = (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . 2 by AMI_1:54
.= ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) . 2 by A4, A12, FUNCT_4:14
.= (while>0 (a,I)) . 2 by A12, SCMFSA6B:7
.= goto 3 by SCMFSA_9:41 ;
A14: 3 in dom (while>0 (a,I)) by SCMFSA_9:37;
A15: (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3)) . 3 = (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . 3 by AMI_1:54
.= ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) . 3 by A4, A14, FUNCT_4:14
.= (while>0 (a,I)) . 3 by A14, SCMFSA6B:7
.= goto ((card I) + 5) by SCMFSA_9:40 ;
A16: (card I) + 5 in dom (while>0 (a,I)) by SCMFSA_9:38;
A17: (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4)) . ((card I) + 5) = (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . ((card I) + 5) by AMI_1:54
.= ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) . ((card I) + 5) by A4, A16, FUNCT_4:14
.= (while>0 (a,I)) . ((card I) + 5) by A16, SCMFSA6B:7
.= halt SCM+FSA by SCMFSA_9:39 ;
A18: ( ( for c being Int-Location holds (Exec ((goto ((card I) + 5)),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3)))) . c = (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3)) . c ) & ( for f being FinSeq-Location holds (Exec ((goto ((card I) + 5)),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3)))) . f = (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3)) . f ) ) by SCMFSA_2:95;
A19: ( ( for c being Int-Location holds (Exec ((goto 2),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)))) . c = (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)) . c ) & ( for f being FinSeq-Location holds (Exec ((goto 2),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)))) . f = (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)) . f ) ) by SCMFSA_2:95;
Y: (ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1))) /. (IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1))) = (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)) . (IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1))) by COMPOS_1:38;
IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)) = (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)) . (IC SCM+FSA)
.= succ 0 by A2, A8, A11, A5, SCMFSA_2:97
.= 0 + 1 ;
then A20: CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1))),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1))) = goto 2 by A7, Y;
T: ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)) by AMI_1:123;
A21: Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + 1)) = Following ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1))) by EXTPRO_1:4
.= Exec ((goto 2),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1))) by A20, T ;
Y: (ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2))) /. (IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2))) = (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2)) . (IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2))) by COMPOS_1:38;
IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2)) = (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2)) . (IC SCM+FSA)
.= 2 by A21, SCMFSA_2:95 ;
then A22: CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2))),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2))) = goto 3 by A13, Y;
T: ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2)) by AMI_1:123;
A23: Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(2 + 1)) = Following ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2))) by EXTPRO_1:4
.= Exec ((goto 3),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2))) by A22, T ;
Y: (ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))) /. (IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))) = (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3)) . (IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))) by COMPOS_1:38;
IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3)) = (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3)) . (IC SCM+FSA)
.= 3 by A23, SCMFSA_2:95 ;
then A24: CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))) = goto ((card I) + 5) by A15, Y;
T: ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3)) by AMI_1:123;
A25: Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(3 + 1)) = Following ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))) by EXTPRO_1:4
.= Exec ((goto ((card I) + 5)),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))) by A24, T ;
Y: (ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4))) /. (IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4))) = (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4)) . (IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4))) by COMPOS_1:38;
TX: ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4)) by AMI_1:123;
IC (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4)) = (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4)) . (IC SCM+FSA)
.= (card I) + 5 by A25, SCMFSA_2:95 ;
then A26: CurInstr ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4))) = halt SCM+FSA by A17, Y, TX;
then A27: ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) halts_on s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by EXTPRO_1:30;
A28: s = s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by A1, FUNCT_4:79;

now

let k be Element of NAT ; :: thesis: ( CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) = halt SCM+FSA implies not 4 > k )
TX: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,k)) by AMI_1:123;
assume A29: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) = halt SCM+FSA ; :: thesis: not 4 > k
assume 4 > k ; :: thesis: contradiction
then 3 + 1 > k ;
then A30: k <= 3 by NAT_1:13;

per cases ( k = 0 or k = 1 or k = 2 or k = 3 ) by A30, NAT_1:28;

suppose k = 0 ; :: thesis: contradiction

then Comput ((ProgramPart s),s,k) = s by EXTPRO_1:3;
hence contradiction by A28, A10, A29, SCMFSA_2:49; :: thesis: verum

end;

suppose k = 1 ; :: thesis: contradiction

hence contradiction by A28, A20, A29, TX, SCMFSA_2:47; :: thesis: verum

end;

suppose k = 2 ; :: thesis: contradiction

hence contradiction by A28, A22, A29, TX, SCMFSA_2:47; :: thesis: verum

end;

suppose k = 3 ; :: thesis: contradiction

hence contradiction by A28, A24, A29, TX, SCMFSA_2:47; :: thesis: verum

end;

end;

end;

hence A31: LifeSpan ((ProgramPart s),s) = 4 by A28, A26, A27, EXTPRO_1:def 14; :: thesis: for k being Element of NAT holds DataPart (Comput ((ProgramPart s),s,k)) = DataPart s
A32: ( ( for c being Int-Location holds (Exec ((a >0_goto 4),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))))) . c = (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . c ) & ( for f being FinSeq-Location holds (Exec ((a >0_goto 4),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))))) . f = (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . f ) ) by SCMFSA_2:97;
then A33: DataPart (Comput ((ProgramPart s),s,1)) = DataPart s by A28, A11, SCMFSA6A:38;
then A34: DataPart (Comput ((ProgramPart s),s,2)) = DataPart s by A28, A21, A19, SCMFSA6A:38;
A35: ( ( for c being Int-Location holds (Exec ((goto 3),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2)))) . c = (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2)) . c ) & ( for f being FinSeq-Location holds (Exec ((goto 3),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2)))) . f = (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2)) . f ) ) by SCMFSA_2:95;
then DataPart (Comput ((ProgramPart s),s,3)) = DataPart s by A28, A23, A34, SCMFSA6A:38;
then A36: DataPart (Comput ((ProgramPart s),s,4)) = DataPart s by A28, A25, A18, SCMFSA6A:38;
let k be Element of NAT ; :: thesis: DataPart (Comput ((ProgramPart s),s,k)) = DataPart s
( k <= 3 or 3 < k ) ;
then A37: ( 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 A37;

suppose k = 0 ; :: thesis: DataPart (Comput ((ProgramPart s),s,k)) = DataPart s

hence DataPart (Comput ((ProgramPart s),s,k)) = DataPart s by EXTPRO_1:3; :: thesis: verum

end;

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

hence DataPart (Comput ((ProgramPart s),s,k)) = DataPart s by A28, A11, A32, SCMFSA6A:38; :: thesis: verum

end;

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

hence DataPart (Comput ((ProgramPart s),s,k)) = DataPart s by A28, A21, A19, A33, SCMFSA6A:38; :: thesis: verum

end;

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

hence DataPart (Comput ((ProgramPart s),s,k)) = DataPart s by A28, A23, A35, A34, SCMFSA6A:38; :: thesis: verum

end;

suppose 4 <= k ; :: thesis: DataPart (Comput ((ProgramPart s),s,k)) = DataPart s

then CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,k))) = halt SCM+FSA by A28, A27, A31, SCMFSA8A:4;
hence DataPart (Comput ((ProgramPart s),s,k)) = DataPart s by A31, A36, EXTPRO_1:24; :: thesis: verum

end;

end;