Theory "wellorder"

Signature

Definitions

wZERO_def

⊢ wZERO = mkWO ∅

wobound_def

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

wo2wo_def

⊢ ∀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))

wleast_def

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

wellorder_TY_DEF

⊢ ∃rep. TYPE_DEFINITION wellorder rep

wellorder_def

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

wellorder_ABSREP

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

wellfounded_def

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

remove_def

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

poset

⊢ ∀l.
      poset l ⇔
      (∀x. fl l x ⇒ l (x,x)) ∧ (∀x y z. l (x,y) ∧ l (y,z) ⇒ l (x,z)) ∧
      ∀x y. l (x,y) ∧ l (y,x) ⇒ (x = y)

orderlt_def

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

orderiso_def

⊢ ∀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

iseg_def

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

fromNatWO_def

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

fl

⊢ ∀l x. fl l x ⇔ ∃y. l (x,y) ∨ l (y,x)

finite_def

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

elsOf_def

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

chain

⊢ ∀l P. chain l P ⇔ ∀x y. P x ∧ P y ⇒ l (x,y) ∨ l (y,x)

ADD1_def

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

Theorems

ZL_SUBSETS_BIGUNION_NONEMPTY

⊢ ∀P.
      (∃x. P x) ∧
      (∀c.
           (∃x. x ∈ c) ∧ (∀x. x ∈ c ⇒ P x) ∧
           (∀x y. x ∈ c ∧ y ∈ c ⇒ x ⊆ y ∨ y ⊆ x) ⇒
           P (BIGUNION c)) ⇒
      ∃a. P a ∧ ∀x. P x ∧ a ⊆ x ⇒ (a = x)

ZL_SUBSETS_BIGUNION

⊢ ∀P.
      (∀c.
           (∀x. x ∈ c ⇒ P x) ∧ (∀x y. x ∈ c ∧ y ∈ c ⇒ x ⊆ y ∨ y ⊆ x) ⇒
           P (BIGUNION c)) ⇒
      ∃a. P a ∧ ∀x. P x ∧ a ⊆ x ⇒ (a = x)

ZL_SUBSETS

⊢ ∀P.
      (∀c.
           (∀x. x ∈ c ⇒ P x) ∧ (∀x y. x ∈ c ∧ y ∈ c ⇒ x ⊆ y ∨ y ⊆ x) ⇒
           ∃z. P z ∧ ∀x. x ∈ c ⇒ x ⊆ z) ⇒
      ∃a. P a ∧ ∀x. P x ∧ a ⊆ x ⇒ (a = x)

ZL

⊢ ∀l.
      poset l ∧ (∃x. (λx. fl l x) x) ∧
      (∀P. chain l P ⇒ ∃y. fl l y ∧ ∀x. P x ⇒ l (x,y)) ⇒
      ∃y. fl l y ∧ ∀x. l (y,x) ⇒ (y = x)

wobounds_preserve_bijections

⊢ 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))

wobound2

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

wo_INDUCTION

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

wo2wo_thm

⊢ ∀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)

wo2wo_ONTO

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

wo2wo_mono

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

wo2wo_IN_w2

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

wo2wo_EQ_SOME_downwards

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

wo2wo_EQ_NONE_woseg

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

wo2wo_EQ_NONE

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

wo2wo_11

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

wleast_SUBSET

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

wleast_IN_wo

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

wleast_EQ_NONE

⊢ (wleast w s = NONE) ⇒ elsOf w ⊆ s

WLE_wZERO

⊢ (x,y) WLE wZERO ⇔ F

WLE_wobound

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

WLE_WIN_EQ

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

WLE_WIN

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

WLE_TRANS

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

WLE_elsOf

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

WLE_ANTISYM

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

WIN_wZERO

⊢ (x,y) WIN wZERO ⇔ F

WIN_wobound

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

WIN_WLE

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

WIN_WF2

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

WIN_WF

⊢ Wellfounded (λp. p WIN w)

WIN_trichotomy

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

WIN_TRANS

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

WIN_remove

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

