$$$zorn2.pvs
zorn2 [ T: TYPE ] : THEORY

  BEGIN

  IMPORTING zorn

  X, Y: VAR set[T]

  A, B, C: VAR set[set[T]]

  chain?(A): bool =
     FORALL (X, Y: (A)): subset?(X, Y) or subset?(Y, X)


  %----------------------------------------
  %  Specializations of Zorn's Lemma 
  %  when order relation = set inclusion  
  %-----------------------------------------

  zorn_subset: LEMMA 
      (FORALL A: subset?(A, C) and chain?(A) IMPLIES 
	  EXISTS (X:(C)) : FORALL (Y: (A)): subset?(Y, X))
    IMPLIES 
        EXISTS (X: (C)): FORALL (Y: (C)): subset?(X, Y) IMPLIES Y=X

  zorn_subset2: LEMMA
      (FORALL A: subset?(A, C) AND chain?(A) IMPLIES C(union(A)))
    IMPLIES 
        EXISTS (X: (C)): FORALL (Y: (C)): subset?(X, Y) IMPLIES Y=X


  END zorn2

$$$zorn2.prf
(|zorn2|
 (|zorn_subset| "" (SKOSIMP)
  (("" (LEMMA "zorn[(C!1), lambda (X, Y:(C!1)): subset?(X, Y)]")
    (("1" (GROUND)
      (("1" (DELETE -2) (("1" (REDUCE :INSTANTIATOR INST!) NIL NIL))
        NIL)
       ("2" (DELETE 2)
        (("2" (SKOSIMP)
          (("2" (INST - "{ X | C!1(X) AND A!1(X) }")
            (("2" (GROUND)
              (("1" (DELETE -2)
                (("1" (GRIND :EXCLUDE "subset?" :INSTANTIATOR INST!)
                  NIL NIL))
                NIL)
               ("2" (DELETE -1 2) (("2" (GRIND) NIL NIL)) NIL)
               ("3" (DELETE 2)
                (("3" (GRIND :EXCLUDE "subset?") NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (DELETE -1 2)
      (("2" (GRIND)
        (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (REDUCE) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|zorn_subset2| "" (AUTO-REWRITE "union_upper_bound[T]")
  (("" (SKOSIMP)
    (("" (REWRITE "zorn_subset")
      (("" (DELETE 2) (("" (REDUCE :INSTANTIATOR INST!) NIL NIL)) NIL))
      NIL))
    NIL))
  NIL))


$$$well_ordering.pvs
well_ordering  [ T : TYPE ] : THEORY

  BEGIN

  R : VAR [T, T -> bool]

  x, y, z : VAR T


  %-------------------------------
  %  Definition of well ordering
  %-------------------------------

  well_order?(R) : bool = well_founded?(R) AND trichotomous?(R);


  %------------------------------------------
  % a well ordering is a strict total order
  %------------------------------------------

  S : VAR (well_order?)

  wo_transitive : LEMMA   S(x, y) AND S(y, z) IMPLIES S(x, z)

  wo_irreflexive : LEMMA  NOT S(x, x)

  wo_strict_total_order : LEMMA  strict_total_order?(S)


  END well_ordering

$$$well_ordering.prf
(|well_ordering|
 (|wo_transitive| "" (SKOSIMP :PREDS? T)
  (("" (EXPAND* "well_order?" "trichotomous?[T]" "well_founded?[T]")
    (("" (FLATTEN) (("" (INST - "{x | x=x!1 OR x=y!1 OR x=z!1}") (("" (REDUCE :IF-MATCH ALL) NIL NIL)) NIL)) NIL)) NIL))
  NIL)
 (|wo_irreflexive| "" (SKOSIMP :PREDS? T)
  (("" (EXPAND* "well_order?" "trichotomous?" "well_founded?")
    (("" (FLATTEN) (("" (DELETE -2) (("" (INST - "{x | x=x!1}") (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL)) NIL))
  NIL)
 (|wo_strict_total_order| "" (SKOLEM-TYPEPRED)
  (("" (AUTO-REWRITE-THEORIES "orders[T]" "relations[T]")
    (("" (ASSERT)
      (("" (PROP)
        (("1" (USE "wo_irreflexive" ("S" "S!1")) NIL NIL) ("2" (USE "wo_transitive" ("S" "S!1")) NIL NIL)
         ("3" (EXPAND "well_order?") (("3" (GROUND) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL))


$$$set_bounds.pvs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Arbitrary unions and intersections  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

set_bounds [ T : TYPE ] : THEORY

  BEGIN

  A, B : VAR set[set[T]]

  X, Y, Z : VAR set[T]

  x : VAR T

  %------------------
  %  Infinite union
  %------------------

  union(A) : set[T] = { x | EXISTS (X : (A)) : X(x) }

  union_upper_bound : LEMMA
	FORALL (X : (A)) : subset?(X, union(A))

  union_least_upper_bound : LEMMA
	subset?(union(A), Y) IFF FORALL (X : (A)) : subset?(X, Y) 

  subset_union : LEMMA 
	(EXISTS (X:(A)): subset?(Y, X)) IMPLIES subset?(Y, union(A))

  union_empty : LEMMA union(emptyset[set[T]]) = emptyset


  %----------------
  %  Intersection
  %----------------

  inter(A) : set[T] = { x | FORALL (X : (A)) : X(x) }

  inter_lower_bound : LEMMA
	FORALL (X : (A)) : subset?(inter(A), X)

  inter_greatest_lower_bound : LEMMA
	subset?(Y, inter(A)) IFF FORALL (X : (A)) : subset?(Y, X)

  subset_inter : LEMMA
	(EXISTS (X : (A)): subset?(X, Y)) IMPLIES subset?(inter(A), Y)

  inter_empty : LEMMA inter(emptyset[set[T]]) = fullset


  %-----------------
  %  pairs of sets
  %-----------------

  pair(X, Y) : (nonempty?[set[T]]) = { Z | Z = X or Z = Y }

  union_pair : LEMMA
	union(pair(X, Y)) = union(X, Y)

  inter_pair : LEMMA
	inter(pair(X, Y)) = intersection(X, Y)



  %-----------
  %  Duality
  %-----------

  inter_complement : LEMMA
	inter(image(complement, A)) = complement(union(A))

  union_complement : LEMMA
	union(image(complement, A)) = complement(inter(A))



  END set_bounds

$$$set_bounds.prf
(|set_bounds| (|union_upper_bound| "" (GRIND) NIL)
 (|union_least_upper_bound| "" (GRIND :IF-MATCH NIL)
  (("1" (REDUCE) NIL) ("2" (REDUCE) NIL)))
 (|subset_union| "" (GRIND) NIL)
 (|union_empty| "" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))
 (|inter_lower_bound| "" (GRIND) NIL)
 (|inter_greatest_lower_bound| "" (GRIND :IF-MATCH NIL)
  (("1" (REDUCE :IF-MATCH BEST) NIL) ("2" (REDUCE :IF-MATCH BEST) NIL)))
 (|subset_inter| "" (GRIND) NIL)
 (|inter_empty| "" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))
 (|pair_TCC1| "" (GRIND) NIL)
 (|union_pair| "" (SKOLEM!)
  (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))))
 (|inter_pair| "" (SKOLEM!)
  (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL)))))
 (|inter_complement| "" (SKOLEM!)
  (("" (APPLY-EXTENSIONALITY :HIDE? T)
    (("" (GRIND :IF-MATCH NIL)
      (("1" (INST - "complement(X!1)") (("1" (ASSERT) NIL) ("2" (INST?) NIL)))
       ("2" (INST?) NIL)))))))
 (|union_complement| "" (SKOLEM!)
  (("" (APPLY-EXTENSIONALITY :HIDE? T)
    (("" (GRIND :IF-MATCH NIL)
      (("1" (INST?) NIL)
       ("2" (INST + "complement(X!1)")
        (("1" (ASSERT) NIL) ("2" (INST?) NIL))))))))))

$$$well_ordering_principle.pvs
well_ordering_principle [T : TYPE] : THEORY

  BEGIN

  IMPORTING set_bounds, well_ordering


  A, B : VAR set[T]

  C : VAR (nonempty?[T])

  M, N : VAR set[set[T]]

  x, y, z : VAR T



  %-----------------
  %  Non full sets
  %-----------------

  nonfull?(A) : bool = EXISTS x : not A(x)

  E, E1, E2 : VAR (nonfull?)


  %-----------------------------------
  %  Variant of the choice function  
  %-----------------------------------

  phi(E) : { x | not E(x) }

  succ(E) : (nonempty?[T]) = add(phi(E), E)


  subset_succ1: LEMMA subset?(E, succ(E))

  subset_succ2: LEMMA subset?(A, E) IMPLIES subset?(A, succ(E))

  subset_succ3: LEMMA
     subset?(E, A) AND subset?(A, succ(E)) IMPLIES A = E OR A = succ(E)


  %----------
  %  Chains
  %----------

  Chain(M): bool =
	 M(emptyset)
     AND (FORALL E : M(E) IMPLIES M(succ(E)))
     AND (FORALL N : subset?(N, M) IMPLIES M(union(N)))


  %--------------------------
  %  ZM: the smallest chain
  %--------------------------

  ZM : set[set[T]] = inter(Chain)


  ZM_smallest : LEMMA Chain(M) IMPLIES subset?(ZM, M)

  emptyset_in_ZM : LEMMA ZM(emptyset)

  succ_in_ZM : LEMMA ZM(E) IMPLIES ZM(succ(E))

  union_in_ZM : LEMMA subset?(M, ZM) IMPLIES ZM(union(M))

  ZM_is_chain : LEMMA Chain(ZM)


  X, Y, Z : VAR (ZM)


  %---------------
  %  Main lemmas
  %---------------

  H : set[set[T]] = { A | FORALL X: subset?(X, A) or subset?(A, X) }


  H_emptyset : LEMMA  H(emptyset)

  H_succ : LEMMA  H(E) IMPLIES H(succ(E))

  H_union : LEMMA subset?(M, H) IMPLIES H(union(M))

  H_is_chain: PROPOSITION Chain(H)


  %--------------------------------------------------------------
  %  Consequence: ZM is totally ordered by the subset? relation
  %--------------------------------------------------------------

  linear_order_on_ZM : PROPOSITION  subset?(X, Y) OR subset?(Y, X)

  strict_order_on_ZM : PROPOSITION
     strict_subset?(X, Y) OR X=Y OR strict_subset?(Y, X)

  strict_subset_succ : LEMMA
     strict_subset?(X, Y) IMPLIES nonfull?(X) AND Y(phi(X))


  %-----------------
  %  Ordering on T
  %-----------------

  K(x): { E | ZM(E) } = union({ B | ZM(B) AND not B(x) })

  K(C): { E | ZM(E) } = union({ B | ZM(B) AND disjoint?(C, B) })


  phi_K1: LEMMA  phi(K(x)) = x

  phi_K2: LEMMA  C(phi(K(C)))

  phi_K3: LEMMA  K(phi(K(C))) = K(C);

  <(x, y): bool = strict_subset?(K(x), K(y))


  trichotomous: LEMMA trichotomous?(<)

  well_founded: LEMMA well_founded?(<)


  %---------------
  %  Main result
  %---------------

  R : VAR [T, T -> bool]

  well_order_exists : THEOREM  EXISTS R : well_order?(R)

  END well_ordering_principle


$$$well_ordering_principle.prf
(|well_ordering_principle|
 (|phi_TCC1| "" (INST + "lambda E : epsilon! (x: T | NOT E(x)) : true")
  (("" (GRIND) NIL NIL)) NIL)
 (|subset_succ1| "" (GRIND :EXCLUDE "nonfull?") NIL NIL)
 (|subset_succ2| "" (SKOSIMP)
  (("" (AUTO-REWRITE "subset_succ1")
    (("" (USE "subset_transitive" ("c" "succ(E!1)"))
      (("" (ASSERT) NIL NIL)) NIL))
    NIL))
  NIL)
 (|subset_succ3| "" (GRIND :EXCLUDE "nonfull?" :IF-MATCH NIL)
  (("" (APPLY-EXTENSIONALITY :HIDE? T)
    (("" (APPLY-EXTENSIONALITY 2 :HIDE? T)
      (("" (IFF) (("" (REDUCE :IF-MATCH ALL) NIL NIL)) NIL)) NIL))
    NIL))
  NIL)
 (|ZM_smallest| "" (EXPAND "ZM")
  (("" (SKOSIMP) (("" (REWRITE "inter_lower_bound") NIL NIL)) NIL))
  NIL)
 (|emptyset_in_ZM| "" (GRIND :EXCLUDE ("succ" "union")) NIL NIL)
 (|succ_in_ZM| "" (GRIND :EXCLUDE ("nonfull?" "succ" "union")) NIL NIL)
 (|union_in_ZM| "" (SKOSIMP)
  (("" (EXPAND "ZM" +)
    (("" (EXPAND "inter")
      (("" (SKOLEM-TYPEPRED)
        (("" (FORWARD-CHAIN "ZM_smallest")
          (("" (EXPAND "Chain")
            (("" (PROP)
              (("" (INST? -4)
                (("" (ASSERT)
                  (("" (USE "subset_transitive" ("a" "M!1"))
                    (("" (ASSERT) NIL NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|ZM_is_chain| ""
  (GRIND :DEFS NIL :REWRITES
   ("Chain" "emptyset_in_ZM" "succ_in_ZM" "union_in_ZM"))
  NIL NIL)
 (|H_emptyset| "" (GRIND) NIL NIL)
 (|H_succ| "" (SKOSIMP)
  ((""
    (CASE "Chain({ B | ZM(B) and (subset?(B, E!1) or subset?(succ(E!1), B)) })")
    (("1" (FORWARD-CHAIN "ZM_smallest")
      (("1" (DELETE -2 -3)
        (("1"
          (GRIND :DEFS NIL :REWRITES
           ("H" "subset?[set[T]]" "member[set[T]]" "subset_succ1"
            "subset_succ2")
           :IF-MATCH NIL)
          (("1" (INST?) (("1" (GROUND) NIL NIL)) NIL)) NIL))
        NIL))
      NIL)
     ("2" (DELETE 2)
      (("2" (EXPAND "Chain")
        (("2"
          (AUTO-REWRITE "H" "emptyset_in_ZM" "succ_in_ZM"
                        "subset_emptyset[T]" "subset_reflexive[T]"
                        "subset_succ1" "subset_succ2" "subset?[set[T]]"
                        "member[set[T]]")
          (("2" (GROUND)
            (("1" (SKOSIMP)
              (("1" (ASSERT)
                (("1" (INST - "succ(E!2)")
                  (("1" (GROUND)
                    (("1" (FORWARD-CHAIN "subset_succ3")
                      (("1" (REPLACE*) (("1" (ASSERT) NIL NIL)) NIL)
                       ("2" (ASSERT) NIL NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (SKOSIMP)
              (("2" (GROUND)
                (("1" (REWRITE "union_in_ZM")
                  (("1" (SKOSIMP)
                    (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL))
                  NIL)
                 ("2" (REWRITE "subset_union")
                  (("2" (REWRITE "union_least_upper_bound")
                    (("2" (SKOLEM!)
                      (("2" (INST? -)
                        (("2" (GROUND) (("2" (INST?) NIL NIL)) NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|H_union| "" (AUTO-REWRITE "H" "subset?[set[T]]" "member[set[T]]")
  (("" (REDUCE :IF-MATCH NIL)
    (("" (REWRITE "subset_union")
      (("" (REWRITE "union_least_upper_bound")
        (("" (SKOLEM!)
          (("" (INST - "X!2")
            (("" (ASSERT)
              (("" (INST? -) (("" (ASSERT) (("" (INST?) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|H_is_chain| ""
  (AUTO-REWRITE "H_emptyset" "H_succ" "H_union" "Chain")
  (("" (REDUCE :IF-MATCH NIL) NIL NIL)) NIL)
 (|linear_order_on_ZM| "" (SKOSIMP)
  (("" (USE "H_is_chain")
    (("" (FORWARD-CHAIN "ZM_smallest")
      ((""
        (GRIND :DEFS NIL :REWRITES
         ("member[set[T]]" "subset?[set[T]]" "H"))
        NIL NIL))
      NIL))
    NIL))
  NIL)
 (|strict_order_on_ZM| "" (SKOSIMP)
  (("" (EXPAND "strict_subset?")
    (("" (USE "linear_order_on_ZM") (("" (GROUND) NIL NIL)) NIL)) NIL))
  NIL)
 (|strict_subset_succ| "" (SKOSIMP)
  (("" (CASE "nonfull?(X!1)")
    (("1" (ASSERT)
      (("1" (AUTO-REWRITE "succ_in_ZM")
        (("1" (USE "linear_order_on_ZM" ("X" "succ(X!1)" "Y" "Y!1"))
          (("1" (GRIND :EXCLUDE "nonfull?" :IF-MATCH NIL)
            (("1" (INST?) NIL NIL)
             ("2" (APPLY-EXTENSIONALITY :HIDE? T)
              (("2" (REDUCE) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("2" (DELETE 2)
      (("2" (GRIND)
        (("2" (APPLY-EXTENSIONALITY 2 :HIDE? T)
          (("2" (REDUCE) NIL NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (K_TCC1 "" (SKOLEM!)
  (("" (GROUND)
    (("1" (GRIND :EXCLUDE "ZM")
      (("1" (INST + "x!1")
        (("1" (SKOLEM!) (("1" (ASSERT) NIL NIL)) NIL)) NIL))
      NIL)
     ("2" (REWRITE "union_in_ZM")
      (("2" (DELETE 2) (("2" (GRIND :EXCLUDE "ZM") NIL NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (K_TCC2 "" (SKOLEM-TYPEPRED)
  (("" (GROUND)
    (("1" (GRIND :EXCLUDE "ZM") NIL NIL)
     ("2" (REWRITE "union_in_ZM")
      (("2" (DELETE -1 2) (("2" (GRIND :EXCLUDE "ZM") NIL NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (|phi_K1| "" (SKOLEM!)
  (("" (AUTO-REWRITE "succ_in_ZM")
    (("" (ASSERT)
      ((""
        (USE "union_upper_bound"
             ("A" "{ B | ZM(B) AND not B(x!1) }" "X" "succ(K(x!1))"))
        (("1" (REWRITE "K" :DIR RL)
          (("1" (DELETE +)
            (("1" (GRIND :EXCLUDE "K" :IF-MATCH NIL)
              (("1" (INST - "phi(K(x!1))") (("1" (ASSERT) NIL NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("2" (GRIND) NIL NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|phi_K2| "" (SKOLEM!)
  (("" (AUTO-REWRITE "succ_in_ZM")
    (("" (ASSERT)
      ((""
        (USE "union_upper_bound"
             ("A" "{ B | ZM(B) AND disjoint?(C!1, B) }" "X"
              "succ(K(C!1))"))
        (("1" (REWRITE "K" :DIR RL)
          (("1" (DELETE +)
            (("1" (GRIND :EXCLUDE "K" :IF-MATCH NIL)
              (("1" (INST - "phi(K(C!1))") (("1" (ASSERT) NIL NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("2" (CASE "disjoint?(C!1, K(C!1))")
          (("1" (GRIND :EXCLUDE "K" :IF-MATCH NIL)
            (("1" (INST - "x!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)
           ("2" (DELETE 2 3) (("2" (GRIND) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|phi_K3| "" (SKOLEM!)
  (("" (ASSERT)
    (("" (USE "strict_order_on_ZM")
      (("" (GROUND)
        (("1" (FORWARD-CHAIN "strict_subset_succ")
          (("1" (REWRITE "phi_K1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)
         ("2" (FORWARD-CHAIN "strict_subset_succ")
          (("2" (DELETE -1 -3 1)
            (("2" (NAME-REPLACE "x1" "phi(K(C!1))")
              (("2" (GRIND) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|trichotomous| "" (GRIND :DEFS NIL :REWRITES ("trichotomous?" "<"))
  (("" (USE "strict_order_on_ZM")
    (("" (GROUND)
      (("" (AUTO-REWRITE "phi_K1")
        (("" (CASE "phi(K(x!1)) = y!1")
          (("1" (ASSERT) NIL NIL)
           ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|well_founded| "" (EXPAND "well_founded?")
  (("" (SKOSIMP)
    (("" (CASE "nonempty?(p!1)")
      (("1" (ASSERT)
        (("1" (DELETE -)
          (("1" (INST + "phi(K(p!1))")
            (("1" (AUTO-REWRITE "phi_K1" "phi_K3")
              (("1" (SKOLEM-TYPEPRED)
                (("1" (EXPAND "<")
                  (("1" (ASSERT)
                    (("1" (FORWARD-CHAIN "strict_subset_succ")
                      (("1" (ASSERT)
                        (("1" (DELETE -1 -4) (("1" (GRIND) NIL NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (REWRITE "phi_K2") NIL NIL))
            NIL))
          NIL))
        NIL)
       ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (|well_order_exists| "" (INST + "<")
  (("" (EXPAND "well_order?")
    (("" (AUTO-REWRITE "well_founded" "trichotomous")
      (("" (ASSERT) NIL NIL)) NIL))
    NIL))
  NIL))


$$$zorn.pvs
zorn [ T: TYPE, <=:(partial_order?[T]) ] : THEORY

  BEGIN

  IMPORTING well_ordering_principle[T]

  x, y, z: VAR T

  A, B: VAR set[T]

  P: VAR [T -> bool]


  %-----------------------
  %  well ordering on T
  %-----------------------

  <<: (well_order?[T])

  well_founded_relation: LEMMA well_founded?[T](<<)

  total_order: LEMMA x << y OR x = y OR y << x


  %--------------------
  %  properties of <=
  %--------------------

  reflexivity: LEMMA x <= x

  transitivity: LEMMA x <= y AND y <= z IMPLIES x <= z

  antisymmetry: LEMMA x <= y AND y <= x IMPLIES x = y


  %-------------------------------------
  %  Chains: totally orderd sets by <=
  %-------------------------------------

  chain?(A): bool = FORALL (y, z: (A)): y <= z OR z <= y

  bounded?(A): bool = EXISTS x : FORALL (y: (A)): y <= x



  %-----------------
  %  Zorn's Lemma
  %-----------------

  C(x): RECURSIVE bool =
       FORALL (y | y << x): C(y) IMPLIES y <= x
    MEASURE x BY <<

  C_is_chain: LEMMA chain?(C)


  zorn: PROPOSITION
     (FORALL A: chain?(A) IMPLIES bounded?(A))
        IMPLIES EXISTS x : FORALL y : x <= y IMPLIES x = y


  %------------------------
  %  Maximal chains exist
  %------------------------

  D(x): RECURSIVE bool =
        FORALL (y | y << x): D(y) IMPLIES x <= y OR y <= x
     MEASURE x BY <<

  D_is_chain: LEMMA chain?(D)


  maximal_chain: PROPOSITION
     EXISTS A: chain?(A) AND 
	FORALL B: chain?(B) AND subset?(A, B) IMPLIES B = A

  END zorn



$$$zorn.prf
(|zorn|
 (|doublelessp_TCC1| "" (LEMMA "well_order_exists")
  (("" (SKOLEM!) (("" (INST + "R!1") NIL)))))
 (|well_founded_relation| "" (TYPEPRED "zorn.<<")
  (("" (EXPAND "well_order?") (("" (GROUND) NIL NIL)) NIL)) NIL)
 (|total_order| "" (TYPEPRED "zorn.<<")
  (("" (EXPAND* "well_order?" "trichotomous?") (("" (REDUCE) NIL NIL))
    NIL))
  NIL)
 (|reflexivity| "" (TYPEPRED "zorn.<=")
  (("" (EXPAND* "partial_order?" "preorder?" "reflexive?")
    (("" (GROUND) NIL NIL)) NIL))
  NIL)
 (|transitivity| "" (TYPEPRED "zorn.<=")
  (("" (EXPAND* "partial_order?" "preorder?" "transitive?")
    (("" (GROUND) NIL NIL)) NIL))
  NIL)
 (|antisymmetry| "" (TYPEPRED "zorn.<=")
  (("" (EXPAND* "partial_order?" "antisymmetric?")
    (("" (GROUND) NIL NIL)) NIL))
  NIL)
 (C_TCC1 "" (REPLACE-ETA "zorn.<<")
  (("" (REWRITE "well_founded_relation") NIL)))
 (C_TCC2 "" (SKOLEM!) (("" (ASSERT) NIL)))
 (|C_is_chain| "" (EXPAND "chain?")
  (("" (SKOSIMP :PREDS? T)
    (("" (AUTO-REWRITE "reflexivity")
      (("" (LEMMA "total_order" ("x" "y!1" "y" "z!1"))
        (("" (GROUND)
          (("1" (EXPAND "C" -3)
            (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)
           ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)
           ("3" (EXPAND "C" -2)
            (("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|zorn| "" (AUTO-REWRITE "C_is_chain" "bounded?" "antisymmetry")
  (("" (SKOSIMP)
    (("" (INST - "C")
      (("" (ASSERT)
        (("" (SKOLEM!)
          (("" (INST? +)
            (("" (SKOSIMP)
              (("" (CASE "C(y!1)")
                (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)
                 ("2" (EXPAND "C")
                  (("2" (SKOSIMP)
                    (("2" (INST?)
                      (("2" (FORWARD-CHAIN "transitivity") NIL NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|D_is_chain| "" (EXPAND "chain?")
  (("" (SKOSIMP :PREDS? T)
    (("" (AUTO-REWRITE "reflexivity")
      (("" (LEMMA "total_order" ("x" "y!1" "y" "z!1"))
        (("" (GROUND)
          (("1" (EXPAND "D" -3)
            (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)
           ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)
           ("3" (EXPAND "D" -2)
            (("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|maximal_chain| "" (INST + "D")
  (("" (REWRITE "D_is_chain")
    (("" (REDUCE)
      (("" (REWRITE "subset_antisymmetric")
        (("" (EXPAND* "subset?" "member" "chain?")
          (("" (EXPAND "D" 1) (("" (REDUCE) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL))