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:27;
hence a,k1 >=0_goto k2 <> halt SCMPDS by SCMPDS_2:21, SCMPDS_2:93; :: thesis: verum