Commit d2d519cb authored by Michael Kohlhase's avatar Michael Kohlhase

adding wellfounded

parent 0db711e4
......@@ -32,6 +32,7 @@ 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_wellfounded: {A} relOn A⟶ bool ❘ = [A][R] (partialOrder R) ∧ ∀ [B: set A] ∃ [b] b ∈ B ∧ ∀ [c] (R b c) ❘ # wellfounded 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