Structure wellorderTheory

signature wellorderTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val ADD1_def : thm
    val chain : thm
    val elsOf_def : thm
    val finite_def : thm
    val fl : thm
    val fromNatWO_def : thm
    val iseg_def : thm
    val orderiso_def : thm
    val orderlt_def : thm
    val poset : thm
    val remove_def : thm
    val wZERO_def : thm
    val wellfounded_def : thm
    val wellorder_ABSREP : thm
    val wellorder_TY_DEF : thm
    val wellorder_def : thm
    val wleast_def : thm
    val wo2wo_def : thm
    val wobound_def : thm
  
  (*  Theorems  *)
    val FLATTEN_LEMMA : thm
    val FL_RESTRICTED_SUBSET : thm
    val FORALL_NUM : thm
    val IMAGE_wo2wo_SUBSET : thm
    val INJECTIVE_LEFT_INVERSE_NONEMPTY : thm
    val INJ_preserves_antisym : thm
    val INJ_preserves_linear_order : thm
    val INJ_preserves_transitive : thm
    val INJ_preserves_wellorder : thm
    val LT_wZERO : thm
    val POSET_RESTRICTED_SUBSET : thm
    val TARSKI_SET : thm
    val WEXTENSION : thm
    val WF : thm
    val WF_DCHAIN : thm
    val WF_EQ : thm
    val WF_IND : thm
    val WF_REC : thm
    val WF_REC_INVARIANT : thm
    val WF_REC_num : thm
    val WF_UREC : thm
    val WF_UREC_WF : thm
    val WF_num : thm
    val WIN_ADD1 : thm
    val WIN_REFL : thm
    val WIN_TRANS : thm
    val WIN_WF : thm
    val WIN_WF2 : thm
    val WIN_WLE : thm
    val WIN_elsOf : thm
    val WIN_remove : thm
    val WIN_trichotomy : thm
    val WIN_wZERO : thm
    val WIN_wobound : thm
    val WLE_ANTISYM : thm
    val WLE_TRANS : thm
    val WLE_WIN : thm
    val WLE_WIN_EQ : thm
    val WLE_elsOf : thm
    val WLE_wZERO : thm
    val WLE_wobound : thm
    val ZL : thm
    val ZL_SUBSETS : thm
    val ZL_SUBSETS_BIGUNION : thm
    val ZL_SUBSETS_BIGUNION_NONEMPTY : thm
    val allsets_wellorderable : thm
    val antisym_rrestrict : thm
    val destWO_mkWO : thm
    val domain_IMAGE_ff : thm
    val elsOf_ADD1 : thm
    val elsOf_EQ_EMPTY : thm
    val elsOf_WLE : thm
    val elsOf_cardeq_iso : thm
    val elsOf_fromNatWO : thm
    val elsOf_remove : thm
    val elsOf_wZERO : thm
    val elsOf_wobound : thm
    val finite_iso : thm
    val finite_wZERO : thm
    val fromNatWO_11 : thm
    val linear_order_rrestrict : thm
    val mkWO_destWO : thm
    val mono_woseg : thm
    val orderiso_REFL : thm
    val orderiso_SYM : thm
    val orderiso_TRANS : thm
    val orderiso_thm : thm
    val orderiso_unique : thm
    val orderiso_wZERO : thm
    val orderlt_REFL : thm
    val orderlt_TRANS : thm
    val orderlt_WF : thm
    val orderlt_orderiso : thm
    val orderlt_trichotomy : thm
    val range_IMAGE_ff : thm
    val reflexive_rrestrict : thm
    val rrestrict_SUBSET : thm
    val seteq_wlog : thm
    val strict_UNION : thm
    val strict_subset : thm
    val transitive_rrestrict : thm
    val transitive_strict : thm
    val wellfounded_WF : thm
    val wellfounded_subset : thm
    val wellorder_ADD1 : thm
    val wellorder_EMPTY : thm
    val wellorder_SING : thm
    val wellorder_cases : thm
    val wellorder_fromNat : thm
    val wellorder_fromNat_SUM : thm
    val wellorder_remove : thm
    val wellorder_rrestrict : thm
    val wleast_EQ_NONE : thm
    val wleast_IN_wo : thm
    val wleast_SUBSET : thm
    val wo2wo_11 : thm
    val wo2wo_EQ_NONE : thm
    val wo2wo_EQ_NONE_woseg : thm
    val wo2wo_EQ_SOME_downwards : thm
    val wo2wo_IN_w2 : thm
    val wo2wo_ONTO : thm
    val wo2wo_mono : thm
    val wo2wo_thm : thm
    val wo_INDUCTION : thm
    val wobound2 : thm
    val wobounds_preserve_bijections : thm
  
  val wellorder_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [indexedLists] Parent theory of "wellorder"
   
   [patternMatches] Parent theory of "wellorder"
   
   [set_relation] Parent theory of "wellorder"
   
   [ADD1_def]  Definition
      
      ⊢ ∀e w.
          ADD1 e w =
          if e ∈ elsOf w then w
          else mkWO (destWO w ∪ {(x,e) | x ∈ elsOf w} ∪ {(e,e)})
   
   [chain]  Definition
      
      ⊢ ∀l P. chain l P ⇔ ∀x y. P x ∧ P y ⇒ l (x,y) ∨ l (y,x)
   
   [elsOf_def]  Definition
      
      ⊢ ∀w. elsOf w = domain (destWO w) ∪ wrange w
   
   [finite_def]  Definition
      
      ⊢ ∀w. finite w ⇔ FINITE (elsOf w)
   
   [fl]  Definition
      
      ⊢ ∀l x. fl l x ⇔ ∃y. l (x,y) ∨ l (y,x)
   
   [fromNatWO_def]  Definition
      
      ⊢ ∀n. fromNatWO n = mkWO {(INL i,INL j) | i ≤ j ∧ j < n}
   
   [iseg_def]  Definition
      
      ⊢ ∀w x. iseg w x = {y | (y,x) WIN w}
   
   [orderiso_def]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀w1 w2.
          orderlt w1 w2 ⇔ ∃x. x ∈ elsOf w2 ∧ orderiso w1 (wobound x w2)
   
   [poset]  Definition
      
      ⊢ ∀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
   
   [remove_def]  Definition
      
      ⊢ ∀e w. remove e w = mkWO {(x,y) | x ≠ e ∧ y ≠ e ∧ (x,y) WLE w}
   
   [wZERO_def]  Definition
      
      ⊢ wZERO = mkWO ∅
   
   [wellfounded_def]  Definition
      
      ⊢ ∀R. Wellfounded R ⇔
            ∀s. (∃w. w ∈ s) ⇒ ∃min. min ∈ s ∧ ∀w. (w,min) ∈ R ⇒ w ∉ s
   
   [wellorder_ABSREP]  Definition
      
      ⊢ (∀a. mkWO (destWO a) = a) ∧ ∀r. wellorder r ⇔ destWO (mkWO r) = r
   
   [wellorder_TY_DEF]  Definition
      
      ⊢ ∃rep. TYPE_DEFINITION wellorder rep
   
   [wellorder_def]  Definition
      
      ⊢ ∀R. wellorder R ⇔
            Wellfounded (strict R) ∧ linear_order R (domain R ∪ range R) ∧
            reflexive R (domain R ∪ range R)
   
   [wleast_def]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀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))
   
   [wobound_def]  Definition
      
      ⊢ ∀x w. wobound x w = mkWO (rrestrict (destWO w) (iseg w x))
   
   [FLATTEN_LEMMA]  Theorem
      
      ⊢ ∀s. (∀x. x ∈ s ⇒ g (f x) = x) ⇔ ∀y x. x ∈ s ∧ y = f x ⇒ g y = x
   
   [FL_RESTRICTED_SUBSET]  Theorem
      
      ⊢ ∀P. fl (λ(x,y). P x ∧ P y ∧ x ⊆ y) = P
   
   [FORALL_NUM]  Theorem
      
      ⊢ (∀n. P n) ⇔ P 0 ∧ ∀n. P (SUC n)
   
   [IMAGE_wo2wo_SUBSET]  Theorem
      
      ⊢ woseg w1 w2 x ⊆ elsOf w2
   
   [INJECTIVE_LEFT_INVERSE_NONEMPTY]  Theorem
      
      ⊢ ∀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_antisym]  Theorem
      
      ⊢ antisym r ∧ INJ f (domain r ∪ range r) t ⇒
        antisym (IMAGE (f ## f) r)
   
   [INJ_preserves_linear_order]  Theorem
      
      ⊢ 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_transitive]  Theorem
      
      ⊢ transitive r ∧ INJ f (domain r ∪ range r) t ⇒
        transitive (IMAGE (f ## f) r)
   
   [INJ_preserves_wellorder]  Theorem
      
      ⊢ wellorder r ∧ INJ f (domain r ∪ range r) t ⇒
        wellorder (IMAGE (f ## f) r)
   
   [LT_wZERO]  Theorem
      
      ⊢ orderlt w wZERO ⇔ F
   
   [POSET_RESTRICTED_SUBSET]  Theorem
      
      ⊢ ∀P. poset (λ(x,y). P x ∧ P y ∧ x ⊆ y)
   
   [TARSKI_SET]  Theorem
      
      ⊢ ∀f. (∀s t. s ⊆ t ⇒ f s ⊆ f t) ⇒ ∃s. f s = s
   
   [WEXTENSION]  Theorem
      
      ⊢ w1 = w2 ⇔ ∀a b. (a,b) WLE w1 ⇔ (a,b) WLE w2
   
   [WF]  Theorem
      
      ⊢ WF $<< ⇔ ∀P. (∃x. P x) ⇒ ∃x. P x ∧ ∀y. y << x ⇒ ¬P y
   
   [WF_DCHAIN]  Theorem
      
      ⊢ WF $<< ⇔ ¬∃s. ∀n. s (SUC n) << s n
   
   [WF_EQ]  Theorem
      
      ⊢ WF $<< ⇔ ∀P. (∃x. P x) ⇔ ∃x. P x ∧ ∀y. y << x ⇒ ¬P y
   
   [WF_IND]  Theorem
      
      ⊢ WF $<< ⇔ ∀P. (∀x. (∀y. y << x ⇒ P y) ⇒ P x) ⇒ ∀x. P x
   
   [WF_REC]  Theorem
      
      ⊢ 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_REC_INVARIANT]  Theorem
      
      ⊢ 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_num]  Theorem
      
      ⊢ ∀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_UREC]  Theorem
      
      ⊢ 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_UREC_WF]  Theorem
      
      ⊢ (∀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_num]  Theorem
      
      ⊢ WF $<
   
   [WIN_ADD1]  Theorem
      
      ⊢ (x,y) WIN ADD1 e w ⇔
        e ∉ elsOf w ∧ x ∈ elsOf w ∧ y = e ∨ (x,y) WIN w
   
   [WIN_REFL]  Theorem
      
      ⊢ (x,x) WIN w ⇔ F
   
   [WIN_TRANS]  Theorem
      
      ⊢ (x,y) WIN w ∧ (y,z) WIN w ⇒ (x,z) WIN w
   
   [WIN_WF]  Theorem
      
      ⊢ Wellfounded (λp. p WIN w)
   
   [WIN_WF2]  Theorem
      
      ⊢ WF (λx y. (x,y) WIN w)
   
   [WIN_WLE]  Theorem
      
      ⊢ (x,y) WIN w ⇒ (x,y) WLE w
   
   [WIN_elsOf]  Theorem
      
      ⊢ (x,y) WIN w ⇒ x ∈ elsOf w ∧ y ∈ elsOf w
   
   [WIN_remove]  Theorem
      
      ⊢ (x,y) WIN remove e w ⇔ x ≠ e ∧ y ≠ e ∧ (x,y) WIN w
   
   [WIN_trichotomy]  Theorem
      
      ⊢ ∀x y. x ∈ elsOf w ∧ y ∈ elsOf w ⇒ (x,y) WIN w ∨ x = y ∨ (y,x) WIN w
   
   [WIN_wZERO]  Theorem
      
      ⊢ (x,y) WIN wZERO ⇔ F
   
   [WIN_wobound]  Theorem
      
      ⊢ (x,y) WIN wobound z w ⇔ (x,z) WIN w ∧ (y,z) WIN w ∧ (x,y) WIN w
   
   [WLE_ANTISYM]  Theorem
      
      ⊢ (x,y) WLE w ∧ (y,x) WLE w ⇒ x = y
   
   [WLE_TRANS]  Theorem
      
      ⊢ (x,y) WLE w ∧ (y,z) WLE w ⇒ (x,z) WLE w
   
   [WLE_WIN]  Theorem
      
      ⊢ (x,y) WLE w ⇒ x = y ∨ (x,y) WIN w
   
   [WLE_WIN_EQ]  Theorem
      
      ⊢ (x,y) WLE w ⇔ x = y ∧ x ∈ elsOf w ∨ (x,y) WIN w
   
   [WLE_elsOf]  Theorem
      
      ⊢ (x,y) WLE w ⇒ x ∈ elsOf w ∧ y ∈ elsOf w
   
   [WLE_wZERO]  Theorem
      
      ⊢ (x,y) WLE wZERO ⇔ F
   
   [WLE_wobound]  Theorem
      
      ⊢ (x,y) WLE wobound z w ⇔ (x,z) WIN w ∧ (y,z) WIN w ∧ (x,y) WLE w
   
   [ZL]  Theorem
      
      ⊢ ∀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
   
   [ZL_SUBSETS]  Theorem
      
      ⊢ ∀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_SUBSETS_BIGUNION]  Theorem
      
      ⊢ ∀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_BIGUNION_NONEMPTY]  Theorem
      
      ⊢ ∀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
   
   [allsets_wellorderable]  Theorem
      
      ⊢ ∀s. ∃wo. elsOf wo = s
   
   [antisym_rrestrict]  Theorem
      
      ⊢ antisym r ⇒ antisym (rrestrict r s)
   
   [destWO_mkWO]  Theorem
      
      ⊢ ∀r. wellorder r ⇒ destWO (mkWO r) = r
   
   [domain_IMAGE_ff]  Theorem
      
      ⊢ domain (IMAGE (f ## g) r) = IMAGE f (domain r)
   
   [elsOf_ADD1]  Theorem
      
      ⊢ elsOf (ADD1 e w) = e INSERT elsOf w
   
   [elsOf_EQ_EMPTY]  Theorem
      
      ⊢ elsOf w = ∅ ⇔ w = wZERO
   
   [elsOf_WLE]  Theorem
      
      ⊢ x ∈ elsOf w ⇔ (x,x) WLE w
   
   [elsOf_cardeq_iso]  Theorem
      
      ⊢ INJ f (elsOf wo) 𝕌(:α) ⇒ ∃wo'. orderiso wo wo'
   
   [elsOf_fromNatWO]  Theorem
      
      ⊢ elsOf (fromNatWO n) = IMAGE INL (count n)
   
   [elsOf_remove]  Theorem
      
      ⊢ elsOf (remove e w) = elsOf w DELETE e
   
   [elsOf_wZERO]  Theorem
      
      ⊢ elsOf wZERO = ∅
   
   [elsOf_wobound]  Theorem
      
      ⊢ elsOf (wobound x w) = {y | (y,x) WIN w}
   
   [finite_iso]  Theorem
      
      ⊢ orderiso w1 w2 ⇒ (finite w1 ⇔ finite w2)
   
   [finite_wZERO]  Theorem
      
      ⊢ finite wZERO
   
   [fromNatWO_11]  Theorem
      
      ⊢ fromNatWO i = fromNatWO j ⇔ i = j
   
   [linear_order_rrestrict]  Theorem
      
      ⊢ linear_order r (domain r ∪ range r) ⇒
        linear_order (rrestrict r s)
          (domain (rrestrict r s) ∪ range (rrestrict r s))
   
   [mkWO_destWO]  Theorem
      
      ⊢ ∀a. mkWO (destWO a) = a
   
   [mono_woseg]  Theorem
      
      ⊢ (x1,x2) WIN w1 ⇒ woseg w1 w2 x1 ⊆ woseg w1 w2 x2
   
   [orderiso_REFL]  Theorem
      
      ⊢ ∀w. orderiso w w
   
   [orderiso_SYM]  Theorem
      
      ⊢ ∀w1 w2. orderiso w1 w2 ⇒ orderiso w2 w1
   
   [orderiso_TRANS]  Theorem
      
      ⊢ ∀w1 w2 w3. orderiso w1 w2 ∧ orderiso w2 w3 ⇒ orderiso w1 w3
   
   [orderiso_thm]  Theorem
      
      ⊢ orderiso w1 w2 ⇔
        ∃f. BIJ f (elsOf w1) (elsOf w2) ∧
            ∀x y. (x,y) WIN w1 ⇒ (f x,f y) WIN w2
   
   [orderiso_unique]  Theorem
      
      ⊢ 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]  Theorem
      
      ⊢ orderiso wZERO w ⇔ w = wZERO
   
   [orderlt_REFL]  Theorem
      
      ⊢ orderlt w w ⇔ F
   
   [orderlt_TRANS]  Theorem
      
      ⊢ ∀w1 w2 w3. orderlt w1 w2 ∧ orderlt w2 w3 ⇒ orderlt w1 w3
   
   [orderlt_WF]  Theorem
      
      ⊢ WF orderlt
   
   [orderlt_orderiso]  Theorem
      
      ⊢ orderiso x0 y0 ∧ orderiso a0 b0 ⇒ (orderlt x0 a0 ⇔ orderlt y0 b0)
   
   [orderlt_trichotomy]  Theorem
      
      ⊢ orderlt w1 w2 ∨ orderiso w1 w2 ∨ orderlt w2 w1
   
   [range_IMAGE_ff]  Theorem
      
      ⊢ range (IMAGE (f ## g) r) = IMAGE g (range r)
   
   [reflexive_rrestrict]  Theorem
      
      ⊢ reflexive r (domain r ∪ range r) ⇒
        reflexive (rrestrict r s)
          (domain (rrestrict r s) ∪ range (rrestrict r s))
   
   [rrestrict_SUBSET]  Theorem
      
      ⊢ ∀r s. rrestrict r s ⊆ r
   
   [seteq_wlog]  Theorem
      
      ⊢ ∀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_UNION]  Theorem
      
      ⊢ strict (r1 ∪ r2) = strict r1 ∪ strict r2
   
   [strict_subset]  Theorem
      
      ⊢ r1 ⊆ r2 ⇒ strict r1 ⊆ strict r2
   
   [transitive_rrestrict]  Theorem
      
      ⊢ transitive r ⇒ transitive (rrestrict r s)
   
   [transitive_strict]  Theorem
      
      ⊢ transitive r ∧ antisym r ⇒ transitive (strict r)
   
   [wellfounded_WF]  Theorem
      
      ⊢ ∀R. Wellfounded R ⇔ WF (CURRY R)
   
   [wellfounded_subset]  Theorem
      
      ⊢ ∀r0 r. Wellfounded r ∧ r0 ⊆ r ⇒ Wellfounded r0
   
   [wellorder_ADD1]  Theorem
      
      ⊢ e ∉ elsOf w ⇒
        wellorder (destWO w ∪ {(x,e) | x ∈ elsOf w} ∪ {(e,e)})
   
   [wellorder_EMPTY]  Theorem
      
      ⊢ wellorder ∅
   
   [wellorder_SING]  Theorem
      
      ⊢ ∀x y. wellorder {(x,y)} ⇔ x = y
   
   [wellorder_cases]  Theorem
      
      ⊢ ∀w. ∃s. wellorder s ∧ w = mkWO s
   
   [wellorder_fromNat]  Theorem
      
      ⊢ wellorder {(i,j) | i ≤ j ∧ j < n}
   
   [wellorder_fromNat_SUM]  Theorem
      
      ⊢ wellorder {(INL i,INL j) | i ≤ j ∧ j < n}
   
   [wellorder_remove]  Theorem
      
      ⊢ wellorder {(x,y) | x ≠ e ∧ y ≠ e ∧ (x,y) WLE w}
   
   [wellorder_rrestrict]  Theorem
      
      ⊢ wellorder (rrestrict (destWO w) s)
   
   [wleast_EQ_NONE]  Theorem
      
      ⊢ wleast w s = NONE ⇒ elsOf w ⊆ s
   
   [wleast_IN_wo]  Theorem
      
      ⊢ wleast w s = SOME x ⇒
        x ∈ elsOf w ∧ x ∉ s ∧ ∀y. y ∈ elsOf w ∧ y ∉ s ∧ x ≠ y ⇒ (x,y) WIN w
   
   [wleast_SUBSET]  Theorem
      
      ⊢ wleast w s1 = SOME x ∧ wleast w s2 = SOME y ∧ s1 ⊆ s2 ⇒
        x = y ∨ (x,y) WIN w
   
   [wo2wo_11]  Theorem
      
      ⊢ x1 ∈ elsOf w1 ∧ x2 ∈ elsOf w1 ∧ wo2wo w1 w2 x1 = SOME y ∧
        wo2wo w1 w2 x2 = SOME y ⇒
        x1 = x2
   
   [wo2wo_EQ_NONE]  Theorem
      
      ⊢ ∀x. wo2wo w1 w2 x = NONE ⇒ ∀y. (x,y) WIN w1 ⇒ wo2wo w1 w2 y = NONE
   
   [wo2wo_EQ_NONE_woseg]  Theorem
      
      ⊢ wo2wo w1 w2 x = NONE ⇒ elsOf w2 = woseg w1 w2 x
   
   [wo2wo_EQ_SOME_downwards]  Theorem
      
      ⊢ ∀x y.
          wo2wo w1 w2 x = SOME y ⇒
          ∀x0. (x0,x) WIN w1 ⇒ ∃y0. wo2wo w1 w2 x0 = SOME y0
   
   [wo2wo_IN_w2]  Theorem
      
      ⊢ ∀x y. wo2wo w1 w2 x = SOME y ⇒ y ∈ elsOf w2
   
   [wo2wo_ONTO]  Theorem
      
      ⊢ 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]  Theorem
      
      ⊢ wo2wo w1 w2 x0 = SOME y0 ∧ wo2wo w1 w2 x = SOME y ∧ (x0,x) WIN w1 ⇒
        (y0,y) WIN w2
   
   [wo2wo_thm]  Theorem
      
      ⊢ ∀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)
   
   [wo_INDUCTION]  Theorem
      
      ⊢ ∀P w.
          (∀x. (∀y. (y,x) WIN w ⇒ y ∈ elsOf w ⇒ P y) ⇒ x ∈ elsOf w ⇒ P x) ⇒
          ∀x. x ∈ elsOf w ⇒ P x
   
   [wobound2]  Theorem
      
      ⊢ (a,b) WIN w ⇒ wobound a (wobound b w) = wobound a w
   
   [wobounds_preserve_bijections]  Theorem
      
      ⊢ 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))
   
   
*)
end

HOL 4, Kananaskis-14