let s be State of ; :: thesis: for I, J being Program of
for a being read-write Int-Location st s . a <= 0 & J is_closed_on s & J is_halting_on s holds
( if>0 a,I,J is_closed_on s & if>0 a,I,J is_halting_on s )
let I, J be Program of ; :: thesis: for a being read-write Int-Location st s . a <= 0 & J is_closed_on s & J is_halting_on s holds
( if>0 a,I,J is_closed_on s & if>0 a,I,J is_halting_on s )
let a be read-write Int-Location ; :: thesis: ( s . a <= 0 & J is_closed_on s & J is_halting_on s implies ( if>0 a,I,J is_closed_on s & if>0 a,I,J is_halting_on s ) )
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));
A1: (((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;
IC SCM+FSA in dom ((if>0 a,I,J) +* (Start-At (insloc 0 ))) by SF_MASTR:65;
then A2: 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 ;
A3: if>0 a,I,J c= (if>0 a,I,J) +* (Start-At (insloc 0 )) by SCMFSA8A:9;
(if>0 a,I,J) +* (Start-At (insloc 0 )) c= s +* ((if>0 a,I,J) +* (Start-At (insloc 0 ))) by FUNCT_4:26;
then A4: if>0 a,I,J c= s +* ((if>0 a,I,J) +* (Start-At (insloc 0 ))) by A3, XBOOLE_1:1;
A5: 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 A4, 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 A6: 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;
A7: not a in dom ((if>0 a,I,J) +* (Start-At (insloc 0 ))) by SCMFSA6B:12;
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;
then A10: (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, FUNCT_4:14
.= (if>0 a,I,J) . (insloc 0 ) by A8, SCMFSA6B:7
.= a >0_goto (insloc ((card J) + 3)) by Lm3 ;
A11: insloc 1 in dom (if>0 a,I,J) by Lm2;
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 A2, A10 ;
assume s . a <= 0 ; :: thesis: ( not J is_closed_on s or not J is_halting_on s or ( if>0 a,I,J is_closed_on s & if>0 a,I,J is_halting_on s ) )
then (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) . a <= 0 by A7, FUNCT_4:12;
then A13: IC (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1) = Next (insloc 0 ) by A2, A12, SCMFSA_2:97
.= insloc (0 + 1) ;
A14: (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, A11, FUNCT_4:14
.= (if>0 a,I,J) . (insloc 1) by A11, SCMFSA6B:7
.= goto (insloc 2) by Lm3 ;
assume A15: J is_closed_on s ; :: thesis: ( not J is_halting_on s or ( if>0 a,I,J is_closed_on s & if>0 a,I,J is_halting_on s ) )
A16: 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 A13, A14 ;
A17: 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;

A18: now

let f be FinSeq-Location ; :: thesis: (s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . f = (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),2) . f
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 A17, 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 A16, SCMFSA_2:95 ; :: thesis: verum

end;

now

let a be Int-Location ; :: thesis: (s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . a = (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),2) . a
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 A17, 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 A16, SCMFSA_2:95 ; :: thesis: verum

end;

then A19: 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 A18, SCMFSA6A:38;
assume A20: J is_halting_on s ; :: thesis: ( if>0 a,I,J is_closed_on s & if>0 a,I,J is_halting_on s )
then A21: ((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ) is_closed_on s by A15, SCMFSA8A:58;
then A22: ((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;
A23: ProgramPart (s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) halts_on s +* ((((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) by A15, A20, SCMFSA8A:59;
A24: IC (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),2) = insloc 2 by A16, SCMFSA_2:95;

now

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

per cases ( 1 < k or k = 0 or k = 1 ) by A25, XXREAL_0:1;

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

then consider k1 being Nat such that
A27: k1 + 1 = k by NAT_1:6;
0 + 1 < k1 + 1 by A26, A27;
then consider k2 being Nat such that
A28: 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;
A29: 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 A5, 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 A21, SCMFSA7B:def 7;
then m < card (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )) by SCMFSA6A:15;
then A30: m + 2 < card (if>0 a,I,J) by A29, 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 A27, AMI_1:51
.= IC (Computation (Computation (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),1),1),k2) by A28, 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 A1, A22, A6, A24, A19, Th11 ;
hence IC (Computation (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (if>0 a,I,J) by A30, SCMFSA6A:15; :: thesis: verum

end;

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

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

end;

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

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

end;

end;

end;

hence if>0 a,I,J is_closed_on s by SCMFSA7B:def 7; :: thesis: if>0 a,I,J is_halting_on s
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 A1, A22, A6, A24, A19, Th11
.= IncAddr (halt SCM+FSA ),2 by A23, AMI_1:def 46
.= halt SCM+FSA by SCMFSA_4:8 ;
then ProgramPart (s +* ((if>0 a,I,J) +* (Start-At (insloc 0 )))) halts_on s +* ((if>0 a,I,J) +* (Start-At (insloc 0 ))) by AMI_1:146;
hence if>0 a,I,J is_halting_on s by SCMFSA7B:def 8; :: thesis: verum