let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being really-closed MacroInstruction of SCM+FSA
for J being MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a = 0 & I is_halting_on Initialized s,P holds
IExec ((if=0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
let s be State of SCM+FSA; :: thesis: for I being really-closed MacroInstruction of SCM+FSA
for J being MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a = 0 & I is_halting_on Initialized s,P holds
IExec ((if=0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
let I be really-closed MacroInstruction of SCM+FSA ; :: thesis: for J being MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a = 0 & I is_halting_on Initialized s,P holds
IExec ((if=0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
let J be MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location st s . a = 0 & I is_halting_on Initialized s,P holds
IExec ((if=0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
let a be read-write Int-Location; :: thesis: ( s . a = 0 & I is_halting_on Initialized s,P implies IExec ((if=0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
set I1 = I ";" (Stop SCM+FSA);
set s1 = Initialized s;
set P1 = P +* (I ";" (Stop SCM+FSA));
set P3 = P +* (if=0 (a,I,J));
A1: I ";" (Stop SCM+FSA) c= P +* (I ";" (Stop SCM+FSA)) by FUNCT_4:25;
set s4 = Comput ((P +* (if=0 (a,I,J))),(Initialized s),1);
set i = a =0_goto ((card J) + 3);
A2: if=0 (a,I,J) = (((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" (I ";" (Stop SCM+FSA)) by SCMFSA6A:25;
A3: 0 in dom (if=0 (a,I,J)) by AFINSQ_1:65;
A4: (P +* (if=0 (a,I,J))) . 0 = (if=0 (a,I,J)) . 0 by A3, FUNCT_4:13
.= a =0_goto ((card J) + 3) by Lm2 ;
A5: dom (Initialize ((intloc 0) .--> 1)) = {(intloc 0),(IC )} by SCMFSA_M:11;
( a <> intloc 0 & a <> IC ) by SCMFSA_2:56;
then A6: not a in dom (Initialize ((intloc 0) .--> 1)) by A5, TARSKI:def 2;
IC in dom (Initialize ((intloc 0) .--> 1)) by MEMSTR_0:48;
then A7: IC (Initialized s) = IC (Initialize ((intloc 0) .--> 1)) by FUNCT_4:13
.= 0 by MEMSTR_0:def 11 ;
A8: Comput ((P +* (if=0 (a,I,J))),(Initialized s),(0 + 1)) = Following ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),0))) by EXTPRO_1:3
.= Following ((P +* (if=0 (a,I,J))),(Initialized s))
.= Exec ((a =0_goto ((card J) + 3)),(Initialized s)) by A7, A4, PBOOLE:143 ;
A9: if=0 (a,I,J) c= P +* (if=0 (a,I,J)) by FUNCT_4:25;
assume s . a = 0 ; :: thesis: ( not I is_halting_on Initialized s,P or IExec ((if=0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) )
then (Initialized s) . a = 0 by A6, FUNCT_4:11;
then A10: IC (Comput ((P +* (if=0 (a,I,J))),(Initialized s),1)) = (card J) + 3 by A8, SCMFSA_2:70;
A11: for f being FinSeq-Location holds (Initialized s) . f = (Comput ((P +* (if=0 (a,I,J))),(Initialized s),1)) . f by A8, SCMFSA_2:70;
for a being Int-Location holds (Initialized s) . a = (Comput ((P +* (if=0 (a,I,J))),(Initialized s),1)) . a by A8, SCMFSA_2:70;
then A12: DataPart (Initialized s) = DataPart (Comput ((P +* (if=0 (a,I,J))),(Initialized s),1)) by A11, SCMFSA_M:2;
card (((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) = (card ((Macro (a =0_goto ((card J) + 3))) ";" J)) + (card (Goto ((card I) + 1))) by SCMFSA6A:21
.= (card ((Macro (a =0_goto ((card J) + 3))) ";" J)) + 1 by SCMFSA8A:15
.= ((card (Macro (a =0_goto ((card J) + 3)))) + (card J)) + 1 by SCMFSA6A:21
.= ((card J) + 2) + 1 by COMPOS_1:56
.= (card J) + (2 + 1) ;
then A13: Reloc ((I ";" (Stop SCM+FSA)),((card J) + 3)) c= if=0 (a,I,J) by A2, SCMFSA6A:38;
A14: Reloc ((I ";" (Stop SCM+FSA)),((card J) + 3)) c= P +* (if=0 (a,I,J)) by A13, A9, XBOOLE_1:1;
assume A15: I is_halting_on Initialized s,P ; :: thesis: IExec ((if=0 (a,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
then A16: P +* (I ";" (Stop SCM+FSA)) halts_on Initialized s by SCMFSA8A:34;
A17: CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),((LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) + 1)))) = CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),1)),(LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialized s)))))) by EXTPRO_1:4
.= IncAddr ((CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialized s),(LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))))))),((card J) + 3)) by A10, A12, Th2, A14, A1
.= IncAddr ((halt SCM+FSA),((card J) + 3)) by A16, EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_0:4 ;
then A18: P +* (if=0 (a,I,J)) halts_on Initialized s by EXTPRO_1:29;

