let I, J be Program of SCM+FSA ; :: thesis:
let a be read-write Int-Location ; :: thesis:
let s be State of SCM+FSA ; :: thesis:
assume A1: s . a > 0 ; :: thesis:
assume A2: I is_closed_on Initialize s ; :: thesis:
assume A3: I is_halting_on Initialize s ; :: thesis:
set I1 = I ';' (Stop SCM+FSA );
set s1 = s +* (Initialized (I ';' (Stop SCM+FSA )));
set s3 = s +* (Initialized (if>0 a,I,J));
set s4 = Computation (s +* (Initialized (if>0 a,I,J))),1;
set i = a >0_goto (insloc ((card J) + 3));
A4: (I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )) c= s +* (Initialized (I ';' (Stop SCM+FSA ))) by FUNCT_4:26, SCMFSA6B:8;
A5: s +* (Initialized (I ';' (Stop SCM+FSA ))) is halting by A2, A3, SCMFSA8A:55;
I ';' (Stop SCM+FSA ) is_closed_on Initialize s by A2, A3, SCMFSA8A:46;
then A6: I ';' (Stop SCM+FSA ) is_closed_on s +* (Initialized (I ';' (Stop SCM+FSA ))) by Th9;
A7: insloc 0 in dom (if>0 a,I,J) by Lm2;
if>0 a,I,J c= Initialized (if>0 a,I,J) by SCMFSA6A:26;
then A8: dom (if>0 a,I,J) c= dom (Initialized (if>0 a,I,J)) by GRFUNC_1:8;
IC SCM+FSA in dom (Initialized (if>0 a,I,J)) by SCMFSA6A:24;
then A9: IC (s +* (Initialized (if>0 a,I,J))) = (Initialized (if>0 a,I,J)) . (IC SCM+FSA ) by FUNCT_4:14
.= insloc 0 by SCMFSA6A:46 ;
A10: (s +* (Initialized (if>0 a,I,J))) . (insloc 0 ) = (Initialized (if>0 a,I,J)) . (insloc 0 ) by A7, A8, FUNCT_4:14
.= (if>0 a,I,J) . (insloc 0 ) by A7, SCMFSA6A:50
.= a >0_goto (insloc ((card J) + 3)) by Lm3 ;
A11: Computation (s +* (Initialized (if>0 a,I,J))),(0 + 1) = Following (Computation (s +* (Initialized (if>0 a,I,J))),0 ) by AMI_1:14
.= Following (s +* (Initialized (if>0 a,I,J))) by AMI_1:13
.= Exec (a >0_goto (insloc ((card J) + 3))),(s +* (Initialized (if>0 a,I,J))) by A9, A10 ;
A12: card (((a >0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) = card (((Macro (a >0_goto (insloc ((card J) + 3)))) ';' J) ';' (Goto (insloc ((card I) + 1)))) by SCMFSA6A:def 6
.= (card ((Macro (a >0_goto (insloc ((card J) + 3)))) ';' J)) + (card (Goto (insloc ((card I) + 1)))) by SCMFSA6A:61
.= (card ((Macro (a >0_goto (insloc ((card J) + 3)))) ';' J)) + 1 by SCMFSA8A:29
.= ((card (Macro (a >0_goto (insloc ((card J) + 3))))) + (card J)) + 1 by SCMFSA6A:61
.= ((card J) + 2) + 1 by SCMFSA7B:6
.= (card J) + (2 + 1) ;
A13: dom (s | NAT ) = NAT by SCMFSA8A:3;
( not a in dom (Initialized (if>0 a,I,J)) & a in dom s ) by SCMFSA6A:48, SCMFSA_2:66;
then A14: (s +* (Initialized (if>0 a,I,J))) . a > 0 by A1, FUNCT_4:12;
A15: Initialized (if>0 a,I,J) c= s +* (Initialized (if>0 a,I,J)) by FUNCT_4:26;
if>0 a,I,J c= Initialized (if>0 a,I,J) by SCMFSA6A:26;
then A16: if>0 a,I,J c= s +* (Initialized (if>0 a,I,J)) by A15, XBOOLE_1:1;
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;
then ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= if>0 a,I,J by A12, Lm1;
then ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= s +* (Initialized (if>0 a,I,J)) by A16, XBOOLE_1:1;
then ProgramPart [(ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)))] c= Computation (s +* (Initialized (if>0 a,I,J))),1 by AMI_1:99;
then A17: ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= Computation (s +* (Initialized (if>0 a,I,J))),1 by AMI_1:105;
A18: IC (Computation (s +* (Initialized (if>0 a,I,J))),1) = insloc ((card J) + 3) by A11, A14, SCMFSA_2:97;
A19: DataPart (s +* (Initialized (I ';' (Stop SCM+FSA )))) = DataPart (s +* (Initialized (if>0 a,I,J))) by SCMFSA6A:39, SCMFSA6A:53;

