let s be State of SCM+FSA; 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; not P +* ((IC s),(goto (IC s))) halts_on s
set Q = P +* ((IC s),(goto (IC s)));
defpred S1[ 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 for n being Nat st S1[n] holds
S1[n + 1]let n be
Nat;
( S1[n] implies S1[n + 1] )assume
S1[
n]
;
S1[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
S1[
n + 1]
;
verum end;
let n be Nat; EXTPRO_1:def 8 ( 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:
S1[ 0 ]
;
assume A6:
IC (Comput ((P +* ((IC s),(goto (IC s)))),s,n)) in dom (P +* ((IC s),(goto (IC s))))
; 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 S1[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
; verum