Commit e4c1b1c8 authored by Michael Kohlhase's avatar Michael Kohlhase

adding wellfounded

parent d2d519cb
......@@ -32,7 +32,9 @@ theory Relations : base:?Logic =
prop_strictPartialOrder: {A} relOn A⟶ bool ❘ = [A][R] (irreflexive R) ∧ (transitive R) ❘ # strictPartialOrder 2 ❙
prop_order: {A} relOn A⟶ bool ❘ = [A][R] (partialOrder R) ∧ (total R) ❘ # order 2 ❙
prop_strictOrder: {A} relOn A⟶ bool ❘ = [A][R] (strictPartialOrder R) ∧ (total R) ❘ # strictOrder 2 ❙
prop_linearOrder: {A} relOn A⟶ bool ❘ = [A][R] (partialOrder R) ∧ ∀ [a] ∀ [b] R a b ∨ R b a ❘ # linearOrder 2 ❙
prop_wellfounded: {A} relOn A⟶ bool ❘ = [A][R] (partialOrder R) ∧ ∀ [B: set A] ∃ [b] b ∈ B ∧ ∀ [c] (R b c) ❘ # wellfounded 2 ❙
prop_wellOrder: {A} relOn A⟶ bool ❘ = [A][R] (linearOrder R) ∧ (wellfounded R) ❘ # wellOrder 2 ❙
// sameRelation: {A,B} relation A B ⟶ relation A B ⟶ bool ❘ = [A,B,f,g] (inclusion f g) ∧ (inclusion f g) ❘ # sameRelation 3 4 ❙
subrelation : {A,B} relation A B ⟶ relation A B ⟶ bool ❘ = [A,B][R,S] ∀ [x]∀[y] (R x y) ⇒ (S x y) ❘ # 3 sub 4 ❙
......
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