Commit b2bb8f95 authored by MARCHE Claude's avatar MARCHE Claude

example/prover: fixed remaining proofs

parent ef4bac3b
...@@ -445,6 +445,7 @@ module Impl ...@@ -445,6 +445,7 @@ module Impl
let rhoi = rho.unifier in let rhoi = rho.unifier in
let ghost stm = st tm rhoi in let ghost stm = st tm rhoi in
(*let n0 = rho.iteration in*) (*let n0 = rho.iteration in*)
bottomvar rhob rho z;
assert { rho0 z = Var_fo_term z } ; assert { rho0 z = Var_fo_term z } ;
assert { rhoi z = Var_fo_term z } ; assert { rhoi z = Var_fo_term z } ;
(*assert { forall s:int -> (fo_term int int). (*assert { forall s:int -> (fo_term int int).
......
This diff is collapsed.
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