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: J is_closed_on Initialize s ; :: thesis:
assume A3: J is_halting_on Initialize s ; :: thesis:
set I1 = I ';' (Stop SCM+FSA );
set JI2 = ((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA );
set s2 = s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' 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 s5 = Computation (s +* (Initialized (if=0 a,I,J))),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 +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ))) by FUNCT_4:26, SCMFSA6B:8;
A5: s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ))) is halting by A2, A3, SCMFSA8A:60;
((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ) is_closed_on Initialize s by A2, A3, SCMFSA8A:58;
then A6: ((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ) is_closed_on s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' 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: dom (s | NAT ) = (dom s) /\ NAT by RELAT_1:90
.= (((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT ) /\ NAT by SCMFSA6A:34
.= NAT by XBOOLE_1:21 ;
( not a in dom (Initialized (if=0 a,I,J)) & a in dom s ) by SCMFSA6A:48, SCMFSA_2:66;
then A13: (s +* (Initialized (if=0 a,I,J))) . a <> 0 by A1, FUNCT_4:12;
A14: 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 A15: if=0 a,I,J c= s +* (Initialized (if=0 a,I,J)) by A14, 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
.= ((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 +* (Initialized (if=0 a,I,J)) by A15, XBOOLE_1:1;
then ProgramPart [(ProgramPart (Relocated (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),2))] c= Computation (s +* (Initialized (if=0 a,I,J))),2 by AMI_1:99;
then A16: ProgramPart (Relocated (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),2) c= Computation (s +* (Initialized (if=0 a,I,J))),2 by AMI_1:105;
A17: IC (Computation (s +* (Initialized (if=0 a,I,J))),1) = Next (insloc 0 ) by A9, A11, A13, SCMFSA_2:96
.= insloc (0 + 1) ;
A18: insloc 1 in dom (if=0 a,I,J) by Lm2;
A19: (Computation (s +* (Initialized (if=0 a,I,J))),1) . (insloc 1) = (s +* (Initialized (if=0 a,I,J))) . (insloc 1) by AMI_1:54
.= (Initialized (if=0 a,I,J)) . (insloc 1) by A8, A18, FUNCT_4:14
.= (if=0 a,I,J) . (insloc 1) by A18, SCMFSA6A:50
.= goto (insloc 2) by Lm3 ;
A20: Computation (s +* (Initialized (if=0 a,I,J))),(1 + 1) = Following (Computation (s +* (Initialized (if=0 a,I,J))),1) by AMI_1:14
.= Exec (goto (insloc 2)),(Computation (s +* (Initialized (if=0 a,I,J))),1) by A17, A19 ;
then A21: IC (Computation (s +* (Initialized (if=0 a,I,J))),2) = insloc 2 by SCMFSA_2:95;
A22: DataPart (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )))) = DataPart (s +* (Initialized (if=0 a,I,J))) by SCMFSA6A:39, SCMFSA6A:53;

A23: now

let a be Int-Location ; :: thesis:
thus (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )))) . a = (s +* (Initialized (if=0 a,I,J))) . a by A22, SCMFSA6A:38
.= (Computation (s +* (Initialized (if=0 a,I,J))),1) . a by A11, SCMFSA_2:96
.= (Computation (s +* (Initialized (if=0 a,I,J))),2) . a by A20, SCMFSA_2:95 ; :: thesis:

end;

now

let f be FinSeq-Location ; :: thesis:
thus (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )))) . f = (s +* (Initialized (if=0 a,I,J))) . f by A22, SCMFSA6A:38
.= (Computation (s +* (Initialized (if=0 a,I,J))),1) . f by A11, SCMFSA_2:96
.= (Computation (s +* (Initialized (if=0 a,I,J))),2) . f by A20, SCMFSA_2:95 ; :: thesis:

end;

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

now

let l be Element of NAT ; :: thesis:
assume A27: l < (LifeSpan (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ))))) + 2 ; :: 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:48, SCMFSA_2:124; :: thesis:

end;

suppose l = 1 ; :: thesis:

hence CurInstr (Computation (s +* (Initialized (if=0 a,I,J))),l) <> halt SCM+FSA by A17, A19, SCMFSA_2:47, SCMFSA_2:124; :: thesis:

end;

suppose A28: ( l <> 0 & l <> 1 ) ; :: thesis:

