let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA holds not P +* ((IC s),(goto (IC s))) halts_on s
let P be Instruction-Sequence of SCM+FSA; :: thesis: not P +* ((IC s),(goto (IC s))) halts_on s
set Q = P +* ((IC s),(goto (IC s)));
defpred S₁[ Nat] means IC (Comput ((P +* ((IC s),(goto (IC s)))),s,$1)) = IC s;
A1: dom P = NAT by PARTFUN1:def 2;
A2: dom P = dom (P +* ((IC s),(goto (IC s)))) by FUNCT_7:30;

A3: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then A4: CurInstr ((P +* ((IC s),(goto (IC s)))),(Comput ((P +* ((IC s),(goto (IC s)))),s,n))) = (P +* ((IC s),(goto (IC s)))) . (IC s) by A2, A1, PARTFUN1:def 6
.= goto (IC s) by A1, FUNCT_7:31 ;
IC (Comput ((P +* ((IC s),(goto (IC s)))),s,(n + 1))) = IC (Following ((P +* ((IC s),(goto (IC s)))),(Comput ((P +* ((IC s),(goto (IC s)))),s,n)))) by EXTPRO_1:3
.= IC s by A4, SCMFSA_2:69 ;
hence S₁[n + 1] ; :: thesis: verum

end;

let n be Nat; :: according to EXTPRO_1:def 8 :: thesis: ( not IC (Comput ((P +* ((IC s),(goto (IC s)))),s,n)) in dom (P +* ((IC s),(goto (IC s)))) or not CurInstr ((P +* ((IC s),(goto (IC s)))),(Comput ((P +* ((IC s),(goto (IC s)))),s,n))) = halt SCM+FSA )
A5: S₁[ 0 ] ;
assume A6: IC (Comput ((P +* ((IC s),(goto (IC s)))),s,n)) in dom (P +* ((IC s),(goto (IC s)))) ; :: thesis: not CurInstr ((P +* ((IC s),(goto (IC s)))),(Comput ((P +* ((IC s),(goto (IC s)))),s,n))) = halt SCM+FSA
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A7: for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A3);
CurInstr ((P +* ((IC s),(goto (IC s)))),(Comput ((P +* ((IC s),(goto (IC s)))),s,n))) = (P +* ((IC s),(goto (IC s)))) . (IC (Comput ((P +* ((IC s),(goto (IC s)))),s,n))) by A6, PARTFUN1:def 6
.= (P +* ((IC s),(goto (IC s)))) . (IC s) by A7
.= goto (IC s) by A1, FUNCT_7:31 ;
hence not CurInstr ((P +* ((IC s),(goto (IC s)))),(Comput ((P +* ((IC s),(goto (IC s)))),s,n))) = halt SCM+FSA ; :: thesis: verum