new logic example: Los problem

parent 139d7f44
(* Los problem *)
theory LosProblem
type t
predicate p t t
predicate q t t
(* p and q are transitive *)
axiom p_trans: forall x y z: t. p x y -> p y z -> p x z
axiom q_trans: forall x y z: t. q x y -> q y z -> q x z
(* q is symmetric *)
axiom q_sym: forall x y: t. q x y -> q y x
(* p\/q is universal *)
axiom p_or_q: forall x y: t. p x y \/ q x y
(* show that either p or q is universal *)
goal los_problem: (forall x y: t. p x y) \/ (forall x y: t. q x y)
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover
id="0"
name="CVC3"
version="2.4.1"/>
<prover
id="1"
name="Eprover"
version="1.4"/>
<prover
id="2"
name="Spass"
version="3.7"/>
<prover
id="3"
name="Z3"
version="4.3.1"/>
<file
name="../los_problem.why"
verified="true"
expanded="true">
<theory
name="LosProblem"
locfile="../los_problem.why"
loclnum="4" loccnumb="7" loccnume="10"
verified="true"
expanded="true">
<goal
name="los_problem"
locfile="../los_problem.why"
loclnum="21" loccnumb="7" loccnume="18"
sum="33794f3860b4d7d47acff42cdf8abc48"
proved="true"
expanded="true"
shape="aqV0V1FOapV2V3F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
</file>
</why3session>
......@@ -123,11 +123,11 @@ theory MapPermut
l <= i < u -> l <= j < u -> exchange a1 a2 i j -> permut_sub a1 a2 l u
(** [permut_sub m1 m2 l u] is true when the segment
[m1(l..u-1)] is a permutation of the segment
[m2(l..u-1)]
[m2(l..u-1)].
Values outside of the interval (l..u-1) are ignored.
It is defined inductively as the smallest
equivalence relation that contains the
exchanges *)
It is defined inductively as the smallest equivalence relation
that contains the exchanges *)
lemma permut_weakening :
forall a1 a2 : map int 'a. forall l1 r1 l2 r2 : int.
......
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