module T predicate p1 predicate p2 predicate p3 axiom H: p1 -> p2 -> p3 axiom H1: p1 /\ p2 /\ p3 axiom H2: p1 \/ p2 \/ p3 goal G : (p1 \/ p2 \/ p3) -> 1 = 1 end module T2 use int.Int predicate p1 int predicate p2 int predicate p3 int axiom H: forall x. p1 x -> p2 x-> p3 x axiom H1: exists x y z. p1 x /\ p2 y /\ p3 z axiom H2: exists x. p1 x \/ exists y. p2 y \/ exists z. p3 z goal G : (forall x. p1 x \/ p2 x \/ p3 x) -> 1 = 1 end module Unsoundness predicate a predicate b predicate c (* Here if we do things badly we could use a on the right to prove the new hypothesis a on the left (and vice versa with b) This should not be provable. *) axiom H: (a -> (c /\ b)) /\ (b -> a) goal t1: c end module Incompleteness predicate a predicate b predicate c axiom H: (a -> (c /\ b)) /\ (b -> a) /\ a goal t1: c end module Imbrication predicate p1 predicate p2 predicate p3 predicate p4 predicate p5 predicate p6 predicate p7 axiom H: (p1 /\ p2) \/ (p3 /\ p4 /\ (p5 \/ p6 \/ p7)) goal G: True end (* TODO add more complex examples *) module Injection (* To avoid warning on axioms not containing local abstract symbol *) predicate p int constant z: int type t = | C int | D | E bool | F int axiom H: exists x. C x = D /\ p z axiom H1: C 1 = C 4 /\ p z axiom H2: E true = F 4 /\ p z goal G: True end module Injection2 (* To avoid warning on axioms not containing local abstract symbol *) predicate p int constant z: int type t = | C int | D | E bool | F int axiom H: exists x. C x <> D /\ p z axiom H1: C 1 <> C 4 /\ p z axiom H2: E true <> F 4 /\ p z goal G: True end