let s2 be State of SCM+FSA; :: thesis: for P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds not P2 +* ((IC s2),(goto (IC s2))) halts_on s2 +* ((IC s2),(goto (IC s2)))
let P2 be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: not P2 +* ((IC s2),(goto (IC s2))) halts_on s2 +* ((IC s2),(goto (IC s2)))
set s1 = s2 +* ((IC s2),(goto (IC s2)));
set P1 = P2 +* ((IC s2),(goto (IC s2)));
defpred S₁[ Nat] means IC (Comput ((P2 +* ((IC s2),(goto (IC s2)))),(s2 +* ((IC s2),(goto (IC s2)))),$1)) = IC (s2 +* ((IC s2),(goto (IC s2))));
IC <> IC s2 by COMPOS_1:3;
then A1: IC (s2 +* ((IC s2),(goto (IC s2)))) = IC s2 by FUNCT_7:34;
IC s2 in NAT ;
then A2: IC s2 in dom P2 by PARTFUN1:def 4;

A3: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then A5: CurInstr ((P2 +* ((IC s2),(goto (IC s2)))),(Comput ((P2 +* ((IC s2),(goto (IC s2)))),(s2 +* ((IC s2),(goto (IC s2)))),n))) = (P2 +* ((IC s2),(goto (IC s2)))) . (IC (s2 +* ((IC s2),(goto (IC s2))))) by PBOOLE:158
.= goto (IC s2) by A1, A2, FUNCT_7:33 ;
IC (Comput ((P2 +* ((IC s2),(goto (IC s2)))),(s2 +* ((IC s2),(goto (IC s2)))),(n + 1))) = IC (Following ((P2 +* ((IC s2),(goto (IC s2)))),(Comput ((P2 +* ((IC s2),(goto (IC s2)))),(s2 +* ((IC s2),(goto (IC s2)))),n)))) by EXTPRO_1:4
.= IC (s2 +* ((IC s2),(goto (IC s2)))) by A1, A5, SCMFSA_2:95 ;
hence S₁[n + 1] ; :: thesis: verum

end;

let n be Nat; :: according to EXTPRO_1:def 7 :: thesis: ( not IC (Comput ((P2 +* ((IC s2),(goto (IC s2)))),(s2 +* ((IC s2),(goto (IC s2)))),n)) in proj1 (P2 +* ((IC s2),(goto (IC s2)))) or not CurInstr ((P2 +* ((IC s2),(goto (IC s2)))),(Comput ((P2 +* ((IC s2),(goto (IC s2)))),(s2 +* ((IC s2),(goto (IC s2)))),n))) = halt SCM+FSA )
A6: S₁[ 0 ] by EXTPRO_1:3;
assume IC (Comput ((P2 +* ((IC s2),(goto (IC s2)))),(s2 +* ((IC s2),(goto (IC s2)))),n)) in dom (P2 +* ((IC s2),(goto (IC s2)))) ; :: thesis: not CurInstr ((P2 +* ((IC s2),(goto (IC s2)))),(Comput ((P2 +* ((IC s2),(goto (IC s2)))),(s2 +* ((IC s2),(goto (IC s2)))),n))) = halt SCM+FSA
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A7: (P2 +* ((IC s2),(goto (IC s2)))) /. (IC (Comput ((P2 +* ((IC s2),(goto (IC s2)))),(s2 +* ((IC s2),(goto (IC s2)))),n))) = (P2 +* ((IC s2),(goto (IC s2)))) . (IC (Comput ((P2 +* ((IC s2),(goto (IC s2)))),(s2 +* ((IC s2),(goto (IC s2)))),n))) by PBOOLE:158;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A6, A3);
then CurInstr ((P2 +* ((IC s2),(goto (IC s2)))),(Comput ((P2 +* ((IC s2),(goto (IC s2)))),(s2 +* ((IC s2),(goto (IC s2)))),n))) = (P2 +* ((IC s2),(goto (IC s2)))) . (IC (s2 +* ((IC s2),(goto (IC s2))))) by A7
.= goto (IC s2) by A1, A2, FUNCT_7:33 ;
hence not CurInstr ((P2 +* ((IC s2),(goto (IC s2)))),(Comput ((P2 +* ((IC s2),(goto (IC s2)))),(s2 +* ((IC s2),(goto (IC s2)))),n))) = halt SCM+FSA ; :: thesis: verum