let s be State of SCM+FSA ; :: thesis:
let I, J be Program of SCM+FSA ; :: thesis:
let a be read-write Int-Location ; :: thesis:
assume A1: s . a <= 0 ; :: thesis:
assume A2: J is_closed_on s ; :: thesis:
assume A3: J is_halting_on s ; :: thesis:
set I1 = I ';' (Stop SCM+FSA );
set JI2 = ((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA );
set s2 = s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )));
set s3 = s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )));
set s4 = Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1;
set s5 = Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),2;
set i = a >0_goto (insloc ((card J) + 3));
A4: (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )) c= s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) by FUNCT_4:26;
A5: s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) is halting by A2, A3, SCMFSA8A:59;
A6: ((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ) is_closed_on s by A2, A3, SCMFSA8A:58;
then A7: ((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ) is_closed_on s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) by Th10;
A8: insloc 0 in dom (if>0 a,I,J) by Lm2;
if>0 a,I,J c= (if>0 a,I,J) +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A9: dom (if>0 a,I,J) c= dom ((if>0 a,I,J) +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
IC SCM+FSA in dom ((if>0 a,I,J) +* (Start-At (insloc 0 ))) by SF_MASTR:65;
then A10: IC (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) = ((if>0 a,I,J) +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by FUNCT_4:14
.= insloc 0 by SF_MASTR:66 ;
A11: (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) . (insloc 0 ) = ((if>0 a,I,J) +* (Start-At (insloc 0 ))) . (insloc 0 ) by A8, A9, FUNCT_4:14
.= (if>0 a,I,J) . (insloc 0 ) by A8, SCMFSA6B:7
.= a >0_goto (insloc ((card J) + 3)) by Lm3 ;
A12: Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),(0 + 1) = Following (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),0 ) by AMI_1:14
.= Following (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) by AMI_1:13
.= Exec (a >0_goto (insloc ((card J) + 3))),(s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) by A10, A11 ;
( not a in dom ((if>0 a,I,J) +* (Start-At (insloc 0 ))) & a in dom s ) by SCMFSA6B:12, SCMFSA_2:66;
then A13: (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) . a <= 0 by A1, FUNCT_4:12;
A14: (if>0 a,I,J) +* (Start-At (insloc 0 )) c= s +* ((if>0 a,I,J) +* (Start-At (insloc 0 ))) by FUNCT_4:26;
if>0 a,I,J c= (if>0 a,I,J) +* (Start-At (insloc 0 )) by SCMFSA8A:9;
then A15: if>0 a,I,J c= s +* ((if>0 a,I,J) +* (Start-At (insloc 0 ))) by A14, XBOOLE_1:1;
A16: if>0 a,I,J = (((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' (I ';' (Stop SCM+FSA )) by SCMFSA6A:67
.= ((a >0_goto (insloc ((card J) + 3))) ';' J) ';' ((Goto (insloc ((card I) + 1))) ';' (I ';' (Stop SCM+FSA ))) by SCMFSA6A:67
.= (a >0_goto (insloc ((card J) + 3))) ';' (J ';' ((Goto (insloc ((card I) + 1))) ';' (I ';' (Stop SCM+FSA )))) by SCMFSA6A:71
.= (a >0_goto (insloc ((card J) + 3))) ';' ((J ';' (Goto (insloc ((card I) + 1)))) ';' (I ';' (Stop SCM+FSA ))) by SCMFSA6A:67
.= (a >0_goto (insloc ((card J) + 3))) ';' (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) by SCMFSA6A:67
.= (Macro (a >0_goto (insloc ((card J) + 3)))) ';' (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) by SCMFSA6A:def 6 ;
then ProgramPart (Relocated (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),(card (Macro (a >0_goto (insloc ((card J) + 3)))))) c= if>0 a,I,J by Lm1;
then ProgramPart (Relocated (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),2) c= if>0 a,I,J by SCMFSA7B:6;
then ProgramPart (Relocated (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),2) c= s +* ((if>0 a,I,J) +* (Start-At (insloc 0 ))) by A15, XBOOLE_1:1;
then ProgramPart [(ProgramPart (Relocated (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),2))] c= Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),2 by AMI_1:99;
then A17: ProgramPart (Relocated (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),2) c= Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),2 by AMI_1:105;
A18: IC (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1) = Next (insloc 0 ) by A10, A12, A13, SCMFSA_2:97
.= insloc (0 + 1) ;
A19: insloc 1 in dom (if>0 a,I,J) by Lm2;
A20: (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1) . (insloc 1) = (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) . (insloc 1) by AMI_1:54
.= ((if>0 a,I,J) +* (Start-At (insloc 0 ))) . (insloc 1) by A9, A19, FUNCT_4:14
.= (if>0 a,I,J) . (insloc 1) by A19, SCMFSA6B:7
.= goto (insloc 2) by Lm3 ;
A21: Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),(1 + 1) = Following (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1) by AMI_1:14
.= Exec (goto (insloc 2)),(Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1) by A18, A20 ;
then A22: IC (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),2) = insloc 2 by SCMFSA_2:95;
A23: DataPart (s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = DataPart (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) by SCMFSA6A:39, SCMFSA8A:14;

A24: now

let a be Int-Location ; :: thesis:
thus (s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . a = (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) . a by A23, SCMFSA6A:38
.= (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1) . a by A12, SCMFSA_2:97
.= (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),2) . a by A21, SCMFSA_2:95 ; :: thesis:

end;

now

let f be FinSeq-Location ; :: thesis:
thus (s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . f = (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) . f by A23, SCMFSA6A:38
.= (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1) . f by A12, SCMFSA_2:97
.= (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),2) . f by A21, SCMFSA_2:95 ; :: thesis:

end;

then A25: DataPart (s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = DataPart (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),2) by A24, SCMFSA6A:38;
CurInstr (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),((LifeSpan (s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) + 2)) = CurInstr (Computation (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),2),(LifeSpan (s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))))) by AMI_1:51
.= IncAddr (CurInstr (Computation (s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))))),2 by A4, A7, A17, A22, A25, Th11
.= IncAddr (halt SCM+FSA ),2 by A5, AMI_1:def 46
.= halt SCM+FSA by SCMFSA_4:8 ;
then A26: s +* ((if>0 a,I,J) +* (Start-At (insloc 0 ))) is halting by AMI_1:def 20;