now :: thesis: for l being Nat st l < (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) + 1 holds
CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),l))) <> halt SCM+FSA

let l be Nat; :: thesis: ( l < (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) + 1 implies CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),b₁))) <> halt SCM+FSA )
assume A19: l < (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) + 1 ; :: thesis: CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),b₁))) <> halt SCM+FSA

per cases ( l = 0 or l <> 0 ) ;

suppose l = 0 ; :: thesis: CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),b₁))) <> halt SCM+FSA

hence CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),l))) <> halt SCM+FSA by A7, A4, PBOOLE:143; :: thesis: verum

end;

suppose l <> 0 ; :: thesis: not CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),b₁))) = halt SCM+FSA

then consider n being Nat such that
A20: l = n + 1 by NAT_1:6;
assume A21: CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),l))) = halt SCM+FSA ; :: thesis: contradiction
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A22: InsCode (halt SCM+FSA) = 0 by COMPOS_1:70;
InsCode (CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialized s),n)))) = InsCode (IncAddr ((CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialized s),n)))),((card J) + 3))) by COMPOS_0:def 9
.= InsCode (CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),1)),n)))) by A10, A12, Th2, A14, A1
.= 0 by A20, A21, A22, EXTPRO_1:4 ;
then A23: CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialized s),n))) = halt SCM+FSA by SCMFSA_2:95;
n < LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialized s)) by A19, A20, XREAL_1:6;
hence contradiction by A16, A23, EXTPRO_1:def 15; :: thesis: verum

end;

end;

end;

then for l being Nat st CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),l))) = halt SCM+FSA holds
(LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) + 1 <= l ;
then A24: LifeSpan ((P +* (if=0 (a,I,J))),(Initialized s)) = (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) + 1 by A17, A18, EXTPRO_1:def 15;
A25: DataPart (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialized s),(LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))))) by A15, EXTPRO_1:23, SCMFSA8A:34
.= DataPart (Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),1)),(LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))))) by A10, A12, Th2, A1, A14
.= DataPart (Comput ((P +* (if=0 (a,I,J))),(Initialized s),((LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) + 1))) by EXTPRO_1:4
.= DataPart (Result ((P +* (if=0 (a,I,J))),(Initialized s))) by A18, A24, EXTPRO_1:23 ;

