# [isabelle] Problem Axiom

```Hello,
I wish to decomposed an axiom by using intermediate definitions,
I proceed in this way, does it seem correct to you?
locale set_axioms_CLAY =  fixes less_eq :: "object ⇒ object ⇒ bool"  fixes bd00 :: "object ⇒ bool"  fixes bd01 :: "object ⇒ object ⇒ Uniset  ⇒ bool"  fixes bd02 :: "object ⇒ Uniset ⇒ bool"  fixes bd03 :: "object ⇒ object ⇒ Uniset  ⇒ bool"  defines BDOO :  " bd00(B) ≡  less_eq B B"  defines BDO1 :  "bd01 A B β ≡ (∀α. In α B & (∀C::object. In β C ⟷  (∀D. In α D ⟶ less_eq D C)& (∀D. less_eq D C ⟶ (∃E F::object. In α E & less_eq F D & less_eq F E))))"  defines BD02 : "bd02 A β ≡  (∃L. set_eq β (singleton L) & less_eq A L) "  defines  BD03: "bd03 A B β  ≡  bd00(B)  ⟶ bd01 A B β   ⟶  bd02 A β "  assumes BD04: "∀A B::object. less_eq A B  ≡ ∀ β::Uniset. BD03 A B β"begin

Here is the source axiom :lemma BDv4: "∀A B. less_eq A B  ⟷ ( (∀α β . In α B & (∀C. In β C ⟷  (∀D. In α D ⟶ less_eq D C)& (∀D. less_eq D C ⟶ (∃E F. In α E & less_eq F D &less_eq F E))) ⟶ (∃L. set_eq β (singleton L) & less_eq A L)))"

Patrick Barlatier

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.