let s be State of SCMPDS; :: thesis: for P, Q being Instruction-Sequence of SCMPDS st Q = P +* (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) holds
not Q halts_on s
let P, Q be Instruction-Sequence of SCMPDS; :: thesis: ( Q = P +* (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) implies not Q halts_on s )
assume Z: Q = P +* (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) ; :: thesis: not Q halts_on s
set m = ((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)));
A1: (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) . (succ (IC s)) = goto (- 1) by FUNCT_4:63;
IC s <> succ (IC s) ;
then A2: (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) . (IC s) = goto 1 by FUNCT_4:63;
defpred S₁[ Nat] means ( IC (Comput (Q,s,$1)) = IC s or IC (Comput (Q,s,$1)) = succ (IC s) );
A3: dom (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) = {(IC s),(succ (IC s))} by FUNCT_4:62;
then A4: succ (IC s) in dom (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) by TARSKI:def 2;
A6: IC s in dom (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) by A3, TARSKI:def 2;

now

let n be Element of NAT ; :: thesis: ( ( not IC (Comput (Q,s,n)) = IC s & not IC (Comput (Q,s,n)) = succ (IC s) ) or ( IC (Comput (Q,s,b₁)) = IC s & IC (Comput (Q,s,(b₁ + 1))) = succ (IC s) ) or ( IC (Comput (Q,s,b₁)) = succ (IC s) & IC (Comput (Q,s,(b₁ + 1))) = IC s ) )
set Cn = Comput (Q,s,n);
assume A7: ( IC (Comput (Q,s,n)) = IC s or IC (Comput (Q,s,n)) = succ (IC s) ) ; :: thesis: ( ( IC (Comput (Q,s,b₁)) = IC s & IC (Comput (Q,s,(b₁ + 1))) = succ (IC s) ) or ( IC (Comput (Q,s,b₁)) = succ (IC s) & IC (Comput (Q,s,(b₁ + 1))) = IC s ) )
A8: Q /. (IC (Comput (Q,s,n))) = Q . (IC (Comput (Q,s,n))) by PBOOLE:143;

per cases ( IC (Comput (Q,s,n)) = IC s or IC (Comput (Q,s,n)) = succ (IC s) ) by A7;

case A9: IC (Comput (Q,s,n)) = IC s ; :: thesis: IC (Comput (Q,s,(n + 1))) = succ (IC s)

then A10: CurInstr (Q,(Comput (Q,s,n))) = Q . (IC s) by A8
.= goto 1 by A6, A2, Z, 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 A10, SCMPDS_2:54
.= succ (IC s) by A9, SCMPDS_3:10 ; :: thesis: verum

end;

case A12: IC (Comput (Q,s,n)) = succ (IC s) ; :: thesis: IC (Comput (Q,s,(n + 1))) = IC s

reconsider i = IC s as Element of NAT ;
A13: ex j being Element of NAT st
( j = IC (Comput (Q,s,n)) & ICplusConst ((Comput (Q,s,n)),(- 1)) = abs (j + (- 1)) ) by SCMPDS_2:def 18;
A14: Q /. (IC (Comput (Q,s,n))) = Q . (IC (Comput (Q,s,n))) by PBOOLE:143;
A15: CurInstr (Q,(Comput (Q,s,n))) = Q . (succ (IC s)) by A12, A14
.= goto (- 1) by A4, A1, Z, FUNCT_4:13 ;
thus IC (Comput (Q,s,(n + 1))) = IC (Following (Q,(Comput (Q,s,n)))) by EXTPRO_1:3
.= abs ((i + 4) + (- 4)) by A12, A15, A13, SCMPDS_2:54
.= IC s by ABSVALUE:def 1 ; :: thesis: verum

end;

end;

end;

then A17: for n being Element of NAT st S₁[n] holds
S₁[n + 1] ;
let nn be Nat; :: according to EXTPRO_1:def 8 :: thesis: ( not IC (Comput (Q,s,nn)) in proj1 Q or not CurInstr (Q,(Comput (Q,s,nn))) = halt SCMPDS )
reconsider n = nn as Element of NAT by ORDINAL1:def 12;
assume IC (Comput (Q,s,nn)) in dom Q ; :: thesis: not CurInstr (Q,(Comput (Q,s,nn))) = halt SCMPDS
A18: S₁[ 0 ] by EXTPRO_1:2;
A19: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A18, A17);
A21: Q /. (IC (Comput (Q,s,n))) = Q . (IC (Comput (Q,s,n))) by PBOOLE:143;

per cases ( IC (Comput (Q,s,n)) = IC s or IC (Comput (Q,s,n)) = succ (IC s) ) by A19;

suppose IC (Comput (Q,s,n)) = IC s ; :: thesis: not CurInstr (Q,(Comput (Q,s,nn))) = halt SCMPDS

then CurInstr (Q,(Comput (Q,s,n))) = Q . (IC s) by A21
.= goto 1 by A6, A2, Z, FUNCT_4:13 ;
hence not CurInstr (Q,(Comput (Q,s,nn))) = halt SCMPDS by SCMPDS_2:73; :: thesis: verum

end;

suppose IC (Comput (Q,s,n)) = succ (IC s) ; :: thesis: not CurInstr (Q,(Comput (Q,s,nn))) = halt SCMPDS

then CurInstr (Q,(Comput (Q,s,n))) = Q . (succ (IC s)) by A21
.= goto (- 1) by A4, A1, Z, FUNCT_4:13 ;
hence not CurInstr (Q,(Comput (Q,s,nn))) = halt SCMPDS by SCMPDS_2:73; :: thesis: verum

end;

end;