now

let k be Element of NAT ; :: thesis:
( k = 0 or 0 + 1 < k + 1 ) by XREAL_1:8;
then A27: ( k = 0 or 1 <= k ) by NAT_1:13;

per cases by A27, XXREAL_0:1;

suppose A28: 1 < k ; :: thesis:

then consider k1 being Nat such that
A29: k1 + 1 = k by NAT_1:6;
0 + 1 < k1 + 1 by A28, A29;
then consider k2 being Nat such that
A30: k2 + 1 = k1 by NAT_1:6;
reconsider k1 = k1, k2 = k2 as Element of NAT by ORDINAL1:def 13;
reconsider m = IC (Computation (s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k2) as Element of NAT by ORDINAL1:def 13;
A32: card (if>0 a,I,J) = (card (Macro (a >0_goto (insloc ((card J) + 3))))) + (card (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ))) by A16, SCMFSA6A:61
.= 2 + (card (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ))) by SCMFSA7B:6 ;
insloc m in dom (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) by A6, SCMFSA7B:def 7;
then m < card (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) by SCMFSA6A:15;
then A33: m + 2 < card (if>0 a,I,J) by A32, XREAL_1:8;
IC (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),k) = IC (Computation (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1),k1) by A29, AMI_1:51
.= IC (Computation (Computation (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1),1),k2) by A30, AMI_1:51
.= IC (Computation (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),(1 + 1)),k2) by AMI_1:51
.= insloc (m + 2) by A4, A7, A17, A22, A25, Th11 ;
hence IC (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (if>0 a,I,J) by A33, SCMFSA6A:15; :: thesis:

end;

suppose k = 0 ; :: thesis:

hence IC (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (if>0 a,I,J) by A8, A10, AMI_1:13; :: thesis:

end;

suppose k = 1 ; :: thesis:

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

end;

hence if>0 a,I,J is_closed_on s by SCMFSA7B:def 7; :: thesis:
thus if>0 a,I,J is_halting_on s by A26, SCMFSA7B:def 8; :: thesis: