( k2 = 5 or k2 <> 5 ) ;
hence JUMP ((a,k1) >=0_goto k2) is empty by Lm13, Lm14; :: thesis: verum