Theory "wellorder"

Signature

Definitions

wellfounded_def

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

wellorder_def

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

wellorder_TY_DEF

⊢ ∃rep. TYPE_DEFINITION wellorder rep

wellorder_ABSREP

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

elsOf_def

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

iseg_def

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

wobound_def

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

fromNatWO_def

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

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

orderlt_def

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

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

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

wZERO_def

⊢ wZERO = mkWO ∅

finite_def

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

remove_def

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

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

wellfounded_WF

⊢ wellfounded R ⇔ WF (CURRY R)

wellorder_EMPTY

⊢ wellorder ∅

wellorder_SING

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

rrestrict_SUBSET

⊢ rrestrict r s ⊆ r

wellfounded_subset

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

mkWO_destWO

⊢ ∀a. mkWO (destWO a) = a

destWO_mkWO

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

WIN_elsOf

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

WLE_elsOf

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

WIN_trichotomy

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

WIN_REFL

⊢ (x,x) WIN w ⇔ F

WLE_TRANS

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

WLE_ANTISYM

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

WIN_WLE

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

elsOf_WLE

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

transitive_strict

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

WIN_TRANS

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

WIN_WF

⊢ wellfounded (λp. p WIN w)

WIN_WF2

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

strict_subset

⊢ r1 ⊆ r2 ⇒ strict r1 ⊆ strict r2

transitive_rrestrict

⊢ transitive r ⇒ transitive (rrestrict r s)

antisym_rrestrict

⊢ antisym r ⇒ antisym (rrestrict r s)

linear_order_rrestrict

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

reflexive_rrestrict

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

wellorder_rrestrict

⊢ wellorder (rrestrict (destWO w) s)

WIN_wobound

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

WLE_wobound

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

wellorder_cases

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

WEXTENSION

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

wobound2

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

wellorder_fromNat

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

INJ_preserves_transitive

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

INJ_preserves_antisym

⊢ antisym r ∧ INJ f (domain r ∪ range r) t ⇒ antisym (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))

domain_IMAGE_ff

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

range_IMAGE_ff

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

INJ_preserves_wellorder

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

wellorder_fromNat_SUM

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

fromNatWO_11

⊢ fromNatWO i = fromNatWO j ⇔ i = j

elsOf_fromNatWO

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

WLE_WIN

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

elsOf_wobound

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

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_REFL

⊢ ∀w. orderiso w w

orderiso_SYM

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

orderiso_TRANS

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

orderlt_REFL

⊢ orderlt w w ⇔ F

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

orderlt_TRANS

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

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)

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

wo2wo_IN_w2

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

IMAGE_wo2wo_SUBSET

⊢ woseg w1 w2 x ⊆ elsOf w2

wo2wo_EQ_NONE

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

wo2wo_EQ_SOME_downwards

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

mono_woseg

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

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

wo2wo_mono

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

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_EQ_NONE_woseg

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

orderlt_trichotomy

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

elsOf_wZERO

⊢ elsOf wZERO = ∅

WIN_wZERO

⊢ (x,y) WIN wZERO ⇔ F

WLE_wZERO

⊢ (x,y) WLE wZERO ⇔ F

orderiso_wZERO

⊢ orderiso wZERO w ⇔ w = wZERO

elsOf_EQ_EMPTY

⊢ elsOf w = ∅ ⇔ w = wZERO

LT_wZERO

⊢ orderlt w wZERO ⇔ F

orderlt_WF

⊢ WF orderlt

orderlt_orderiso

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

finite_iso

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

finite_wZERO

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

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

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

FORALL_NUM

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

strict_UNION

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

WLE_WIN_EQ

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

wellorder_remove

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

elsOf_remove

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

WIN_remove

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

wellorder_ADD1

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

elsOf_ADD1

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

WIN_ADD1

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

elsOf_cardeq_iso

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

allsets_wellorderable

⊢ ∀s. ∃wo. elsOf wo = s