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 s1 = s +* ((while=0 a,I) +* (Start-At (insloc 0 )));
set s2 = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),1;
set s3 = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),2;
set s4 = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),3;
set s5 = Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),4;
set i = a =0_goto (insloc 4);
A3: s = s +* ((while=0 a,I) +* (Start-At (insloc 0 ))) by A1, FUNCT_4:79;
A4: insloc 0 in dom (while=0 a,I) by SCMFSA_9:10;
while=0 a,I c= (while=0 a,I) +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A5: dom (while=0 a,I) c= dom ((while=0 a,I) +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
A6: IC SCM+FSA in dom ((while=0 a,I) +* (Start-At (insloc 0 ))) by SF_MASTR:65;
A7: 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 A6, FUNCT_4:14
.= insloc 0 by SF_MASTR:66 ;
(s +* ((while=0 a,I) +* (Start-At (insloc 0 )))) . (insloc 0 ) = ((while=0 a,I) +* (Start-At (insloc 0 ))) . (insloc 0 ) by A4, A5, FUNCT_4:14
.= (while=0 a,I) . (insloc 0 ) by A4, SCMFSA6B:7
.= a =0_goto (insloc 4) by SCMFSA_9:11 ;
then A8: CurInstr (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))) = a =0_goto (insloc 4) by A7, AMI_1:def 17;
A9: 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 A8, AMI_1:def 18 ;
( not a in dom ((while=0 a,I) +* (Start-At (insloc 0 ))) & a in dom s ) by SCMFSA6B:12, SCMFSA_2:66;
then A10: (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))) . a = s . a by FUNCT_4:12;
A11: 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, A7, A9, A10, SCMFSA_2:96
.= insloc (0 + 1) ;
A12: insloc 1 in dom (while=0 a,I) by SCMFSA_9:10;
(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 A5, A12, FUNCT_4:14
.= (while=0 a,I) . (insloc 1) by A12, SCMFSA6B:7
.= goto (insloc 2) by SCMFSA_9:11 ;
then A13: CurInstr (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),1) = goto (insloc 2) by A11, AMI_1:def 17;
A14: 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 A13, AMI_1:def 18 ;
A15: insloc 2 in dom (while=0 a,I) by SCMFSA_9:12;
A16: 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 A14, SCMFSA_2:95 ;
(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 A5, A15, FUNCT_4:14
.= (while=0 a,I) . (insloc 2) by A15, SCMFSA6B:7
.= goto (insloc 3) by SCMFSA_9:16 ;
then A17: CurInstr (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),2) = goto (insloc 3) by A16, AMI_1:def 17;
A18: 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 A17, AMI_1:def 18 ;
A19: insloc 3 in dom (while=0 a,I) by SCMFSA_9:12;
set loc5 = insloc ((card I) + 5);
A20: 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 A18, SCMFSA_2:95 ;
(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 A5, A19, FUNCT_4:14
.= (while=0 a,I) . (insloc 3) by A19, SCMFSA6B:7
.= goto (insloc ((card I) + 5)) by SCMFSA_9:15 ;
then A21: CurInstr (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),3) = goto (insloc ((card I) + 5)) by A20, AMI_1:def 17;
A22: 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 A21, AMI_1:def 18 ;
A23: insloc ((card I) + 5) in dom (while=0 a,I) by SCMFSA_9:13;
A24: 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 A22, SCMFSA_2:95 ;
(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 A5, A23, FUNCT_4:14
.= (while=0 a,I) . (insloc ((card I) + 5)) by A23, SCMFSA6B:7
.= halt SCM+FSA by SCMFSA_9:14 ;
then A25: CurInstr (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),4) = halt SCM+FSA by A24, AMI_1:def 17;
then A26: s +* ((while=0 a,I) +* (Start-At (insloc 0 ))) is halting by AMI_1:def 20;

now

let k be Element of NAT ; :: thesis: ( CurInstr (Computation s,k) = halt SCM+FSA implies not 4 > k )
assume A27: CurInstr (Computation s,k) = halt SCM+FSA ; :: thesis: not 4 > k
assume 4 > k ; :: thesis: contradiction
then 3 + 1 > k ;
then A28: k <= 3 by NAT_1:13;

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

suppose k = 0 ; :: thesis: contradiction

then Computation s,k = s by AMI_1:13;
hence contradiction by A3, A8, A27, SCMFSA_2:48, SCMFSA_2:124; :: thesis: verum

end;

suppose k = 1 ; :: thesis: contradiction

hence contradiction by A3, A13, A27, SCMFSA_2:47, SCMFSA_2:124; :: thesis: verum

end;

suppose k = 2 ; :: thesis: contradiction

hence contradiction by A3, A17, A27, SCMFSA_2:47, SCMFSA_2:124; :: thesis: verum

end;

suppose k = 3 ; :: thesis: contradiction

hence contradiction by A3, A21, A27, SCMFSA_2:47, SCMFSA_2:124; :: thesis: verum

end;

end;

end;

hence A29: LifeSpan s = 4 by A3, A25, A26, AMI_1:def 46; :: thesis: for k being Element of NAT holds DataPart (Computation s,k) = DataPart s
A30: ( ( 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;
A31: ( ( 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;
A32: ( ( 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;
A33: ( ( 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:96;
then A34: DataPart (Computation s,1) = DataPart s by A3, A9, SCMFSA6A:38;
then A35: DataPart (Computation s,2) = DataPart s by A3, A14, A32, SCMFSA6A:38;
then DataPart (Computation s,3) = DataPart s by A3, A18, A31, SCMFSA6A:38;
then A36: DataPart (Computation s,4) = DataPart s by A3, A22, A30, 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 A3, A9, A33, SCMFSA6A:38; :: thesis: verum

end;

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

hence DataPart (Computation s,k) = DataPart s by A3, A14, A32, A34, SCMFSA6A:38; :: thesis: verum

end;

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

hence DataPart (Computation s,k) = DataPart s by A3, A18, A31, A35, SCMFSA6A:38; :: thesis: verum

end;

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

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

end;

end;