A20: now

let a be Int-Location ; :: thesis:
thus (s +* (Initialized (I ';' (Stop SCM+FSA )))) . a = (s +* (Initialized (if>0 a,I,J))) . a by A19, SCMFSA6A:38
.= (Computation (s +* (Initialized (if>0 a,I,J))),1) . a by A11, SCMFSA_2:97 ; :: thesis:

end;

now

let f be FinSeq-Location ; :: thesis:
thus (s +* (Initialized (I ';' (Stop SCM+FSA )))) . f = (s +* (Initialized (if>0 a,I,J))) . f by A19, SCMFSA6A:38
.= (Computation (s +* (Initialized (if>0 a,I,J))),1) . f by A11, SCMFSA_2:97 ; :: thesis:

end;

then A21: DataPart (s +* (Initialized (I ';' (Stop SCM+FSA )))) = DataPart (Computation (s +* (Initialized (if>0 a,I,J))),1) by A20, SCMFSA6A:38;
A22: CurInstr (Computation (s +* (Initialized (if>0 a,I,J))),((LifeSpan (s +* (Initialized (I ';' (Stop SCM+FSA ))))) + 1)) = CurInstr (Computation (Computation (s +* (Initialized (if>0 a,I,J))),1),(LifeSpan (s +* (Initialized (I ';' (Stop SCM+FSA )))))) by AMI_1:51
.= IncAddr (CurInstr (Computation (s +* (Initialized (I ';' (Stop SCM+FSA )))),(LifeSpan (s +* (Initialized (I ';' (Stop SCM+FSA ))))))),((card J) + 3) by A4, A6, A17, A18, A21, Th11
.= IncAddr (halt SCM+FSA ),((card J) + 3) by A5, AMI_1:def 46
.= halt SCM+FSA by SCMFSA_4:8 ;
then A23: s +* (Initialized (if>0 a,I,J)) is halting by AMI_1:def 20;

now

let l be Element of NAT ; :: thesis:
assume A24: l < (LifeSpan (s +* (Initialized (I ';' (Stop SCM+FSA ))))) + 1 ; :: thesis:

per cases ;

suppose l = 0 ; :: thesis:

then CurInstr (Computation (s +* (Initialized (if>0 a,I,J))),l) = CurInstr (s +* (Initialized (if>0 a,I,J))) by AMI_1:13;
hence CurInstr (Computation (s +* (Initialized (if>0 a,I,J))),l) <> halt SCM+FSA by A9, A10, SCMFSA_2:49, SCMFSA_2:124; :: thesis:

end;

suppose l <> 0 ; :: thesis:

then consider n being Nat such that
A25: l = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A26: n < LifeSpan (s +* (Initialized (I ';' (Stop SCM+FSA )))) by A24, A25, XREAL_1:8;
assume A27: CurInstr (Computation (s +* (Initialized (if>0 a,I,J))),l) = halt SCM+FSA ; :: thesis:
InsCode (CurInstr (Computation (s +* (Initialized (I ';' (Stop SCM+FSA )))),n)) = InsCode (IncAddr (CurInstr (Computation (s +* (Initialized (I ';' (Stop SCM+FSA )))),n)),((card J) + 3)) by SCMFSA_4:22
.= InsCode (CurInstr (Computation (Computation (s +* (Initialized (if>0 a,I,J))),1),n)) by A4, A6, A17, A18, A21, Th11
.= 0 by A25, A27, AMI_1:51, SCMFSA_2:124 ;
then CurInstr (Computation (s +* (Initialized (I ';' (Stop SCM+FSA )))),n) = halt SCM+FSA by SCMFSA_2:122;
hence contradiction by A5, A26, AMI_1:def 46; :: thesis:

