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 s,P holds
if=0 (a,I,J) is_halting_on s,P
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 s,P holds
if=0 (a,I,J) is_halting_on s,P
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 s,P holds
if=0 (a,I,J) is_halting_on s,P
let J be MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location st s . a = 0 & I 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 & I is_halting_on s,P implies if=0 (a,I,J) is_halting_on s,P )
set I1 = I ";" (Stop SCM+FSA);
set s1 = Initialize s;
set P1 = P +* (I ";" (Stop SCM+FSA));
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 i = a =0_goto ((card J) + 3);
A1: not a in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;
A2: 0 in dom (if=0 (a,I,J)) by AFINSQ_1:65;
A3: (P +* (if=0 (a,I,J))) . 0 = (if=0 (a,I,J)) . 0 by A2, FUNCT_4:13
.= a =0_goto ((card J) + 3) by Lm2 ;
IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
then A4: IC (Initialize s) = IC (Start-At (0,SCM+FSA)) by FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
A5: if=0 (a,I,J) c= P +* (if=0 (a,I,J)) by FUNCT_4:25;
A6: if=0 (a,I,J) = (((a =0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" (I ";" (Stop SCM+FSA)) by SCMFSA6A:25;
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 A7: Reloc ((I ";" (Stop SCM+FSA)),((card J) + 3)) c= if=0 (a,I,J) by A6, SCMFSA6A:38;
A8: Reloc ((I ";" (Stop SCM+FSA)),((card J) + 3)) c= P +* (if=0 (a,I,J)) by A7, A5, XBOOLE_1:1;
A9: 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 A4, A3, PBOOLE:143 ;
A10: for f being FinSeq-Location holds (Initialize s) . f = (Comput ((P +* (if=0 (a,I,J))),(Initialize s),1)) . f by A9, SCMFSA_2:70;
for a being Int-Location holds (Initialize s) . a = (Comput ((P +* (if=0 (a,I,J))),(Initialize s),1)) . a by A9, SCMFSA_2:70;
then A11: DataPart (Initialize s) = DataPart (Comput ((P +* (if=0 (a,I,J))),(Initialize s),1)) by A10, SCMFSA_M:2;
assume s . a = 0 ; :: thesis: ( not I is_halting_on s,P or if=0 (a,I,J) is_halting_on s,P )
then (Initialize s) . a = 0 by A1, FUNCT_4:11;
then A12: IC (Comput ((P +* (if=0 (a,I,J))),(Initialize s),1)) = (card J) + 3 by A9, SCMFSA_2:70;
assume A13: I is_halting_on s,P ; :: thesis: if=0 (a,I,J) is_halting_on s,P
I ";" (Stop SCM+FSA) is_halting_on s,P by A13, SCMFSA8A:30;
then A14: P +* (I ";" (Stop SCM+FSA)) halts_on Initialize s by SCMFSA7B:def 7;
A15: I ";" (Stop SCM+FSA) c= P +* (I ";" (Stop SCM+FSA)) by FUNCT_4:25;
CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialize s),((LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1)))) = CurInstr ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Comput ((P +* (if=0 (a,I,J))),(Initialize s),1)),(LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)))))) by EXTPRO_1:4
.= IncAddr ((CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))))))),((card J) + 3)) by A12, A11, Th2, A8, A15
.= IncAddr ((halt SCM+FSA),((card J) + 3)) by A14, 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