let l be Nat; :: thesis: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st IC s = l & P . l = goto l holds
not P halts_on s
let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA st IC s = l & P . l = goto l holds
not P halts_on s
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( IC s = l & P . l = goto l implies not P halts_on s )
assume that
A1: IC s = l and
A2: P . l = goto l ; :: thesis: not P halts_on s
A3: P /. (IC s) = P . (IC s) by PBOOLE:143;
defpred S₁[ Nat] means Comput (P,s,$1) = s;
A4: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
A5: for f being FinSeq-Location holds (Exec ((goto l),s)) . f = s . f by SCMFSA_2:69;
A6: ( IC (Exec ((goto l),s)) = IC s & ( for a being Int-Location holds (Exec ((goto l),s)) . a = s . a ) ) by A1, SCMFSA_2:69;
assume A7: Comput (P,s,m) = s ; :: thesis: S₁[m + 1]
thus Comput (P,s,(m + 1)) = Following (P,s) by A7, EXTPRO_1:3
.= s by A1, A2, A6, A5, A3, SCMFSA_2:104 ; :: thesis: verum

end;

let mm be Nat; :: according to EXTPRO_1:def 8 :: thesis: ( not IC (Comput (P,s,mm)) in dom P or not CurInstr (P,(Comput (P,s,mm))) = halt SCM+FSA )
reconsider m = mm as Element of NAT by ORDINAL1:def 12;
A8: S₁[ 0 ] ;
for m being Nat holds S₁[m] from NAT_1:sch 2(A8, A4);
then A9: S₁[m] ;
assume IC (Comput (P,s,mm)) in dom P ; :: thesis: not CurInstr (P,(Comput (P,s,mm))) = halt SCM+FSA
thus CurInstr (P,(Comput (P,s,mm))) <> halt SCM+FSA by A1, A2, A9, PBOOLE:143; :: thesis: verum