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 (insloc 0 )) c= s & s . a <= 0 holds
( LifeSpan s = 4 & ( for k being Element of NAT holds DataPart (Computation 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 (insloc 0 )) c= s & s . a <= 0 holds
( LifeSpan s = 4 & ( for k being Element of NAT holds DataPart (Computation s,k) = DataPart s ) )
let I be Program of SCM+FSA ; :: thesis: ( (while>0 a,I) +* (Start-At (insloc 0 )) c= s & s . a <= 0 implies ( LifeSpan s = 4 & ( for k being Element of NAT holds DataPart (Computation s,k) = DataPart s ) ) )
assume that
A1: (while>0 a,I) +* (Start-At (insloc 0 )) c= s and
A2: s . a <= 0 ; :: thesis: ( LifeSpan s = 4 & ( for k being Element of NAT holds DataPart (Computation s,k) = DataPart s ) )
set i = a >0_goto (insloc 4);
set s1 = s +* ((while>0 a,I) +* (Start-At (insloc 0 )));
A3: IC SCM+FSA in dom ((while>0 a,I) +* (Start-At (insloc 0 ))) by SF_MASTR:65;
while>0 a,I c= (while>0 a,I) +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A4: dom (while>0 a,I) c= dom ((while>0 a,I) +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
not a in dom ((while>0 a,I) +* (Start-At (insloc 0 ))) by SCMFSA6B:12;
then A5: (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . a = s . a by FUNCT_4:12;
A6: insloc 1 in dom (while>0 a,I) by SCMFSA_9:10;
A7: (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1) . (insloc 1) = (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . (insloc 1) by AMI_1:54
.= ((while>0 a,I) +* (Start-At (insloc 0 ))) . (insloc 1) by A4, A6, FUNCT_4:14
.= (while>0 a,I) . (insloc 1) by A6, SCMFSA6B:7
.= goto (insloc 2) by SCMFSA_9:11 ;
A8: IC (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))) = (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . (IC SCM+FSA ) by AMI_1:def 15
.= ((while>0 a,I) +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A3, FUNCT_4:14
.= insloc 0 by SF_MASTR:66 ;
A9: insloc 0 in dom (while>0 a,I) by SCMFSA_9:10;
then (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . (insloc 0 ) = ((while>0 a,I) +* (Start-At (insloc 0 ))) . (insloc 0 ) by A4, FUNCT_4:14
.= (while>0 a,I) . (insloc 0 ) by A9, SCMFSA6B:7
.= a >0_goto (insloc 4) by SCMFSA_9:11 ;
then A10: CurInstr (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))) = a >0_goto (insloc 4) by A8, AMI_1:def 17;
A11: Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(0 + 1) = Following (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),0 ) by AMI_1:14
.= Following (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))) by AMI_1:13
.= Exec (a >0_goto (insloc 4)),(s +* ((while>0 a,I) +* (Start-At (insloc 0 )))) by A10, AMI_1:def 18 ;
set loc5 = insloc ((card I) + 5);
set s5 = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),4;
set s4 = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),3;
set s3 = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),2;
set s2 = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1;
A12: insloc 2 in dom (while>0 a,I) by SCMFSA_9:37;
A13: (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),2) . (insloc 2) = (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . (insloc 2) by AMI_1:54
.= ((while>0 a,I) +* (Start-At (insloc 0 ))) . (insloc 2) by A4, A12, FUNCT_4:14
.= (while>0 a,I) . (insloc 2) by A12, SCMFSA6B:7
.= goto (insloc 3) by SCMFSA_9:41 ;
A14: insloc 3 in dom (while>0 a,I) by SCMFSA_9:37;
A15: (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),3) . (insloc 3) = (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . (insloc 3) by AMI_1:54
.= ((while>0 a,I) +* (Start-At (insloc 0 ))) . (insloc 3) by A4, A14, FUNCT_4:14
.= (while>0 a,I) . (insloc 3) by A14, SCMFSA6B:7
.= goto (insloc ((card I) + 5)) by SCMFSA_9:40 ;
A16: insloc ((card I) + 5) in dom (while>0 a,I) by SCMFSA_9:38;
A17: (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),4) . (insloc ((card I) + 5)) = (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . (insloc ((card I) + 5)) by AMI_1:54
.= ((while>0 a,I) +* (Start-At (insloc 0 ))) . (insloc ((card I) + 5)) by A4, A16, FUNCT_4:14
.= (while>0 a,I) . (insloc ((card I) + 5)) by A16, SCMFSA6B:7
.= halt SCM+FSA by SCMFSA_9:39 ;
A18: ( ( for c being Int-Location holds (Exec (goto (insloc ((card I) + 5))),(Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),3)) . c = (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),3) . c ) & ( for f being FinSeq-Location holds (Exec (goto (insloc ((card I) + 5))),(Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),3)) . f = (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),3) . f ) ) by SCMFSA_2:95;
A19: ( ( for c being Int-Location holds (Exec (goto (insloc 2)),(Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1)) . c = (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1) . c ) & ( for f being FinSeq-Location holds (Exec (goto (insloc 2)),(Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1)) . f = (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1) . f ) ) by SCMFSA_2:95;
IC (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1) = (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1) . (IC SCM+FSA ) by AMI_1:def 15
.= Next (insloc 0 ) by A2, A8, A11, A5, SCMFSA_2:97
.= insloc (0 + 1) ;
then A20: CurInstr (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1) = goto (insloc 2) by A7, AMI_1:def 17;
A21: Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(1 + 1) = Following (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1) by AMI_1:14
.= Exec (goto (insloc 2)),(Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1) by A20, AMI_1:def 18 ;
IC (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),2) = (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),2) . (IC SCM+FSA ) by AMI_1:def 15
.= insloc 2 by A21, SCMFSA_2:95 ;
then A22: CurInstr (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),2) = goto (insloc 3) by A13, AMI_1:def 17;
A23: Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(2 + 1) = Following (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),2) by AMI_1:14
.= Exec (goto (insloc 3)),(Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),2) by A22, AMI_1:def 18 ;
IC (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),3) = (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),3) . (IC SCM+FSA ) by AMI_1:def 15
.= insloc 3 by A23, SCMFSA_2:95 ;
then A24: CurInstr (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),3) = goto (insloc ((card I) + 5)) by A15, AMI_1:def 17;
A25: Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(3 + 1) = Following (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),3) by AMI_1:14
.= Exec (goto (insloc ((card I) + 5))),(Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),3) by A24, AMI_1:def 18 ;
IC (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),4) = (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),4) . (IC SCM+FSA ) by AMI_1:def 15
.= insloc ((card I) + 5) by A25, SCMFSA_2:95 ;
then A26: CurInstr (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),4) = halt SCM+FSA by A17, AMI_1:def 17;
then A27: s +* ((while>0 a,I) +* (Start-At (insloc 0 ))) is halting by AMI_1:def 20;
A28: s = s +* ((while>0 a,I) +* (Start-At (insloc 0 ))) by A1, FUNCT_4:79;

now

let k be Element of NAT ; :: thesis: ( CurInstr (Computation s,k) = halt SCM+FSA implies not 4 > k )
assume A29: CurInstr (Computation 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 Computation s,k = s by AMI_1:13;
hence contradiction by A28, A10, A29, SCMFSA_2:49, SCMFSA_2:124; :: thesis: verum

end;

suppose k = 1 ; :: thesis: contradiction

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

end;

suppose k = 2 ; :: thesis: contradiction

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

end;

suppose k = 3 ; :: thesis: contradiction

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

end;

end;

end;

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

hence DataPart (Computation s,k) = DataPart s by AMI_1:13; :: thesis: verum

end;

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

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

end;

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

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

end;

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

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

end;

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

then CurInstr (Computation s,k) = halt SCM+FSA by A28, A27, A31, SCMFSA8A:4;
hence DataPart (Computation s,k) = DataPart s by A31, A36, AMI_1:127; :: thesis: verum

end;

end;