Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- Inductive R : nat -> nat -> nat -> Prop :=
- | c1 : R 0 0 0
- | c2 : forall m n o, R m n o -> R (S m) n (S o)
- | c3 : forall m n o, R m n o -> R m (S n) (S o)
- | c4 : forall m n o, R (S m) (S n) (S (S o)) -> R m n o
- | c5 : forall m n o, R m n o -> R n m o.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement