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