Commit fb4f1710 authored by MARCHE Claude's avatar MARCHE Claude

new example logic/ffx.why

parent a216e56e
theory T
type t
predicate r t
function f t : t
axiom a : forall x:t. r x \/ r (f x)
goal g1 : exists x:t. r x /\ r (f (f x))
goal g2 : exists x:t. r x /\ r (f (f (f (f x))))
goal g3 : exists x:t. r x /\ r (f (f (f (f (f (f x))))))
goal g4 : exists x:t. r x /\ r (f (f (f (f (f (f (f (f x))))))))
goal g5 : exists x:t. r x /\ r (f (f (f (f (f (f (f (f (f (f x))))))))))
goal g6 : exists x:t. r x /\ r (f (f (f (f (f (f (f (f (f (f (f (f x))))))))))))
goal g7 : exists x:t. r x /\ r (f (f (f (f (f (f (f (f (f (f (f (f (f (f x))))))))))))))
end
\ No newline at end of file
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