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

now

let n be Element of NAT ; :: thesis: ( ( not IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n) = IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))) & not IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n) = succ (IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))) ) or ( IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),b₁) = IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))) & IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),(b₁ + 1)) = succ (IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))) ) or ( IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),b₁) = succ (IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))) & IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),(b₁ + 1)) = IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))) ) )
set Cn = Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n;
assume A7: ( IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n) = IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))) or IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n) = succ (IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))) ) ; :: thesis: ( ( IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),b₁) = IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))) & IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),(b₁ + 1)) = succ (IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))) ) or ( IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),b₁) = succ (IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))) & IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),(b₁ + 1)) = IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))) ) )
Y: (ProgramPart (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n)) /. (IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n)) = (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n) . (IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n)) by COMPOS_1:38;

per cases ( IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n) = IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))) or IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n) = succ (IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))) ) by A7;

case A8: IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n) = IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))) ; :: thesis: IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),(n + 1)) = succ (IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))))

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

end;

case A10: IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n) = succ (IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))) ; :: thesis: IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),(n + 1)) = IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))

reconsider i = IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))) as Element of NAT ;
A11: ex j being Element of NAT st
( j = IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n) & ICplusConst (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n),(- 1) = abs (j + (- 1)) ) by SCMPDS_2:def 20;
Y: (ProgramPart (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n)) /. (IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n)) = (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n) . (IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n)) by COMPOS_1:38;
A12: CurInstr (ProgramPart (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n)),(Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n) = (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))) . (succ (IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))))) by A10, Y, AMI_1:54
.= goto (- 1) by A4, A1, A5, FUNCT_4:14 ;
T: ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))) = ProgramPart (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n) by AMI_1:123;
thus IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),(n + 1)) = IC (Following (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n)) by AMI_1:14
.= abs ((i + 4) + (- 4)) by A10, A12, A11, T, SCMPDS_2:66
.= IC (s2 +* ((IC s2),(succ (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 nn be Nat; :: according to AMI_1:def 20 :: thesis: ( not IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),nn) in proj1 (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))) or not CurInstr (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),nn) = halt SCMPDS )
reconsider n = nn as Element of NAT by ORDINAL1:def 13;
assume IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),nn) in dom (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))) ; :: thesis: not CurInstr (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),nn) = 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);
T: ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))) = ProgramPart (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n) by AMI_1:123;
Y: (ProgramPart (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n)) /. (IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n)) = (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n) . (IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n)) by COMPOS_1:38;

per cases ( IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n) = IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))) or IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n) = succ (IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))) ) by A15;

suppose IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n) = IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))) ; :: thesis: not CurInstr (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),nn) = halt SCMPDS

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

end;

suppose IC (Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),n) = succ (IC (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))) ; :: thesis: not CurInstr (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(Comput (ProgramPart (s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1))))),(s2 +* ((IC s2),(succ (IC s2)) --> (goto 1),(goto (- 1)))),nn) = halt SCMPDS

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

end;

end;