let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) = goto 0 & ( for m being Element of NAT st m <= LifeSpan ((P +* I),(Initialize s)) holds
CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),m))) <> halt SCM+FSA ) )
A1: dom (id the InstructionsF of SCM+FSA) = the InstructionsF of SCM+FSA ;
let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) = goto 0 & ( for m being Element of NAT st m <= LifeSpan ((P +* I),(Initialize s)) holds
CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),m))) <> halt SCM+FSA ) )
let I be Program of SCM+FSA; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P implies ( CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) = goto 0 & ( for m being Element of NAT st m <= LifeSpan ((P +* I),(Initialize s)) holds
CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),m))) <> halt SCM+FSA ) ) )
set s1 = Initialize s;
set P1 = P +* I;
set s2 = Initialize s;
set P2 = P +* (loop I);
A2: I c= P +* I by FUNCT_4:25;
assume that
A3: I is_closed_on s,P and
A4: I is_halting_on s,P ; :: thesis: ( CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) = goto 0 & ( for m being Element of NAT st m <= LifeSpan ((P +* I),(Initialize s)) holds
CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),m))) <> halt SCM+FSA ) )
set k = LifeSpan ((P +* I),(Initialize s));
A5: IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) in dom I by A3, SCMFSA7B:def 6;
A6: dom (loop I) = dom I by FUNCT_4:99;
A7: P +* I halts_on Initialize s by A4, SCMFSA7B:def 7;
then A8: CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) = halt SCM+FSA by EXTPRO_1:def 15;
A9: CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) = (P +* I) . (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) by PBOOLE:143
.= I . (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) by A2, A5, GRFUNC_1:2 ;
A10: rng I c= the InstructionsF of SCM+FSA by RELAT_1:def 19;
A11: (P +* (loop I)) /. (IC (Comput ((P +* (loop I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) = (P +* (loop I)) . (IC (Comput ((P +* (loop I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) by PBOOLE:143;
Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))) = Comput ((P +* (loop I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))) by A3, A4, Th76;
hence A12: CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) = (P +* (loop I)) . (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) by A11
.= (loop I) . (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) by A5, A6, FUNCT_4:13
.= (((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto 0))) * I) . (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) by A10, FUNCT_7:116
.= ((id the InstructionsF of SCM+FSA) +* ((halt SCM+FSA),(goto 0))) . (halt SCM+FSA) by A8, A5, A9, FUNCT_1:13
.= goto 0 by A1, FUNCT_7:31 ;
:: thesis: for m being Element of NAT st m <= LifeSpan ((P +* I),(Initialize s)) holds
CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),m))) <> halt SCM+FSA
let m be Element of NAT ; :: thesis: ( m <= LifeSpan ((P +* I),(Initialize s)) implies CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),m))) <> halt SCM+FSA )
assume A13: m <= LifeSpan ((P +* I),(Initialize s)) ; :: thesis: CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),m))) <> halt SCM+FSA

per cases ( m < LifeSpan ((P +* I),(Initialize s)) or m = LifeSpan ((P +* I),(Initialize s)) ) by A13, XXREAL_0:1;

suppose A14: m < LifeSpan ((P +* I),(Initialize s)) ; :: thesis: CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),m))) <> halt SCM+FSA

then CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),m))) <> halt SCM+FSA by A7, EXTPRO_1:def 15;
hence CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),m))) <> halt SCM+FSA by A3, A4, A14, Th77; :: thesis: verum

end;

suppose m = LifeSpan ((P +* I),(Initialize s)) ; :: thesis: CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),m))) <> halt SCM+FSA

hence CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),m))) <> halt SCM+FSA by A12; :: thesis: verum

end;

end;