Why3 Standard Library index

# Relations

## Relations and orders

```theory EndoRelation
type t
predicate rel t t
end

theory Reflexive
clone export EndoRelation
axiom Refl : forall x:t. rel x x
end

theory Irreflexive
clone export EndoRelation
axiom Strict : forall x:t. not rel x x
end

theory Transitive
clone export EndoRelation
axiom Trans : forall x y z:t. rel x y -> rel y z -> rel x z
end

theory Symmetric
clone export EndoRelation
axiom Symm : forall x y:t. rel x y -> rel y x
end

theory Asymmetric
clone export EndoRelation
axiom Asymm : forall x y:t. rel x y -> not rel y x
end

theory Antisymmetric
clone export EndoRelation
axiom Antisymm : forall x y:t. rel x y -> rel y x -> x = y
end

theory Total
clone export EndoRelation
axiom Total : forall x y:t. rel x y \/ rel y x
end

theory PreOrder
clone export Reflexive
clone export Transitive with type t = t, predicate rel = rel
end

theory Equivalence
clone export PreOrder
clone export Symmetric with type t = t, predicate rel = rel
end

theory TotalPreOrder
clone export PreOrder
clone export Total with type t = t, predicate rel = rel
end

theory PartialOrder
clone export PreOrder
clone export Antisymmetric with type t = t, predicate rel = rel
end

theory TotalOrder
clone export PartialOrder
clone export Total with type t = t, predicate rel = rel
end

theory PartialStrictOrder
clone export Transitive
clone export Asymmetric with type t = t, predicate rel = rel
end

theory TotalStrictOrder
clone export PartialStrictOrder
axiom Trichotomy : forall x y:t. rel x y \/ rel y x \/ x = y
end

theory Inverse
clone export EndoRelation

predicate inv_rel (x y : t) = rel y x
end

```

## Closures

```theory ReflClosure
clone export EndoRelation

inductive relR t t =
| BaseRefl : forall x:t. relR x x
| StepRefl : forall x y:t. rel x y -> relR x y
end

theory TransClosure
clone export EndoRelation

inductive relT t t =
| BaseTrans : forall x y:t. rel x y -> relT x y
| StepTrans : forall x y z:t. relT x y -> rel y z -> relT x z

lemma relT_transitive:
forall x y z: t. relT x y -> relT y z -> relT x z
end

theory ReflTransClosure
clone export EndoRelation

inductive relTR t t =
| BaseTransRefl : forall x:t. relTR x x
| StepTransRefl : forall x y z:t. relTR x y -> rel y z -> relTR x z

lemma relTR_transitive:
forall x y z: t. relTR x y -> relTR y z -> relTR x z
end

```

## Lexicographic ordering

```theory Lex

type t1
type t2

predicate rel1 t1 t1
predicate rel2 t2 t2

inductive lex (t1, t2) (t1, t2) =
| Lex_1: forall x1 x2 : t1, y1 y2 : t2.
rel1 x1 x2 -> lex (x1,y1) (x2,y2)
| Lex_2: forall x : t1, y1 y2 : t2.
rel2 y1 y2 -> lex (x,y1) (x,y2)

end

```

## Minimum and maximum for total orders

```theory MinMax

type t
predicate le t t

clone TotalOrder with type t = t, predicate rel = le

function min (x y : t) : t = if le x y then x else y
function max (x y : t) : t = if le x y then y else x

lemma Min_r : forall x y:t. le y x -> min x y = y
lemma Max_l : forall x y:t. le y x -> max x y = x

lemma Min_comm : forall x y:t. min x y = min y x
lemma Max_comm : forall x y:t. max x y = max y x

lemma Min_assoc : forall x y z:t. min (min x y) z = min x (min y z)
lemma Max_assoc : forall x y z:t. max (max x y) z = max x (max y z)

end

```

## Well-founded relation

```theory WellFounded

type t

predicate r t t

inductive acc (x: t) =
| acc_x: forall x: t. (forall y: t. r y x -> acc y) -> acc x

axiom well_founded: forall x: t. acc x

end
```

Generated by why3doc 0.88.0