let a be Int_position ; :: thesis: for k1, k2 being Integer holds (a,k1) <=0_goto k2 <> halt SCMPDS
let k1, k2 be Integer; :: thesis: (a,k1) <=0_goto k2 <> halt SCMPDS
InsCode ((a,k1) <=0_goto k2) = 5 by SCMPDS_2:17;
hence (a,k1) <=0_goto k2 <> halt SCMPDS by SCMPDS_2:12, SCMPDS_2:81; :: thesis: verum