WIN_REFL

⊢ (x,x) WIN w ⇔ F

WIN_elsOf

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

WIN_ADD1

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

WF_UREC_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)) ⇒
  WF $<<

WF_UREC

⊢ 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)

WF_REC_num

⊢ ∀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_REC_INVARIANT

⊢ 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

WF_REC

⊢ 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_num

⊢ WF $<

WF_IND

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

WF_EQ

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

WF_DCHAIN

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

WF

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

WEXTENSION

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

wellorder_SING

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

wellorder_rrestrict

⊢ wellorder (rrestrict (destWO w) s)

wellorder_remove

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

wellorder_fromNat_SUM

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

wellorder_fromNat

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

wellorder_EMPTY

⊢ wellorder ∅

wellorder_cases

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

wellorder_ADD1

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

wellfounded_WF

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

wellfounded_subset

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

transitive_strict

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

transitive_rrestrict

⊢ transitive r ⇒ transitive (rrestrict r s)

TARSKI_SET

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

strict_UNION

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

strict_subset

⊢ r1 ⊆ r2 ⇒ strict r1 ⊆ strict r2

seteq_wlog

⊢ ∀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)

rrestrict_SUBSET

⊢ ∀r s. rrestrict r s ⊆ r

reflexive_rrestrict

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

range_IMAGE_ff

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

POSET_RESTRICTED_SUBSET

⊢ ∀P. poset (λ(x,y). P x ∧ P y ∧ x ⊆ y)

orderlt_WF

⊢ WF orderlt

orderlt_trichotomy

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

orderlt_TRANS

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

orderlt_REFL

⊢ orderlt w w ⇔ F

orderlt_orderiso

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

orderiso_wZERO

⊢ orderiso wZERO w ⇔ (w = wZERO)

orderiso_unique

⊢ 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_TRANS

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

orderiso_thm

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

orderiso_SYM

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

orderiso_REFL

⊢ ∀w. orderiso w w

mono_woseg

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

mkWO_destWO

⊢ ∀a. mkWO (destWO a) = a

LT_wZERO

⊢ orderlt w wZERO ⇔ F

linear_order_rrestrict

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

INJECTIVE_LEFT_INVERSE_NONEMPTY

⊢ ∀f s t.
      (∃x. x ∈ s) ⇒
      ((∀x y. x ∈ s ∧ y ∈ s ∧ (f x = f y) ⇒ (x = y)) ⇔
       ∃g. (∀y. y ∈ t ⇒ g y ∈ s) ∧ ∀x. x ∈ s ⇒ (g (f x) = x))

INJ_preserves_wellorder

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

INJ_preserves_transitive

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

INJ_preserves_linear_order

⊢ 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))

INJ_preserves_antisym

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

IMAGE_wo2wo_SUBSET

⊢ woseg w1 w2 x ⊆ elsOf w2

fromNatWO_11

⊢ (fromNatWO i = fromNatWO j) ⇔ (i = j)

FORALL_NUM

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

FLATTEN_LEMMA

⊢ ∀s. (∀x. x ∈ s ⇒ (g (f x) = x)) ⇔ ∀y x. x ∈ s ∧ (y = f x) ⇒ (g y = x)

FL_RESTRICTED_SUBSET

⊢ ∀P. fl (λ(x,y). P x ∧ P y ∧ x ⊆ y) = P

finite_wZERO

⊢ finite wZERO

finite_iso

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

elsOf_wZERO

⊢ elsOf wZERO = ∅

elsOf_wobound

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

elsOf_WLE

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

elsOf_remove

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

elsOf_fromNatWO

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

elsOf_EQ_EMPTY

⊢ (elsOf w = ∅) ⇔ (w = wZERO)

elsOf_cardeq_iso

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

elsOf_ADD1

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

domain_IMAGE_ff

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

destWO_mkWO

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

antisym_rrestrict

⊢ antisym r ⇒ antisym (rrestrict r s)

allsets_wellorderable

⊢ ∀s. ∃wo. elsOf wo = s