Commit 526fe8bd authored by Francois Bobot's avatar Francois Bobot
Browse files

Fix : ajout de l'axiom oublié pour l'encodage

parent 1f621407
......@@ -11,7 +11,9 @@ theory Builtin
logic tty : ty
logic d2t(deco) : t
logic t2u(t) : undeco
axiom Conv : forall x:t[t2u(x)]. d2t(sort(tty,t2u(x)))=x
axiom Conv1 : forall x:t[sort(tty,t2u(x))]. d2t(sort(tty,t2u(x)))=x
axiom Conv2 : forall x:undeco[t2u(d2t(sort(tty,x)))].
t2u(d2t(sort(tty,x)))=x
end
theory Kept
......
Supports Markdown
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