A26: now :: thesis: for x being object st x in dom (IExec ((if=0 (a,I,J)),P,s)) holds
(IExec ((if=0 (a,I,J)),P,s)) . x = ((IExec ((I ";" (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x

let x be object ; :: thesis: ( x in dom (IExec ((if=0 (a,I,J)),P,s)) implies (IExec ((if=0 (a,I,J)),P,s)) . b₁ = ((IExec ((I ";" (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b₁ )
A27: IExec ((I ";" (Stop SCM+FSA)),P,s) = Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s)) by SCMFSA6B:def 1;
A29: IExec ((if=0 (a,I,J)),P,s) = Result ((P +* (if=0 (a,I,J))),(Initialized s)) by SCMFSA6B:def 1;
assume A30: x in dom (IExec ((if=0 (a,I,J)),P,s)) ; :: thesis: (IExec ((if=0 (a,I,J)),P,s)) . b₁ = ((IExec ((I ";" (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b₁

per cases ( x is Int-Location or x is FinSeq-Location or x = IC ) by A30, SCMFSA_M:1;

suppose A31: x is Int-Location ; :: thesis: (IExec ((if=0 (a,I,J)),P,s)) . b₁ = ((IExec ((I ";" (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b₁

then x <> IC by SCMFSA_2:56;
then A32: not x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by TARSKI:def 1;
thus (IExec ((if=0 (a,I,J)),P,s)) . x = (Result ((P +* (if=0 (a,I,J))),(Initialized s))) . x by A29
.= (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) . x by A25, A31, SCMFSA_M:2
.= (IExec ((I ";" (Stop SCM+FSA)),P,s)) . x by A27
.= ((IExec ((I ";" (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x by A32, FUNCT_4:11 ; :: thesis: verum

end;

suppose A33: x is FinSeq-Location ; :: thesis: (IExec ((if=0 (a,I,J)),P,s)) . b₁ = ((IExec ((I ";" (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b₁

then x <> IC by SCMFSA_2:57;
then A34: not x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by TARSKI:def 1;
thus (IExec ((if=0 (a,I,J)),P,s)) . x = (Result ((P +* (if=0 (a,I,J))),(Initialized s))) . x by A29
.= (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) . x by A25, A33, SCMFSA_M:2
.= (IExec ((I ";" (Stop SCM+FSA)),P,s)) . x by A27
.= ((IExec ((I ";" (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x by A34, FUNCT_4:11 ; :: thesis: verum

end;

suppose A35: x = IC ; :: thesis: (IExec ((if=0 (a,I,J)),P,s)) . b₁ = ((IExec ((I ";" (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . b₁

then A36: x in dom (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by TARSKI:def 1;
A37: IC (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) = (IExec ((I ";" (Stop SCM+FSA)),P,s)) . (IC ) by A27
.= IC ((IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA))) by A15, SCMFSA8A:36
.= card I by FUNCT_4:113 ;
thus (IExec ((if=0 (a,I,J)),P,s)) . x = (Result ((P +* (if=0 (a,I,J))),(Initialized s))) . x by A29
.= (Comput ((P +* (if=0 (a,I,J))),(Initialized s),((LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))) + 1))) . x by A18, A24, EXTPRO_1:23
.= IC (Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialized s),1)),(LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialized s))))) by A35, EXTPRO_1:4
.= (IC (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialized s),(LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialized s)))))) + ((card J) + 3) by A10, A12, Th2, A14, A1
.= (IC (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialized s)))) + ((card J) + 3) by A15, EXTPRO_1:23, SCMFSA8A:34
.= (Start-At (((card I) + ((card J) + 3)),SCM+FSA)) . (IC ) by A37, FUNCOP_1:72
.= ((IExec ((I ";" (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) . x by A35, A36, FUNCT_4:13 ; :: thesis: verum

end;

end;

end;

dom (IExec ((if=0 (a,I,J)),P,s)) = the carrier of SCM+FSA by PARTFUN1:def 2
.= dom ((IExec ((I ";" (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))) by PARTFUN1:def 2 ;
hence IExec ((if=0 (a,I,J)),P,s) = (IExec ((I ";" (Stop SCM+FSA)),P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by A26, FUNCT_1:2
.= ((IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA))) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by A15, SCMFSA8A:36
.= (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) by FUNCT_4:114 ;
:: thesis: verum