let s be State of SCMPDS; :: thesis: for P, Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st Q = P +* (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) holds
not Q halts_on s
let P, Q be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: 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:66;
IC s <> succ (IC s) ;
then A2: (((IC s),(succ (IC s))) --> ((goto 1),(goto (- 1)))) . (IC s) = goto 1 by FUNCT_4:66;
defpred S1[ 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:65;
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,b1)) = IC s & IC (Comput (Q,s,(b1 + 1))) = succ (IC s) ) or ( IC (Comput (Q,s,b1)) = succ (IC s) & 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)) = succ (IC s) ) ; :: thesis: ( ( IC (Comput (Q,s,b1)) = IC s & IC (Comput (Q,s,(b1 + 1))) = succ (IC s) ) or ( IC (Comput (Q,s,b1)) = succ (IC s) & IC (Comput (Q,s,(b1 + 1))) = IC s ) )
A8: Q /. (IC (Comput (Q,s,n))) = Q . (IC (Comput (Q,s,n))) by PBOOLE:158;
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, FUNCT_4:14, Z ;
thus IC (Comput (Q,s,(n + 1))) = IC (Following (Q,(Comput (Q,s,n)))) by EXTPRO_1:4
.= ICplusConst ((Comput (Q,s,n)),1) by A10, SCMPDS_2:66
.= succ (IC s) by A9, SCMPDS_3:20 ; :: 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 20;
A14: Q /. (IC (Comput (Q,s,n))) = Q . (IC (Comput (Q,s,n))) by PBOOLE:158;
A15: CurInstr (Q,(Comput (Q,s,n))) = Q . (succ (IC s)) by A12, A14
.= goto (- 1) by A4, A1, FUNCT_4:14, Z ;
thus IC (Comput (Q,s,(n + 1))) = IC (Following (Q,(Comput (Q,s,n)))) by EXTPRO_1:4
.= abs ((i + 4) + (- 4)) by A12, A15, A13, SCMPDS_2:66
.= IC s by ABSVALUE:def 1 ; :: thesis: verum
end;
end;
end;
then A17: for n being Element of NAT st S1[n] holds
S1[n + 1] ;
let nn be Nat; :: according to EXTPRO_1:def 7 :: 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 13;
assume IC (Comput (Q,s,nn)) in dom Q ; :: thesis: not CurInstr (Q,(Comput (Q,s,nn))) = halt SCMPDS
A18: S1[ 0 ] by EXTPRO_1:3;
A19: for n being Element of NAT holds S1[n] from NAT_1:sch 1(A18, A17);
 A21: Q /. (IC (Comput (Q,s,n))) = Q . (IC (Comput (Q,s,n))) by PBOOLE:158;
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, FUNCT_4:14, Z ;
hence not CurInstr (Q,(Comput (Q,s,nn))) = halt SCMPDS by SCMPDS_2:85; :: 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, FUNCT_4:14, Z ;
hence not CurInstr (Q,(Comput (Q,s,nn))) = halt SCMPDS by SCMPDS_2:85; :: thesis: verum
end;
end;