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) = 4 by SCMPDS_2:16;
hence (a,k1) <>0_goto k2 <> halt SCMPDS by SCMPDS_2:12, SCMPDS_2:81; :: thesis: verum