Theory wellorder

⊢ ∀e w.
    ADD1 e w =
    if e ∈ elsOf w then w
    else mkWO (destWO w ∪ {(x,e) | x ∈ elsOf w} ∪ {(e,e)})

⊢ ∀w. elsOf w = domain (destWO w) ∪ wrange w

⊢ ∀w. finite w ⇔ FINITE (elsOf w)

⊢ ∀n. fromNatWO n = mkWO {(INL i,INL j) | i ≤ j ∧ j < n}

⊢ ∀w x. iseg w x = {y | (y,x) WIN w}

⊢ ∀w1 w2.
    orderiso w1 w2 ⇔
    ∃f. (∀x. x ∈ elsOf w1 ⇒ f x ∈ elsOf w2) ∧
        (∀x1 x2. x1 ∈ elsOf w1 ∧ x2 ∈ elsOf w1 ⇒ (f x1 = f x2 ⇔ x1 = x2)) ∧
        (∀y. y ∈ elsOf w2 ⇒ ∃x. x ∈ elsOf w1 ∧ f x = y) ∧
        ∀x y. (x,y) WIN w1 ⇒ (f x,f y) WIN w2

⊢ ∀w1 w2. orderlt w1 w2 ⇔ ∃x. x ∈ elsOf w2 ∧ orderiso w1 (wobound x w2)

⊢ ∀e w. remove e w = mkWO {(x,y) | x ≠ e ∧ y ≠ e ∧ (x,y) WLE w}

⊢ wZERO = mkWO ∅

⊢ ∀R. Wellfounded R ⇔
      ∀s. (∃w. w ∈ s) ⇒ ∃min. min ∈ s ∧ ∀w. (w,min) ∈ R ⇒ w ∉ s

⊢ (∀a. mkWO (destWO a) = a) ∧ ∀r. wellorder r ⇔ destWO (mkWO r) = r

⊢ ∃rep. TYPE_DEFINITION wellorder rep

⊢ ∀R. wellorder R ⇔
      Wellfounded (strict R) ∧ linear_order R (domain R ∪ range R) ∧
      reflexive R (domain R ∪ range R)

⊢ ∀w s.
    wleast w s =
    some x.
      x ∈ elsOf w ∧ x ∉ s ∧ ∀y. y ∈ elsOf w ∧ y ∉ s ∧ x ≠ y ⇒ (x,y) WIN w

⊢ ∀w1 w2.
    wo2wo w1 w2 =
    WFREC (λx y. (x,y) WIN w1)
      (λf x.
           (let
              s0 = IMAGE f (iseg w1 x);
              s1 = IMAGE THE (s0 DELETE NONE)
            in
              if s1 = elsOf w2 then NONE else wleast w2 s1))

⊢ ∀x w. wobound x w = mkWO (rrestrict (destWO w) (iseg w x))

⊢ (∀n. P n) ⇔ P 0 ∧ ∀n. P (SUC n)

⊢ woseg w1 w2 x ⊆ elsOf w2

