Commit 4eed53de authored by MARCHE Claude's avatar MARCHE Claude

Driver for Zenon Modulo: no encoding needed

parent f495fe54
......@@ -21,12 +21,7 @@ transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
transformation "discriminate"
transformation "encoding_tptp"
theory BuiltIn
syntax predicate (=) "(%1 = %2)"
meta "eliminate_algebraic" "no_index"
end
import "discrimination.gen"
......@@ -9,6 +9,10 @@ theory T
meta "rewrite" prop union_def1
goal g: mem 1 (add 2 (add 1 (add 0 empty)))
type t
constant a:t
constant b:t
constant c:t
goal g: mem a (add b (add a (add c empty)))
end
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment