let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA
for a being read-write Int-Location st s . a <= 0 holds
( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s )
let I be Program of SCM+FSA ; :: thesis: for a being read-write Int-Location st s . a <= 0 holds
( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s )
let a be read-write Int-Location ; :: thesis: ( s . a <= 0 implies ( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s ) )
assume A1: s . a <= 0 ; :: thesis: ( while>0 a,I is_halting_on s & while>0 a,I is_closed_on 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);
A2: insloc 0 in dom (while>0 a,I) by Th10;
while>0 a,I c= (while>0 a,I) +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A3: dom (while>0 a,I) c= dom ((while>0 a,I) +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
A4: IC SCM+FSA in dom ((while>0 a,I) +* (Start-At (insloc 0 ))) by SF_MASTR:65;
A5: 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 A4, 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 A2, A3, FUNCT_4:14
.= (while>0 a,I) . (insloc 0 ) by A2, SCMFSA6B:7
.= a >0_goto (insloc 4) by Th11 ;
then A6: CurInstr (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))) = a >0_goto (insloc 4) by A5, AMI_1:def 17;
A7: 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 A6, 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 A8: (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . a = s . a by FUNCT_4:12;
A9: 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 A1, A5, A7, A8, SCMFSA_2:97
.= insloc (0 + 1) ;
A10: insloc 1 in dom (while>0 a,I) by Th10;
(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 A3, A10, FUNCT_4:14
.= (while>0 a,I) . (insloc 1) by A10, SCMFSA6B:7
.= goto (insloc 2) by Th11 ;
then A11: CurInstr (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),1) = goto (insloc 2) by A9, AMI_1:def 17;
A12: 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 A11, AMI_1:def 18 ;
A13: insloc 2 in dom (while>0 a,I) by Th37;
A14: 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 A12, 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 A3, A13, FUNCT_4:14
.= (while>0 a,I) . (insloc 2) by A13, SCMFSA6B:7
.= goto (insloc 3) by Th41 ;
then A15: CurInstr (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),2) = goto (insloc 3) by A14, AMI_1:def 17;
A16: 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 A15, AMI_1:def 18 ;
A17: insloc 3 in dom (while>0 a,I) by Th37;
set loc5 = insloc ((card I) + 5);
A18: 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 A16, 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 A3, A17, FUNCT_4:14
.= (while>0 a,I) . (insloc 3) by A17, SCMFSA6B:7
.= goto (insloc ((card I) + 5)) by Th40 ;
then A19: CurInstr (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),3) = goto (insloc ((card I) + 5)) by A18, AMI_1:def 17;
A20: 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 A19, AMI_1:def 18 ;
A21: insloc ((card I) + 5) in dom (while>0 a,I) by Th38;
A22: 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 A20, 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 A3, A21, FUNCT_4:14
.= (while>0 a,I) . (insloc ((card I) + 5)) by A21, SCMFSA6B:7
.= halt SCM+FSA by Th39 ;
then A23: CurInstr (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),4) = halt SCM+FSA by A22, AMI_1:def 17;
then s +* ((while>0 a,I) +* (Start-At (insloc 0 ))) is halting by AMI_1:def 20;
hence while>0 a,I is_halting_on s by SCMFSA7B:def 8; :: thesis: while>0 a,I is_closed_on s

now

let k be Element of NAT ; :: thesis: IC (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),b₁) in dom (while>0 a,I)
A24: ( k <= 3 or k >= 3 + 1 ) by NAT_1:13;

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

suppose k = 0 ; :: thesis: IC (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),b₁) in dom (while>0 a,I)

hence IC (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),k) in dom (while>0 a,I) by A2, A5, AMI_1:13; :: thesis: verum

end;

suppose k = 1 ; :: thesis: IC (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),b₁) in dom (while>0 a,I)

hence IC (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),k) in dom (while>0 a,I) by A9, Th10; :: thesis: verum

end;

suppose k = 2 ; :: thesis: IC (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),b₁) in dom (while>0 a,I)

hence IC (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),k) in dom (while>0 a,I) by A14, Th37; :: thesis: verum

end;

suppose k = 3 ; :: thesis: IC (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),b₁) in dom (while>0 a,I)

hence IC (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),k) in dom (while>0 a,I) by A18, Th37; :: thesis: verum

end;

suppose k >= 4 ; :: thesis: IC (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),b₁) in dom (while>0 a,I)

hence IC (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),k) in dom (while>0 a,I) by A21, A22, A23, AMI_1:52; :: thesis: verum

end;

end;

end;

hence while>0 a,I is_closed_on s by SCMFSA7B:def 7; :: thesis: verum