let a be Int_position; :: thesis: for k1, k2 being Integer st k2 <> 5 holds
JUMP ((a,k1) >=0_goto k2) = {}
let k1, k2 be Integer; :: thesis: ( k2 <> 5 implies JUMP ((a,k1) >=0_goto k2) = {} )
set i = (a,k1) >=0_goto k2;
set X = { (NIC (((a,k1) >=0_goto k2),l)) where l is Nat : verum } ;
assume A1: k2 <> 5 ; :: thesis: JUMP ((a,k1) >=0_goto k2) = {}
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {} c= JUMP ((a,k1) >=0_goto k2)
set x1 = ((- k2) + |.k2.|) + 4;
let x be object ; :: thesis: ( x in JUMP ((a,k1) >=0_goto k2) implies b1 in {} )
assume A2: x in JUMP ((a,k1) >=0_goto k2) ; :: thesis: b1 in {}
A3: ((- k2) + |.k2.|) + 4 > ((- k2) + |.k2.|) + 0 by XREAL_1:6;
then A4: ((- k2) + |.k2.|) + 4 > 0 by ABSVALUE:27;
then reconsider x1 = ((- k2) + |.k2.|) + 4 as Element of NAT by INT_1:3;
set nl1 = |.k2.| + x1;
set nl2 = (|.k2.| + x1) + x1;
set l1 = |.k2.| + x1;
set l2 = (|.k2.| + x1) + x1;
NIC (((a,k1) >=0_goto k2),(|.k2.| + x1)) in { (NIC (((a,k1) >=0_goto k2),l)) where l is Nat : verum } ;
then x in NIC (((a,k1) >=0_goto k2),(|.k2.| + x1)) by A2, SETFAM_1:def 1;
then consider s1 being Element of product (the_Values_of SCMPDS) such that
A5: x = IC (Exec (((a,k1) >=0_goto k2),s1)) and
A6: IC s1 = |.k2.| + x1 ;
consider m1 being Element of NAT such that
A7: m1 = IC s1 and
A8: ICplusConst (s1,k2) = |.(m1 + k2).| by SCMPDS_2:def 18;
NIC (((a,k1) >=0_goto k2),((|.k2.| + x1) + x1)) in { (NIC (((a,k1) >=0_goto k2),l)) where l is Nat : verum } ;
then x in NIC (((a,k1) >=0_goto k2),((|.k2.| + x1) + x1)) by A2, SETFAM_1:def 1;
then consider s2 being Element of product (the_Values_of SCMPDS) such that
A9: x = IC (Exec (((a,k1) >=0_goto k2),s2)) and
A10: IC s2 = (|.k2.| + x1) + x1 ;
consider m2 being Element of NAT such that
A11: m2 = IC s2 and
A12: ICplusConst (s2,k2) = |.(m2 + k2).| by SCMPDS_2:def 18;
per cases ( ( s1 . (DataLoc ((s1 . a),k1)) >= 0 & s2 . (DataLoc ((s2 . a),k1)) >= 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) < 0 & s2 . (DataLoc ((s2 . a),k1)) < 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) < 0 & s2 . (DataLoc ((s2 . a),k1)) >= 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) >= 0 & s2 . (DataLoc ((s2 . a),k1)) < 0 ) ) ;
suppose that A13: s1 . (DataLoc ((s1 . a),k1)) >= 0 and
A14: s2 . (DataLoc ((s2 . a),k1)) >= 0 ; :: thesis: b1 in {}
A15: x = |.(m2 + k2).| by A9, A12, A14, SCMPDS_2:57;
A16: x = |.(m1 + k2).| by A5, A8, A13, SCMPDS_2:57;
thus x in {} :: thesis: verum
proof
per cases ( (((|.k2.| + x1) + 2) - 2) + k2 = ((((|.k2.| + x1) + x1) + 2) - 2) + k2 or (((|.k2.| + x1) + 2) - 2) + k2 = - (((((|.k2.| + x1) + x1) + 2) - 2) + k2) ) by A6, A7, A10, A11, A16, A15, ABSVALUE:28;
suppose (((|.k2.| + x1) + 2) - 2) + k2 = ((((|.k2.| + x1) + x1) + 2) - 2) + k2 ; :: thesis: x in {}
hence x in {} by A3, ABSVALUE:27; :: thesis: verum
end;
suppose (((|.k2.| + x1) + 2) - 2) + k2 = - (((((|.k2.| + x1) + x1) + 2) - 2) + k2) ; :: thesis: x in {}
hence x in {} by Lm4; :: thesis: verum
end;
end;
end;
end;
suppose that A17: s1 . (DataLoc ((s1 . a),k1)) < 0 and
A18: s2 . (DataLoc ((s2 . a),k1)) < 0 ; :: thesis: b1 in {}
A19: x = ((|.k2.| + x1) + x1) + 1 by A9, A10, A18, SCMPDS_2:57;
x = (|.k2.| + x1) + 1 by A5, A6, A17, SCMPDS_2:57;
hence x in {} by A3, A19, ABSVALUE:27; :: thesis: verum
end;
suppose that A20: s1 . (DataLoc ((s1 . a),k1)) < 0 and
A21: s2 . (DataLoc ((s2 . a),k1)) >= 0 ; :: thesis: b1 in {}
reconsider n1 = |.k2.| + x1 as Element of NAT ;
set w1 = n1;
A22: x = |.(m2 + k2).| by A9, A12, A21, SCMPDS_2:57;
A23: x = n1 + 1 by A5, A6, A20, SCMPDS_2:57
.= n1 + 1 ;
thus x in {} :: thesis: verum
proof
per cases ( n1 + 1 = m2 + k2 or n1 + 1 = - (m2 + k2) ) by A23, A22, ABSVALUE:1;
suppose n1 + 1 = m2 + k2 ; :: thesis: x in {}
then (|.k2.| + x1) + 1 = (|.k2.| + x1) + (x1 + k2) by A10, A11;
hence x in {} by Lm5; :: thesis: verum
end;
suppose n1 + 1 = - (m2 + k2) ; :: thesis: x in {}
hence x in {} by A4, A10, A11, Lm6; :: thesis: verum
end;
end;
end;
end;
suppose that A24: s1 . (DataLoc ((s1 . a),k1)) >= 0 and
A25: s2 . (DataLoc ((s2 . a),k1)) < 0 ; :: thesis: b1 in {}
reconsider n2 = (|.k2.| + x1) + x1 as Element of NAT ;
A26: x = n2 + 1 by A9, A10, A25, SCMPDS_2:57
.= n2 + 1 ;
set w2 = n2;
A27: x = |.(m1 + k2).| by A5, A8, A24, SCMPDS_2:57;
thus x in {} :: thesis: verum
proof
per cases ( n2 + 1 = m1 + k2 or n2 + 1 = - (m1 + k2) ) by A27, A26, ABSVALUE:1;
suppose n2 + 1 = m1 + k2 ; :: thesis: x in {}
hence x in {} by A1, A6, A7, Lm7; :: thesis: verum
end;
suppose n2 + 1 = - (m1 + k2) ; :: thesis: x in {}
hence x in {} by A4, A6, A7, Lm8; :: thesis: verum
end;
end;
end;
end;
end;
end;
thus {} c= JUMP ((a,k1) >=0_goto k2) ; :: thesis: verum