diff options
Diffstat (limited to 'examples/sym_zeq.v')
| -rw-r--r-- | examples/sym_zeq.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/examples/sym_zeq.v b/examples/sym_zeq.v new file mode 100644 index 0000000..b940490 --- /dev/null +++ b/examples/sym_zeq.v @@ -0,0 +1,12 @@ +Require Import SMTCoq. +Require Import Bool. +Local Open Scope int63_scope. + +Open Scope Z_scope. + +Parameter h : Z -> Z -> Z. +Axiom h_Sm_n : forall x y, h (x+1) y =? h x y. + +Lemma h_1_0 : + h 1 0 =? h 0 0. +Proof. verit_base h_Sm_n; vauto. Qed. |