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 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 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 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 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 SF_MASTR:65;
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 ))) = (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) . (IC SCM+FSA ) by AMI_1:def 15
.= ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )) . (IC SCM+FSA ) by A3, FUNCT_4:14
.= 0 by SF_MASTR:66 ;
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 AMI_1:150;
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, AMI_1:def 16;
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 AMI_1:14
.= Following (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) by AMI_1:13
.= Exec (a >0_goto 4),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))) by A10, AMI_1:def 18 ;
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 AMI_1:150;
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 ) by AMI_1:def 15
.= 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, AMI_1:def 16;
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:144;
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 AMI_1:14
.= 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, AMI_1:def 18 ;
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 AMI_1:150;
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 ) by AMI_1:def 15
.= 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, AMI_1:def 16;
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:144;
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 AMI_1:14
.= 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, AMI_1:def 18 ;
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 AMI_1:150;
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 ) by AMI_1:def 15
.= 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, AMI_1:def 16;
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:144;
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 AMI_1:14
.= 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, AMI_1:def 18 ;
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 AMI_1:150;
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 ) by AMI_1:def 15
.= (card I) + 5 by A25, SCMFSA_2:95 ;
then A26: CurInstr (ProgramPart (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) = halt SCM+FSA by A17, Y, AMI_1:def 16;
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 AMI_1:146;
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 (Comput (ProgramPart s),s,k)),(Comput (ProgramPart s),s,k) = halt SCM+FSA implies not 4 > k )
assume A29: CurInstr (ProgramPart (Comput (ProgramPart s),s,k)),(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;
end;
end;
hence A31: LifeSpan s = 4 by A28, A26, A27, AMI_1:def 46; :: 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 AMI_1:13; :: 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 (Comput (ProgramPart s),s,k)),(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, AMI_1:127; :: thesis: verum
end;
end;