wpcalls_why.why 905 Bytes
Newer Older
François Bobot's avatar
François Bobot committed
1
theory Why2
2
  use unit_inf.Unit
François Bobot's avatar
François Bobot committed
3 4 5
  use int.Int
  use int.ComputerDivision
  use real.Real
6
  use bool_inf.Bool
Andrei Paskevich's avatar
Andrei Paskevich committed
7
  predicate eq_unit Unit.unit Unit.unit
François Bobot's avatar
François Bobot committed
8

Andrei Paskevich's avatar
Andrei Paskevich committed
9
  predicate neq_unit Unit.unit Unit.unit
François Bobot's avatar
François Bobot committed
10

Andrei Paskevich's avatar
Andrei Paskevich committed
11
  predicate eq_bool Bool.bool Bool.bool
François Bobot's avatar
François Bobot committed
12

Andrei Paskevich's avatar
Andrei Paskevich committed
13
  predicate neq_bool Bool.bool Bool.bool
François Bobot's avatar
François Bobot committed
14

Andrei Paskevich's avatar
Andrei Paskevich committed
15
  predicate lt_int int int
François Bobot's avatar
François Bobot committed
16

Andrei Paskevich's avatar
Andrei Paskevich committed
17
  predicate le_int int int
François Bobot's avatar
François Bobot committed
18

Andrei Paskevich's avatar
Andrei Paskevich committed
19
  predicate gt_int int int
François Bobot's avatar
François Bobot committed
20

Andrei Paskevich's avatar
Andrei Paskevich committed
21
  predicate ge_int int int
François Bobot's avatar
François Bobot committed
22

Andrei Paskevich's avatar
Andrei Paskevich committed
23
  predicate eq_int int int
François Bobot's avatar
François Bobot committed
24

Andrei Paskevich's avatar
Andrei Paskevich committed
25
  predicate neq_int int int
François Bobot's avatar
François Bobot committed
26

Andrei Paskevich's avatar
Andrei Paskevich committed
27
  function add_int int int : int
François Bobot's avatar
François Bobot committed
28

Andrei Paskevich's avatar
Andrei Paskevich committed
29
  function sub_int int int : int
François Bobot's avatar
François Bobot committed
30

Andrei Paskevich's avatar
Andrei Paskevich committed
31
  function mul_int int int : int
François Bobot's avatar
François Bobot committed
32

Andrei Paskevich's avatar
Andrei Paskevich committed
33
  function div_int int int : int
François Bobot's avatar
François Bobot committed
34

Andrei Paskevich's avatar
Andrei Paskevich committed
35
  function mod_int int int : int
François Bobot's avatar
François Bobot committed
36

Andrei Paskevich's avatar
Andrei Paskevich committed
37
  function neg_int int : int
François Bobot's avatar
François Bobot committed
38

Andrei Paskevich's avatar
Andrei Paskevich committed
39
  predicate zwf_zero (a : int) (b : int) = ((Int.(<=) 0 b) /\ (Int.(<) a b))
François Bobot's avatar
François Bobot committed
40 41 42 43 44 45 46 47 48 49

  goal P_po_1:
    (forall x:int.
      (forall x0:int.
        (forall x1:int.
          ((x0 = (Int.(-) 1 x : int)) ->
           ((x1 = (Int.(-) 1 x0 : int)) -> (x1 = x))))))


end