⊢ antisym r ∧ INJ f (domain r ∪ range r) t ⇒ antisym (IMAGE (f ## f) r)

⊢ linear_order r (domain r ∪ range r) ∧ INJ f (domain r ∪ range r) t ⇒
  linear_order (IMAGE (f ## f) r) (IMAGE f (domain r ∪ range r))

⊢ transitive r ∧ INJ f (domain r ∪ range r) t ⇒
  transitive (IMAGE (f ## f) r)

⊢ wellorder r ∧ INJ f (domain r ∪ range r) t ⇒ wellorder (IMAGE (f ## f) r)

⊢ orderlt w wZERO ⇔ F

⊢ ∃R. StrongLinearOrder R ∧ WF R

⊢ ∀f. (∀s t. s ⊆ t ⇒ f s ⊆ f t) ⇒ ∃s. f s = s

⊢ w1 = w2 ⇔ ∀a b. (a,b) WLE w1 ⇔ (a,b) WLE w2

⊢ WF $<< ⇔ ∀P. (∃x. P x) ⇒ ∃x. P x ∧ ∀y. y << x ⇒ ¬P y

⊢ WF $<< ⇔ ¬∃s. ∀n. s (SUC n) << s n

⊢ WF $<< ⇔ ∀P. (∃x. P x) ⇔ ∃x. P x ∧ ∀y. y << x ⇒ ¬P y

⊢ WF $<< ⇔ ∀P. (∀x. (∀y. y << x ⇒ P y) ⇒ P x) ⇒ ∀x. P x

⊢ WF $<< ⇒
  ∀H. (∀f g x. (∀z. z << x ⇒ f z = g z) ⇒ H f x = H g x) ⇒
      ∃f. ∀x. f x = H f x

⊢ WF $<< ⇒
  ∀H S.
    (∀f g x.
       (∀z. z << x ⇒ f z = g z ∧ S z (f z)) ⇒ H f x = H g x ∧ S x (H f x)) ⇒
    ∃f. ∀x. f x = H f x

⊢ ∀H. (∀f g n. (∀m. m < n ⇒ f m = g m) ⇒ H f n = H g n) ⇒
      ∃f. ∀n. f n = H f n

⊢ WF $<< ⇒
  ∀H. (∀f g x. (∀z. z << x ⇒ f z = g z) ⇒ H f x = H g x) ⇒
      ∀f g. (∀x. f x = H f x) ∧ (∀x. g x = H g x) ⇒ f = g

⊢ (∀H. (∀f g x. (∀z. z << x ⇒ (f z ⇔ g z)) ⇒ (H f x ⇔ H g x)) ⇒
       ∀f g. (∀x. f x ⇔ H f x) ∧ (∀x. g x ⇔ H g x) ⇒ f = g) ⇒
  WF $<<

⊢ WF $<

⊢ (x,y) WIN ADD1 e w ⇔ e ∉ elsOf w ∧ x ∈ elsOf w ∧ y = e ∨ (x,y) WIN w

⊢ (x,x) WIN w ⇔ F

⊢ (x,y) WIN w ∧ (y,z) WIN w ⇒ (x,z) WIN w

⊢ Wellfounded (λp. p WIN w)

⊢ WF (λx y. (x,y) WIN w)

⊢ (x,y) WIN w ⇒ (x,y) WLE w

⊢ (x,y) WIN w ⇒ x ∈ elsOf w ∧ y ∈ elsOf w

⊢ (x,y) WIN remove e w ⇔ x ≠ e ∧ y ≠ e ∧ (x,y) WIN w

⊢ ∀x y. x ∈ elsOf w ∧ y ∈ elsOf w ⇒ (x,y) WIN w ∨ x = y ∨ (y,x) WIN w

⊢ (x,y) WIN wZERO ⇔ F

⊢ (x,y) WIN wobound z w ⇔ (x,z) WIN w ∧ (y,z) WIN w ∧ (x,y) WIN w

⊢ (x,y) WLE w ∧ (y,x) WLE w ⇒ x = y

⊢ (x,y) WLE w ∧ (y,z) WLE w ⇒ (x,z) WLE w

⊢ (x,y) WLE w ⇒ x = y ∨ (x,y) WIN w

⊢ (x,y) WLE w ⇔ x = y ∧ x ∈ elsOf w ∨ (x,y) WIN w

⊢ (x,y) WLE w ⇒ x ∈ elsOf w ∧ y ∈ elsOf w

⊢ (x,y) WLE wZERO ⇔ F

⊢ (x,y) WLE wobound z w ⇔ (x,z) WIN w ∧ (y,z) WIN w ∧ (x,y) WLE w

⊢ ∀s. ∃wo. elsOf wo = s

⊢ antisym r ⇒ antisym (rrestrict r s)

⊢ ∀r. wellorder r ⇒ destWO (mkWO r) = r

⊢ domain (IMAGE (f ## g) r) = IMAGE f (domain r)

⊢ elsOf (ADD1 e w) = e INSERT elsOf w

⊢ elsOf w = ∅ ⇔ w = wZERO

⊢ x ∈ elsOf w ⇔ (x,x) WLE w

⊢ INJ f (elsOf wo) 𝕌(:α) ⇒ ∃wo'. orderiso wo wo'

⊢ elsOf (fromNatWO n) = IMAGE INL (count n)

⊢ elsOf (remove e w) = elsOf w DELETE e

⊢ elsOf wZERO = ∅

⊢ elsOf (wobound x w) = {y | (y,x) WIN w}

⊢ orderiso w1 w2 ⇒ (finite w1 ⇔ finite w2)

⊢ finite wZERO

⊢ fromNatWO i = fromNatWO j ⇔ i = j

⊢ linear_order r (domain r ∪ range r) ⇒
  linear_order (rrestrict r s)
    (domain (rrestrict r s) ∪ range (rrestrict r s))

⊢ ∀a. mkWO (destWO a) = a

⊢ (x1,x2) WIN w1 ⇒ woseg w1 w2 x1 ⊆ woseg w1 w2 x2

⊢ ∀w. orderiso w w

⊢ ∀w1 w2. orderiso w1 w2 ⇒ orderiso w2 w1

⊢ ∀w1 w2 w3. orderiso w1 w2 ∧ orderiso w2 w3 ⇒ orderiso w1 w3

⊢ orderiso w1 w2 ⇔
  ∃f. BIJ f (elsOf w1) (elsOf w2) ∧ ∀x y. (x,y) WIN w1 ⇒ (f x,f y) WIN w2

⊢ BIJ f1 (elsOf w1) (elsOf w2) ∧ BIJ f2 (elsOf w1) (elsOf w2) ∧
  (∀x y. (x,y) WIN w1 ⇒ (f1 x,f1 y) WIN w2) ∧
  (∀x y. (x,y) WIN w1 ⇒ (f2 x,f2 y) WIN w2) ⇒
  ∀x. x ∈ elsOf w1 ⇒ f1 x = f2 x

⊢ orderiso wZERO w ⇔ w = wZERO

⊢ orderlt w w ⇔ F

⊢ ∀w1 w2 w3. orderlt w1 w2 ∧ orderlt w2 w3 ⇒ orderlt w1 w3

⊢ WF orderlt

⊢ orderiso x0 y0 ∧ orderiso a0 b0 ⇒ (orderlt x0 a0 ⇔ orderlt y0 b0)

⊢ orderlt w1 w2 ∨ orderiso w1 w2 ∨ orderlt w2 w1

⊢ range (IMAGE (f ## g) r) = IMAGE g (range r)

⊢ reflexive r (domain r ∪ range r) ⇒
  reflexive (rrestrict r s)
    (domain (rrestrict r s) ∪ range (rrestrict r s))

⊢ ∀r s. rrestrict r s ⊆ r

⊢ ∀f. (∀a b. P a b ⇒ P b a) ∧ (∀x a b. P a b ∧ x ∈ f a ⇒ x ∈ f b) ⇒
      ∀a b. P a b ⇒ f a = f b

⊢ strict (r1 ∪ r2) = strict r1 ∪ strict r2

⊢ r1 ⊆ r2 ⇒ strict r1 ⊆ strict r2

⊢ transitive r ⇒ transitive (rrestrict r s)

⊢ transitive r ∧ antisym r ⇒ transitive (strict r)

⊢ ∀R. Wellfounded R ⇔ WF (CURRY R)

⊢ ∀r0 r. Wellfounded r ∧ r0 ⊆ r ⇒ Wellfounded r0

⊢ e ∉ elsOf w ⇒ wellorder (destWO w ∪ {(x,e) | x ∈ elsOf w} ∪ {(e,e)})

⊢ wellorder ∅

⊢ ∀x y. wellorder {(x,y)} ⇔ x = y

⊢ ∀w. ∃s. wellorder s ∧ w = mkWO s

⊢ wellorder {(i,j) | i ≤ j ∧ j < n}

⊢ wellorder {(INL i,INL j) | i ≤ j ∧ j < n}

⊢ wellorder {(x,y) | x ≠ e ∧ y ≠ e ∧ (x,y) WLE w}

⊢ wellorder (rrestrict (destWO w) s)

⊢ wleast w s = NONE ⇒ elsOf w ⊆ s

⊢ wleast w s = SOME x ⇒
  x ∈ elsOf w ∧ x ∉ s ∧ ∀y. y ∈ elsOf w ∧ y ∉ s ∧ x ≠ y ⇒ (x,y) WIN w

⊢ wleast w s1 = SOME x ∧ wleast w s2 = SOME y ∧ s1 ⊆ s2 ⇒
  x = y ∨ (x,y) WIN w

⊢ x1 ∈ elsOf w1 ∧ x2 ∈ elsOf w1 ∧ wo2wo w1 w2 x1 = SOME y ∧
  wo2wo w1 w2 x2 = SOME y ⇒
  x1 = x2

⊢ ∀x. wo2wo w1 w2 x = NONE ⇒ ∀y. (x,y) WIN w1 ⇒ wo2wo w1 w2 y = NONE

⊢ wo2wo w1 w2 x = NONE ⇒ elsOf w2 = woseg w1 w2 x

⊢ ∀x y.
    wo2wo w1 w2 x = SOME y ⇒
    ∀x0. (x0,x) WIN w1 ⇒ ∃y0. wo2wo w1 w2 x0 = SOME y0

⊢ ∀x y. wo2wo w1 w2 x = SOME y ⇒ y ∈ elsOf w2

⊢ x ∈ elsOf w1 ∧ wo2wo w1 w2 x = SOME y ∧ (y0,y) WIN w2 ⇒
  ∃x0. x0 ∈ elsOf w1 ∧ wo2wo w1 w2 x0 = SOME y0

⊢ wo2wo w1 w2 x0 = SOME y0 ∧ wo2wo w1 w2 x = SOME y ∧ (x0,x) WIN w1 ⇒
  (y0,y) WIN w2

⊢ ∀x. wo2wo w w2 x =
      (let
         s0 = IMAGE (wo2wo w w2) (iseg w x);
         s1 = IMAGE THE (s0 DELETE NONE)
       in
         if s1 = elsOf w2 then NONE else wleast w2 s1)

⊢ ∀P w.
    (∀x. (∀y. (y,x) WIN w ⇒ y ∈ elsOf w ⇒ P y) ⇒ x ∈ elsOf w ⇒ P x) ⇒
    ∀x. x ∈ elsOf w ⇒ P x

⊢ (a,b) WIN w ⇒ wobound a (wobound b w) = wobound a w

⊢ BIJ f (elsOf w1) (elsOf w2) ∧ x ∈ elsOf w1 ∧
  (∀x y. (x,y) WIN w1 ⇒ (f x,f y) WIN w2) ⇒
  BIJ f (elsOf (wobound x w1)) (elsOf (wobound (f x) w2))