let l be Nat; 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; 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; ( 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
; not P halts_on s
A3:
P /. (IC s) = P . (IC s)
by PBOOLE:143;
defpred S1[ Nat] means Comput (P,s,$1) = s;
A4:
for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be
Nat;
( S1[m] implies S1[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
;
S1[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
;
verum
end;
let mm be Nat; EXTPRO_1:def 8 ( 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:
S1[ 0 ]
;
for m being Nat holds S1[m]
from NAT_1:sch 2(A8, A4);
then A9:
S1[m]
;
assume
IC (Comput (P,s,mm)) in dom P
; 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; verum