let s2 be State of ; :: thesis: not ProgramPart (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))) halts_on s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))
set m = (IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1));
set s1 = s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)));
A1: ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))) . (Next (IC s2)) = goto (- 1) by FUNCT_4:66;
IC s2 <> Next (IC s2) ;
then A2: ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))) . (IC s2) = goto 1 by FUNCT_4:66;
defpred S₁[ Nat] means ( IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),$1) = IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))) or IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),$1) = Next (IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))) );
A3: dom ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))) = {(IC s2),(Next (IC s2))} by FUNCT_4:65;
then A4: Next (IC s2) in dom ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))) by TARSKI:def 2;
( IC SCMPDS <> IC s2 & IC SCMPDS <> Next (IC s2) ) by AMI_1:48;
then not IC SCMPDS in dom ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))) by A3, TARSKI:def 2;
then A5: IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))) = IC s2 by FUNCT_4:12;
A6: IC s2 in dom ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))) by A3, TARSKI:def 2;

now

let n be Element of NAT ; :: thesis: ( ( not IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n) = IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))) & not IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n) = Next (IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))) ) or ( IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),b₁) = IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))) & IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),(b₁ + 1)) = Next (IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))) ) or ( IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),b₁) = Next (IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))) & IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),(b₁ + 1)) = IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))) ) )
set Cn = Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n;
assume A7: ( IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n) = IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))) or IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n) = Next (IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))) ) ; :: thesis: ( ( IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),b₁) = IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))) & IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),(b₁ + 1)) = Next (IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))) ) or ( IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),b₁) = Next (IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))) & IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),(b₁ + 1)) = IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))) ) )

per cases ( IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n) = IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))) or IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n) = Next (IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))) ) by A7;

case A8: IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n) = IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))) ; :: thesis: IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),(n + 1)) = Next (IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))))

then A9: CurInstr (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n) = (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))) . (IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))) by AMI_1:54
.= goto 1 by A6, A2, A5, FUNCT_4:14 ;
thus IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),(n + 1)) = IC (Following (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n)) by AMI_1:14
.= ICplusConst (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n),1 by A9, SCMPDS_2:66
.= Next (IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))) by A8, SCMPDS_3:20 ; :: thesis: verum

end;

case A10: IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n) = Next (IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))) ; :: thesis: IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),(n + 1)) = IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))

reconsider i = IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))) as Element of NAT by AMI_1:def 4;
A11: ex j being Element of NAT st
( j = IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n) & ICplusConst (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n),(- 1) = abs (j + (- 1)) ) by SCMPDS_2:def 20;
A12: CurInstr (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n) = (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))) . (Next (IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))))) by A10, AMI_1:54
.= goto (- 1) by A4, A1, A5, FUNCT_4:14 ;
thus IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),(n + 1)) = IC (Following (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n)) by AMI_1:14
.= abs ((i + 4) + (- 4)) by A10, A12, A11, SCMPDS_2:66
.= IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))) by ABSVALUE:def 1 ; :: thesis: verum

end;

end;

end;

then A13: for n being Element of NAT st S₁[n] holds
S₁[n + 1] ;
let n be Element of NAT ; :: according to AMI_1:def 20 :: thesis: ( not IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n) in dom (ProgramPart (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))) or not (ProgramPart (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))) . (IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n)) = halt SCMPDS )
assume IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n) in dom (ProgramPart (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))) ; :: thesis: not (ProgramPart (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))) . (IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n)) = halt SCMPDS
A14: S₁[ 0 ] by AMI_1:13;
A15: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A14, A13);

per cases ( IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n) = IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))) or IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n) = Next (IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))) ) by A15;

suppose IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n) = IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))) ; :: thesis: not (ProgramPart (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))) . (IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n)) = halt SCMPDS

then CurInstr (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n) = (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))) . (IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))) by AMI_1:54
.= goto 1 by A6, A2, A5, FUNCT_4:14 ;
then CurInstr (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n) <> halt SCMPDS by SCMPDS_2:85;
hence not (ProgramPart (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))) . (IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n)) = halt SCMPDS by AMI_1:145; :: thesis: verum

end;

suppose IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n) = Next (IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))) ; :: thesis: not (ProgramPart (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))) . (IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n)) = halt SCMPDS

then CurInstr (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n) = (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))) . (Next (IC (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))))) by AMI_1:54
.= goto (- 1) by A4, A1, A5, FUNCT_4:14 ;
then CurInstr (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n) <> halt SCMPDS by SCMPDS_2:85;
hence not (ProgramPart (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1))))) . (IC (Computation (s2 +* ((IC s2),(Next (IC s2)) --> (goto 1),(goto (- 1)))),n)) = halt SCMPDS by AMI_1:145; :: thesis: verum

end;

end;