then consider n being Nat such that
A29: l = n + 1 by NAT_1:6;
n + 1 < ((LifeSpan (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ))))) + 1) + 1 by A27, A29;
then A30: n < (LifeSpan (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ))))) + 1 by XREAL_1:8;
n <> 0 by A28, A29;
then consider l2 being Nat such that
A31: n = l2 + 1 by NAT_1:6;
reconsider l2 = l2 as Element of NAT by ORDINAL1:def 13;
A32: l2 < LifeSpan (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )))) by A30, A31, XREAL_1:8;
assume A33: CurInstr (Computation (s +* (Initialized (if=0 a,I,J))),l) = halt SCM+FSA ; :: thesis:
InsCode (CurInstr (Computation (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )))),l2)) = InsCode (IncAddr (CurInstr (Computation (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )))),l2)),2) by SCMFSA_4:22
.= InsCode (CurInstr (Computation (Computation (s +* (Initialized (if=0 a,I,J))),2),l2)) by A4, A6, A16, A21, A24, Th11
.= InsCode (CurInstr (Computation (s +* (Initialized (if=0 a,I,J))),(l2 + (1 + 1)))) by AMI_1:51
.= 0 by A29, A31, A33, SCMFSA_2:124 ;
then CurInstr (Computation (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )))),l2) = halt SCM+FSA by SCMFSA_2:122;
hence contradiction by A5, A32, 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 (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ))))) + 2 <= l ;
then A34: LifeSpan (s +* (Initialized (if=0 a,I,J))) = (LifeSpan (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ))))) + 2 by A25, A26, AMI_1:def 46;
A35: DataPart (Result (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ))))) = DataPart (Computation (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )))),(LifeSpan (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )))))) by A2, A3, AMI_1:122, SCMFSA8A:60
.= DataPart (Computation (Computation (s +* (Initialized (if=0 a,I,J))),2),(LifeSpan (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )))))) by A4, A6, A16, A21, A24, Th11
.= DataPart (Computation (s +* (Initialized (if=0 a,I,J))),((LifeSpan (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ))))) + 2)) by AMI_1:51
.= DataPart (Result (s +* (Initialized (if=0 a,I,J)))) by A26, A34, AMI_1:122 ;
A36: dom (IExec (if=0 a,I,J),s) = the carrier of SCM+FSA by AMI_1:79
.= dom ((IExec (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),s) +* (Start-At (insloc (((card I) + (card J)) + 3)))) by AMI_1:79 ;

now

let x be set ; :: thesis:

A37: 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;

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

per cases by A40, SCMFSA6A:35;

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

then x <> IC SCM+FSA by SCMFSA_2:81;
then A43: ( x in dom (IExec (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),s) & not x in dom (Start-At (insloc (((card I) + (card J)) + 3))) ) by A41, A42, 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 A37, A39, A42, FUNCT_4:12, SCMFSA_2:84
.= (Result (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ))))) . x by A35, A42, SCMFSA6A:38
.= (IExec (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),s) . x by A37, A38, A42, FUNCT_4:12, SCMFSA_2:84
.= ((IExec (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),s) +* (Start-At (insloc (((card I) + (card J)) + 3)))) . x by A43, FUNCT_4:12 ; :: thesis:

end;

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

then x <> IC SCM+FSA by SCMFSA_2:82;
then A45: ( x in dom (IExec (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),s) & not x in dom (Start-At (insloc (((card I) + (card J)) + 3))) ) by A41, A44, 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 A37, A39, A44, FUNCT_4:12, SCMFSA_2:85
.= (Result (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ))))) . x by A35, A44, SCMFSA6A:38
.= (IExec (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),s) . x by A37, A38, A44, FUNCT_4:12, SCMFSA_2:85
.= ((IExec (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),s) +* (Start-At (insloc (((card I) + (card J)) + 3)))) . x by A45, FUNCT_4:12 ; :: thesis:

end;

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

then A47: x in dom (Start-At (insloc (((card I) + (card J)) + 3))) by A41, TARSKI:def 1;
A48: IC (Result (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ))))) = IC (IExec (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),s) by A37, A38, A46, AMI_1:48, FUNCT_4:12
.= insloc (((card I) + (card J)) + 1) by A2, A3, SCMFSA8A:61 ;
thus (IExec (if=0 a,I,J),s) . x = (Result (s +* (Initialized (if=0 a,I,J)))) . x by A37, A39, A46, AMI_1:48, FUNCT_4:12
.= (Computation (s +* (Initialized (if=0 a,I,J))),((LifeSpan (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ))))) + 2)) . x by A26, A34, AMI_1:122
.= IC (Computation (Computation (s +* (Initialized (if=0 a,I,J))),2),(LifeSpan (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )))))) by A46, AMI_1:51
.= (IC (Computation (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )))),(LifeSpan (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA ))))))) + 2 by A4, A6, A16, A21, A24, Th11
.= (IC (Result (s +* (Initialized (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )))))) + 2 by A2, A3, AMI_1:122, SCMFSA8A:60
.= (Start-At ((insloc (((card I) + (card J)) + 1)) + 2)) . (IC SCM+FSA ) by A48, FUNCOP_1:87
.= ((IExec (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),s) +* (Start-At (insloc (((card I) + (card J)) + 3)))) . x by A46, A47, FUNCT_4:14 ; :: thesis:

end;

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

then x <> IC SCM+FSA by AMI_1:48;
then A50: ( x in dom (IExec (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),s) & not x in dom (Start-At (insloc (((card I) + (card J)) + 3))) ) by A41, A49, Th2, TARSKI:def 1;
A51: x in NAT by A49, AMI_1:def 4;
hence (IExec (if=0 a,I,J),s) . x = (s | NAT ) . x by A12, A39, FUNCT_4:14
.= (IExec (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),s) . x by A12, A38, A51, FUNCT_4:14
.= ((IExec (((J ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )),s) +* (Start-At (insloc (((card I) + (card J)) + 3)))) . x by A50, FUNCT_4:12 ;
:: thesis:

end;

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