let s be State of SCMPDS; for P, Q being Instruction-Sequence of SCMPDS st Q = P +* (((IC s),((IC s) + 1)) --> ((goto 1),(goto (- 1)))) holds
not Q halts_on s
let P, Q be Instruction-Sequence of SCMPDS; ( Q = P +* (((IC s),((IC s) + 1)) --> ((goto 1),(goto (- 1)))) implies not Q halts_on s )
assume A1:
Q = P +* (((IC s),((IC s) + 1)) --> ((goto 1),(goto (- 1))))
; not Q halts_on s
set m = ((IC s),((IC s) + 1)) --> ((goto 1),(goto (- 1)));
A2:
(((IC s),((IC s) + 1)) --> ((goto 1),(goto (- 1)))) . ((IC s) + 1) = goto (- 1)
by FUNCT_4:63;
IC s <> (IC s) + 1
;
then A3:
(((IC s),((IC s) + 1)) --> ((goto 1),(goto (- 1)))) . (IC s) = goto 1
by FUNCT_4:63;
defpred S1[ Nat] means ( IC (Comput (Q,s,$1)) = IC s or IC (Comput (Q,s,$1)) = (IC s) + 1 );
A4:
dom (((IC s),((IC s) + 1)) --> ((goto 1),(goto (- 1)))) = {(IC s),((IC s) + 1)}
by FUNCT_4:62;
then A5:
(IC s) + 1 in dom (((IC s),((IC s) + 1)) --> ((goto 1),(goto (- 1))))
by TARSKI:def 2;
A6:
IC s in dom (((IC s),((IC s) + 1)) --> ((goto 1),(goto (- 1))))
by A4, TARSKI:def 2;
now for n being Nat holds
( ( not IC (Comput (Q,s,n)) = IC s & not IC (Comput (Q,s,n)) = (IC s) + 1 ) or ( IC (Comput (Q,s,n)) = IC s & IC (Comput (Q,s,(n + 1))) = (IC s) + 1 ) or ( IC (Comput (Q,s,n)) = (IC s) + 1 & IC (Comput (Q,s,(n + 1))) = IC s ) )let n be
Nat;
( ( not IC (Comput (Q,s,n)) = IC s & not IC (Comput (Q,s,n)) = (IC s) + 1 ) or ( IC (Comput (Q,s,b1)) = IC s & IC (Comput (Q,s,(b1 + 1))) = (IC s) + 1 ) or ( IC (Comput (Q,s,b1)) = (IC s) + 1 & IC (Comput (Q,s,(b1 + 1))) = IC s ) )set Cn =
Comput (
Q,
s,
n);
assume A7:
(
IC (Comput (Q,s,n)) = IC s or
IC (Comput (Q,s,n)) = (IC s) + 1 )
;
( ( IC (Comput (Q,s,b1)) = IC s & IC (Comput (Q,s,(b1 + 1))) = (IC s) + 1 ) or ( IC (Comput (Q,s,b1)) = (IC s) + 1 & IC (Comput (Q,s,(b1 + 1))) = IC s ) )per cases
( IC (Comput (Q,s,n)) = IC s or IC (Comput (Q,s,n)) = (IC s) + 1 )
by A7;
case A8:
IC (Comput (Q,s,n)) = IC s
;
IC (Comput (Q,s,(n + 1))) = (IC s) + 1then A9:
CurInstr (
Q,
(Comput (Q,s,n))) =
Q . (IC s)
by PBOOLE:143
.=
goto 1
by A6, A3, A1, FUNCT_4:13
;
thus IC (Comput (Q,s,(n + 1))) =
IC (Following (Q,(Comput (Q,s,n))))
by EXTPRO_1:3
.=
ICplusConst (
(Comput (Q,s,n)),1)
by A9, SCMPDS_2:54
.=
(IC s) + 1
by A8, SCMPDS_3:10
;
verum end; case A10:
IC (Comput (Q,s,n)) = (IC s) + 1
;
IC (Comput (Q,s,(n + 1))) = IC sreconsider i =
IC s as
Element of
NAT ;
A11:
ex
j being
Element of
NAT st
(
j = IC (Comput (Q,s,n)) &
ICplusConst (
(Comput (Q,s,n)),
(- 1))
= |.(j + (- 1)).| )
by SCMPDS_2:def 18;
A12:
CurInstr (
Q,
(Comput (Q,s,n))) =
Q . ((IC s) + 1)
by A10, PBOOLE:143
.=
goto (- 1)
by A5, A2, A1, FUNCT_4:13
;
thus IC (Comput (Q,s,(n + 1))) =
IC (Following (Q,(Comput (Q,s,n))))
by EXTPRO_1:3
.=
|.((i + 4) + (- 4)).|
by A10, A12, A11, SCMPDS_2:54
.=
IC s
by ABSVALUE:def 1
;
verum end; end;
then A13:
for n being Nat st S1[n] holds
S1[n + 1]
;
let nn be Nat; EXTPRO_1:def 8 ( not IC (Comput (Q,s,nn)) in proj1 Q or not CurInstr (Q,(Comput (Q,s,nn))) = halt SCMPDS )
reconsider n = nn as Nat ;
assume
IC (Comput (Q,s,nn)) in dom Q
; not CurInstr (Q,(Comput (Q,s,nn))) = halt SCMPDS
A14:
S1[ 0 ]
;
A15:
for n being Nat holds S1[n]
from NAT_1:sch 2(A14, A13);