let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I, J being really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a <> 0 & J is_halting_on s,P holds
if=0 (a,I,J) is_halting_on s,P
let s be State of SCM+FSA; :: thesis: for I, J being really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a <> 0 & J is_halting_on s,P holds
if=0 (a,I,J) is_halting_on s,P
let I, J be really-closed MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location st s . a <> 0 & J is_halting_on s,P holds
if=0 (a,I,J) is_halting_on s,P
let a be read-write Int-Location; :: thesis: ( s . a <> 0 & J is_halting_on s,P implies if=0 (a,I,J) is_halting_on s,P )
set I1 = I ";" (Stop SCM+FSA);
reconsider JI2 = ((J ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA) as really-closed Program of SCM+FSA by Lm3;
set s2 = Initialize s;
set P2 = P +* JI2;
A1: JI2 c= P +* JI2 by FUNCT_4:25;
set s3 = Initialize s;
set P3 = P +* (if=0 (a,I,J));
set s4 = Comput ((P +* (if=0 (a,I,J))),(Initialize s),1);
set s5 = Comput ((P +* (if=0 (a,I,J))),(Initialize s),2);
set i = a =0_goto ((card J) + 3);
IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
then A2: IC (Initialize s) = IC (Start-At (0,SCM+FSA)) by FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
A3: if=0 (a,I,J) c= P +* (if=0 (a,I,J)) by FUNCT_4:25;
if=0 (a,I,J) = (((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" (I ";" (Stop SCM+FSA)) by SCMFSA6A:25
.= ((a =0_goto ((card J) + 3)) ";" J) ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA))) by SCMFSA6A:25
.= (a =0_goto ((card J) + 3)) ";" (J ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA)))) by SCMFSA6A:29
.= (a =0_goto ((card J) + 3)) ";" ((J ";" (Goto ((card I) + 1))) ";" (I ";" (Stop SCM+FSA))) by SCMFSA6A:25
.= (Macro (a =0_goto ((card J) + 3))) ";" JI2 by SCMFSA6A:25 ;
then Reloc (JI2,(card (Macro (a =0_goto ((card J) + 3))))) c= if=0 (a,I,J) by SCMFSA6A:38;
then A4: Reloc (JI2,2) c= if=0 (a,I,J) by COMPOS_1:56;
A5: Reloc (JI2,2) c= P +* (if=0 (a,I,J)) by A4, A3, XBOOLE_1:1;
A6: not a in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;
A7: 0 in dom (if=0 (a,I,J)) by AFINSQ_1:65;
A8: if=0 (a,I,J) c= P +* (if=0 (a,I,J)) by FUNCT_4:25;
A9: (P +* (if=0 (a,I,J))) . 0 = (if=0 (a,I,J)) . 0 by A7, FUNCT_4:13
.= a =0_goto ((card J) + 3) by Lm2 ;
A10: 1 in dom (if=0 (a,I,J)) by Lm1;
A11: Comput ((P +* (if=0 (a,I,J))),(Initialize s),(0 + 1)) = Following ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialize s),0))) by EXTPRO_1:3
.= Following ((P +* (if=0 (a,I,J))),(Initialize s))
.= Exec ((a =0_goto ((card J) + 3)),(Initialize s)) by A2, A9, PBOOLE:143 ;
assume s . a <> 0 ; :: thesis: ( not J is_halting_on s,P or if=0 (a,I,J) is_halting_on s,P )
then (Initialize s) . a <> 0 by A6, FUNCT_4:11;
then A12: IC (Comput ((P +* (if=0 (a,I,J))),(Initialize s),1)) = 0 + 1 by A2, A11, SCMFSA_2:70;
A13: (P +* (if=0 (a,I,J))) . 1 = (if=0 (a,I,J)) . 1 by A10, A8, GRFUNC_1:2
.= goto 2 by Lm2 ;
A14: Comput ((P +* (if=0 (a,I,J))),(Initialize s),(1 + 1)) = Following ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialize s),1))) by EXTPRO_1:3
.= Exec ((goto 2),(Comput ((P +* (if=0 (a,I,J))),(Initialize s),1))) by A12, A13, PBOOLE:143 ;

A15: now :: thesis: for f being FinSeq-Location holds (Initialize s) . f = (Comput ((P +* (if=0 (a,I,J))),(Initialize s),2)) . f

let f be FinSeq-Location ; :: thesis: (Initialize s) . f = (Comput ((P +* (if=0 (a,I,J))),(Initialize s),2)) . f
thus (Initialize s) . f = (Comput ((P +* (if=0 (a,I,J))),(Initialize s),1)) . f by A11, SCMFSA_2:70
.= (Comput ((P +* (if=0 (a,I,J))),(Initialize s),2)) . f by A14, SCMFSA_2:69 ; :: thesis: verum

end;

now :: thesis: for a being Int-Location holds (Initialize s) . a = (Comput ((P +* (if=0 (a,I,J))),(Initialize s),2)) . a

let a be Int-Location; :: thesis: (Initialize s) . a = (Comput ((P +* (if=0 (a,I,J))),(Initialize s),2)) . a
thus (Initialize s) . a = (Comput ((P +* (if=0 (a,I,J))),(Initialize s),1)) . a by A11, SCMFSA_2:70
.= (Comput ((P +* (if=0 (a,I,J))),(Initialize s),2)) . a by A14, SCMFSA_2:69 ; :: thesis: verum

end;

then A16: DataPart (Initialize s) = DataPart (Comput ((P +* (if=0 (a,I,J))),(Initialize s),2)) by A15, SCMFSA_M:2;
assume A17: J is_halting_on s,P ; :: thesis: if=0 (a,I,J) is_halting_on s,P
A18: P +* JI2 halts_on Initialize s by A17, SCMFSA8A:38;
A19: IC (Comput ((P +* (if=0 (a,I,J))),(Initialize s),2)) = 2 by A14, SCMFSA_2:69;
CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialize s),((LifeSpan ((P +* JI2),(Initialize s))) + 2)))) = CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialize s),2)),(LifeSpan ((P +* JI2),(Initialize s)))))) by EXTPRO_1:4
.= IncAddr ((CurInstr ((P +* JI2),(Comput ((P +* JI2),(Initialize s),(LifeSpan ((P +* JI2),(Initialize s))))))),2) by A19, A16, Th2, A5, A1
.= IncAddr ((halt SCM+FSA),2) by A18, EXTPRO_1:def 15
.= halt SCM+FSA by COMPOS_0:4 ;
then P +* (if=0 (a,I,J)) halts_on Initialize s by EXTPRO_1:29;
hence if=0 (a,I,J) is_halting_on s,P by SCMFSA7B:def 7; :: thesis: verum