end;

then for l being Element of NAT st CurInstr (Computation (s +* (Initialized (if>0 a,I,J))),l) = halt SCM+FSA holds
(LifeSpan (s +* (Initialized (I ';' (Stop SCM+FSA ))))) + 1 <= l ;
then A28: LifeSpan (s +* (Initialized (if>0 a,I,J))) = (LifeSpan (s +* (Initialized (I ';' (Stop SCM+FSA ))))) + 1 by A22, A23, AMI_1:def 46;
A29: DataPart (Result (s +* (Initialized (I ';' (Stop SCM+FSA ))))) = DataPart (Computation (s +* (Initialized (I ';' (Stop SCM+FSA )))),(LifeSpan (s +* (Initialized (I ';' (Stop SCM+FSA )))))) by A2, A3, AMI_1:122, SCMFSA8A:55
.= DataPart (Computation (Computation (s +* (Initialized (if>0 a,I,J))),1),(LifeSpan (s +* (Initialized (I ';' (Stop SCM+FSA )))))) by A4, A6, A17, A18, A21, Th11
.= DataPart (Computation (s +* (Initialized (if>0 a,I,J))),((LifeSpan (s +* (Initialized (I ';' (Stop SCM+FSA ))))) + 1)) by AMI_1:51
.= DataPart (Result (s +* (Initialized (if>0 a,I,J)))) by A23, A28, AMI_1:122 ;
A30: dom (IExec (if>0 a,I,J),s) = the carrier of SCM+FSA by AMI_1:79
.= dom ((IExec (I ';' (Stop SCM+FSA )),s) +* (Start-At (insloc (((card I) + (card J)) + 3)))) by AMI_1:79 ;

now

let x be set ; :: thesis:

A31: now

assume x in dom (s | NAT ) ; :: thesis:
then x in NAT by RELAT_1:86;
hence x is Instruction-Location of SCM+FSA by AMI_1:def 4; :: thesis:

end;

A32: IExec (I ';' (Stop SCM+FSA )),s = (Result (s +* (Initialized (I ';' (Stop SCM+FSA ))))) +* (s | NAT ) by SCMFSA6B:def 1;
A33: IExec (if>0 a,I,J),s = (Result (s +* (Initialized (if>0 a,I,J)))) +* (s | NAT ) by SCMFSA6B:def 1;
assume A34: x in dom (IExec (if>0 a,I,J),s) ; :: thesis:
A35: dom (Start-At (insloc (((card I) + (card J)) + 3))) = {(IC SCM+FSA )} by FUNCOP_1:19;

per cases by A34, SCMFSA6A:35;

suppose A36: x is Int-Location ; :: thesis:

then x <> IC SCM+FSA by SCMFSA_2:81;
then A37: ( x in dom (IExec (I ';' (Stop SCM+FSA )),s) & not x in dom (Start-At (insloc (((card I) + (card J)) + 3))) ) by A35, A36, SCMFSA_2:66, TARSKI:def 1;
thus (IExec (if>0 a,I,J),s) . x = (Result (s +* (Initialized (if>0 a,I,J)))) . x by A31, A33, A36, FUNCT_4:12, SCMFSA_2:84
.= (Result (s +* (Initialized (I ';' (Stop SCM+FSA ))))) . x by A29, A36, SCMFSA6A:38
.= (IExec (I ';' (Stop SCM+FSA )),s) . x by A31, A32, A36, FUNCT_4:12, SCMFSA_2:84
.= ((IExec (I ';' (Stop SCM+FSA )),s) +* (Start-At (insloc (((card I) + (card J)) + 3)))) . x by A37, FUNCT_4:12 ; :: thesis:

end;

suppose A38: x is FinSeq-Location ; :: thesis:

