[x,y] plus (Pos x) (Pos y) --> Pos (Nat.plus x y).
[x,y] plus (Pos x) (Neg y) --> ifThenElse (Nat.greater x y) (Pos (Nat.moins x y)) (ifThenElse (Nat.eq x y) 0 (Neg (Nat.moins y x))).
[x,y] plus (Neg x) (Pos y) --> ifThenElse (Nat.greater x y) (Neg (Nat.moins x y)) (ifThenElse (Nat.eq x y) 0 (Pos (Nat.moins y x))).
[x,y] plus (Neg x) (Neg y) --> Neg (Nat.plus x y).
[x,y] plus (Pos x) (Pos y) --> Pos (natBinaire.plus x y).
[x,y] plus (Pos x) (Neg y) --> ifThenElse (natBinaire.greater x y) (Pos (natBinaire.moins x y)) (ifThenElse (natBinaire.eq x y) 0 (Neg (natBinaire.moins y x))).
[x,y] plus (Neg x) (Pos y) --> ifThenElse (natBinaire.greater x y) (Neg (natBinaire.moins x y)) (ifThenElse (natBinaire.eq x y) 0 (Pos (natBinaire.moins y x))).
[x,y] plus (Neg x) (Neg y) --> Neg (natBinaire.plus x y).
def moins : Int -> Int -> Int.
[x] moins x 0 --> x.
...
...
@@ -30,21 +30,21 @@ def moins : Int -> Int -> Int.
def mult : Int -> Int -> Int.
[] mult 0 _ --> 0.
[] mult _ 0 --> 0.
[x,y] mult (Pos x) (Pos y) --> Pos (Nat.mult x y).
[x,y] mult (Pos x) (Neg y) --> Neg (Nat.mult x y).
[x,y] mult (Neg x) (Pos y) --> Neg (Nat.mult x y).
[x,y] mult (Neg x) (Neg y) --> Pos (Nat.mult x y).
[x,y] mult (Pos x) (Pos y) --> Pos (natBinaire.mult x y).
[x,y] mult (Pos x) (Neg y) --> Neg (natBinaire.mult x y).
[x,y] mult (Neg x) (Pos y) --> Neg (natBinaire.mult x y).
[x,y] mult (Neg x) (Neg y) --> Pos (natBinaire.mult x y).
def geq : Int -> Int -> Bool.
[] geq 0 0 --> T.
[y] geq 0 (Pos y) --> F.
[y] geq 0 (Neg y) --> T.
[x] geq (Pos x) 0 --> T.
[x,y] geq (Pos x) (Pos y) --> Nat.geq x y.
[x,y] geq (Pos x) (Pos y) --> natBinaire.geq x y.
[x,y] geq (Pos x) (Neg y) --> T.
[x] geq (Neg x) 0 --> F.
[x,y] geq (Neg x) (Pos y) --> F.
[x,y] geq (Neg x) (Neg y) --> Nat.geq y x.
[x,y] geq (Neg x) (Neg y) --> natBinaire.geq y x.
#EVAL[WHNF] mult (Pos (Nat.x2 (Nat.x2plus1 Nat.1))) (Pos (Nat.x2 Nat.1)).
#EVAL[WHNF] mult (Pos (natBinaire.x2 (natBinaire.x2plus1 natBinaire.1))) (Pos (natBinaire.x2 natBinaire.1)).