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 EXTPRO_1:4
.= 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 EXTPRO_1:4
.= 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 EXTPRO_1:def 7 :: 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 EXTPRO_1:3;
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 ;
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 by T, SCMPDS_2:85; :: 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 ;
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 by T, SCMPDS_2:85; :: thesis: verum

end;

end;