then x <> IC SCM+FSA by SCMFSA_2:82;
then A39: ( x in dom (IExec (I ';' (Stop SCM+FSA )),s) & not x in dom (Start-At (insloc (((card I) + (card J)) + 3))) ) by A35, A38, SCMFSA_2:67, TARSKI:def 1;
thus (IExec (if>0 a,I,J),s) . x = (Result (s +* (Initialized (if>0 a,I,J)))) . x by A31, A33, A38, FUNCT_4:12, SCMFSA_2:85
.= (Result (s +* (Initialized (I ';' (Stop SCM+FSA ))))) . x by A29, A38, SCMFSA6A:38
.= (IExec (I ';' (Stop SCM+FSA )),s) . x by A31, A32, A38, FUNCT_4:12, SCMFSA_2:85
.= ((IExec (I ';' (Stop SCM+FSA )),s) +* (Start-At (insloc (((card I) + (card J)) + 3)))) . x by A39, FUNCT_4:12 ; :: thesis:

end;

suppose A40: x = IC SCM+FSA ; :: thesis:

then A41: x in dom (Start-At (insloc (((card I) + (card J)) + 3))) by A35, TARSKI:def 1;
A42: IC (Result (s +* (Initialized (I ';' (Stop SCM+FSA ))))) = (IExec (I ';' (Stop SCM+FSA )),s) . (IC SCM+FSA ) by A31, A32, A40, AMI_1:48, FUNCT_4:12
.= IC ((IExec I,s) +* (Start-At (insloc (card I)))) by A2, A3, SCMFSA8A:57
.= insloc (card I) by AMI_1:111 ;
thus (IExec (if>0 a,I,J),s) . x = (Result (s +* (Initialized (if>0 a,I,J)))) . x by A31, A33, A40, AMI_1:48, FUNCT_4:12
.= (Computation (s +* (Initialized (if>0 a,I,J))),((LifeSpan (s +* (Initialized (I ';' (Stop SCM+FSA ))))) + 1)) . x by A23, A28, AMI_1:122
.= IC (Computation (Computation (s +* (Initialized (if>0 a,I,J))),1),(LifeSpan (s +* (Initialized (I ';' (Stop SCM+FSA )))))) by A40, AMI_1:51
.= (IC (Computation (s +* (Initialized (I ';' (Stop SCM+FSA )))),(LifeSpan (s +* (Initialized (I ';' (Stop SCM+FSA ))))))) + ((card J) + 3) by A4, A6, A17, A18, A21, Th11
.= (IC (Result (s +* (Initialized (I ';' (Stop SCM+FSA )))))) + ((card J) + 3) by A2, A3, AMI_1:122, SCMFSA8A:55
.= (Start-At ((insloc (card I)) + ((card J) + 3))) . (IC SCM+FSA ) by A42, FUNCOP_1:87
.= ((IExec (I ';' (Stop SCM+FSA )),s) +* (Start-At (insloc (((card I) + (card J)) + 3)))) . x by A40, A41, FUNCT_4:14 ; :: thesis:

end;

suppose A43: x is Instruction-Location of SCM+FSA ; :: thesis:

then x <> IC SCM+FSA by AMI_1:48;
then A44: ( x in dom (IExec (I ';' (Stop SCM+FSA )),s) & not x in dom (Start-At (insloc (((card I) + (card J)) + 3))) ) by A35, A43, Th2, TARSKI:def 1;
A45: x in NAT by A43, AMI_1:def 4;
hence (IExec (if>0 a,I,J),s) . x = (s | NAT ) . x by A13, A33, FUNCT_4:14
.= (IExec (I ';' (Stop SCM+FSA )),s) . x by A13, A32, A45, FUNCT_4:14
.= ((IExec (I ';' (Stop SCM+FSA )),s) +* (Start-At (insloc (((card I) + (card J)) + 3)))) . x by A44, FUNCT_4:12 ;
:: thesis:

end;

hence IExec (if>0 a,I,J),s = (IExec (I ';' (Stop SCM+FSA )),s) +* (Start-At (insloc (((card I) + (card J)) + 3))) by A30, FUNCT_1:9
.= ((IExec I,s) +* (Start-At (insloc (card I)))) +* (Start-At (insloc (((card I) + (card J)) + 3))) by A2, A3, SCMFSA8A:57
.= (IExec I,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) by AMI_1:141 ;
:: thesis: