Skip to content

Instantly share code, notes, and snippets.

@nkaretnikov

nkaretnikov/R.v

Created April 21, 2015 23:05
Show Gist options
  • Save nkaretnikov/3b382cc99cbcf0e1f196 to your computer and use it in GitHub Desktop.
Save nkaretnikov/3b382cc99cbcf0e1f196 to your computer and use it in GitHub Desktop.
Download ZIP
R
Raw
R.v
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment