let s be State of SCMPDS; :: thesis: 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; :: thesis: ( 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)))) ; :: thesis: 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 S₁[ 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 :: thesis: 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; :: thesis: ( ( not IC (Comput (Q,s,n)) = IC s & not IC (Comput (Q,s,n)) = (IC s) + 1 ) or ( IC (Comput (Q,s,b₁)) = IC s & IC (Comput (Q,s,(b₁ + 1))) = (IC s) + 1 ) or ( IC (Comput (Q,s,b₁)) = (IC s) + 1 & 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)) = (IC s) + 1 ) ; :: thesis: ( ( IC (Comput (Q,s,b₁)) = IC s & IC (Comput (Q,s,(b₁ + 1))) = (IC s) + 1 ) or ( IC (Comput (Q,s,b₁)) = (IC s) + 1 & IC (Comput (Q,s,(b₁ + 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 ; :: thesis: IC (Comput (Q,s,(n + 1))) = (IC s) + 1

then 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 ; :: thesis: verum

end;

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

reconsider 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 ; :: thesis: verum

end;

end;

end;

then A13: for n being 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 Nat ;
assume IC (Comput (Q,s,nn)) in dom Q ; :: thesis: not CurInstr (Q,(Comput (Q,s,nn))) = halt SCMPDS
A14: S₁[ 0 ] ;
A15: for n being Nat holds S₁[n] from NAT_1:sch 2(A14, A13);

per cases ( IC (Comput (Q,s,n)) = IC s or IC (Comput (Q,s,n)) = (IC s) + 1 ) by A15;

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 PBOOLE:143
.= goto 1 by A6, A3, A1, 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)) = (IC s) + 1 ; :: thesis: not CurInstr (Q,(Comput (Q,s,nn))) = halt SCMPDS

then CurInstr (Q,(Comput (Q,s,n))) = Q . ((IC s) + 1) by PBOOLE:143
.= goto (- 1) by A5, A2, A1, FUNCT_4:13 ;
hence not CurInstr (Q,(Comput (Q,s,nn))) = halt SCMPDS by SCMPDS_2:73; :: thesis: verum

end;

end;