Beginning of Section TaggedSets

Let tag : set → set ≝ λalpha ⇒ SetAdjoin alpha {1}

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.

¬ TransSet {1}

In Proofgold the corresponding term root is 8f2d67... and proposition id is be9a70...

Proof:

Assume H1: TransSet {1}.

We prove the intermediate claim L1: 0 ∈ {1}.

An exact proof term for the current goal is H1 1 (SingI 1) 0 In_0_1.

Apply neq_0_1 to the current goal.

An exact proof term for the current goal is SingE 1 0 L1.

∎

Theorem. (not_ordinal_Sing1)

¬ ordinal {1}

In Proofgold the corresponding term root is 99a3f6... and proposition id is db7977...

Proof:

Assume H1.

Apply H1 to the current goal.

Assume H2 _.

An exact proof term for the current goal is not_TransSet_Sing1 H2.

∎

Theorem. (tagged_not_ordinal)

∀y, ¬ ordinal (y ')

In Proofgold the corresponding term root is f9488c... and proposition id is aaf6e4...

Proof:

Let y be given.

Assume H1: ordinal (y ').

We prove the intermediate claim L1: {1} ∈ y '.

We will prove {1} ∈ y ∪ {{1}}.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is SingI {1}.

Apply not_ordinal_Sing1 to the current goal.

An exact proof term for the current goal is ordinal_Hered (y ') H1 {1} L1.

∎

Theorem. (tagged_notin_ordinal)

∀alpha y, ordinal alpha → (y ') ∉ alpha

In Proofgold the corresponding term root is b603ba... and proposition id is c0e2c3...

Proof:

Let alpha and y be given.

Assume H1 H2.

Apply tagged_not_ordinal y to the current goal.

An exact proof term for the current goal is ordinal_Hered alpha H1 (y ') H2.

∎

Theorem. (tagged_eqE_Subq)

∀alpha beta, ordinal alpha → alpha ' = beta ' → alpha ⊆ beta

In Proofgold the corresponding term root is cf032f... and proposition id is ef37f5...

Proof:

Let alpha and beta be given.

Assume Ha He.

Let gamma be given.

Assume Hc: gamma ∈ alpha.

We prove the intermediate claim L1: gamma ∈ beta '.

rewrite the current goal using He (from right to left).

We will prove gamma ∈ alpha ∪ {{1}}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is Hc.

Apply binunionE beta {{1}} gamma L1 to the current goal.

Assume H1: gamma ∈ beta.

An exact proof term for the current goal is H1.

Assume H1: gamma ∈ {{1}}.

We will prove False.

Apply not_ordinal_Sing1 to the current goal.

rewrite the current goal using SingE {1} gamma H1 (from right to left).

An exact proof term for the current goal is ordinal_Hered alpha Ha gamma Hc.

∎

Theorem. (tagged_eqE_eq)

∀alpha beta, ordinal alpha → ordinal beta → alpha ' = beta ' → alpha = beta

In Proofgold the corresponding term root is 1f7dc9... and proposition id is ec1608...

Proof:

Let alpha and beta be given.

Assume Ha Hb He.

An exact proof term for the current goal is set_ext alpha beta (tagged_eqE_Subq alpha beta Ha He) (tagged_eqE_Subq beta alpha Hb (λq ⇒ He (λu v ⇒ q v u))).

∎

Theorem. (tagged_ReplE)

∀alpha beta, ordinal alpha → ordinal beta → beta ' ∈ {gamma '|gamma ∈ alpha} → beta ∈ alpha

In Proofgold the corresponding term root is a1d43c... and proposition id is 70c250...

Proof:

Let alpha and beta be given.

Assume Ha Hb.

Assume H1: beta ' ∈ {gamma '|gamma ∈ alpha}.

Apply ReplE_impred alpha (λgamma ⇒ gamma ') (beta ') H1 to the current goal.

Let gamma be given.

Assume H2: gamma ∈ alpha.

Assume H3: beta ' = gamma '.

We prove the intermediate claim L2: beta = gamma.

An exact proof term for the current goal is tagged_eqE_eq beta gamma Hb (ordinal_Hered alpha Ha gamma H2) H3.

rewrite the current goal using L2 (from left to right).

An exact proof term for the current goal is H2.

∎

Theorem. (ordinal_notin_tagged_Repl)

∀alpha Y, ordinal alpha → alpha ∉ {y '|y ∈ Y}

In Proofgold the corresponding term root is 7f35b5... and proposition id is e7ff3b...

Proof:

Let alpha and Y be given.

Assume H1: ordinal alpha.

Assume H2: alpha ∈ {y '|y ∈ Y}.

Apply ReplE_impred Y (λy ⇒ y ') alpha H2 to the current goal.

Let y be given.

Assume H3: y ∈ Y.

Assume H4: alpha = y '.

Apply tagged_not_ordinal y to the current goal.

We will prove ordinal (y ').

rewrite the current goal using H4 (from right to left).

An exact proof term for the current goal is H1.

∎

Definition. We define SNoElts_ to be λalpha ⇒ alpha ∪ {beta '|beta ∈ alpha} of type set → set.

In Proofgold the corresponding term root is c0ec73... and object id is 6f0c36...

Theorem. (SNoElts_mon)

∀alpha beta, alpha ⊆ beta → SNoElts_ alpha ⊆ SNoElts_ beta

In Proofgold the corresponding term root is 49a08e... and proposition id is 859611...

Proof:

Let alpha and beta be given.

Assume H1: alpha ⊆ beta.

Let x be given.

Assume H2: x ∈ alpha ∪ {gamma '|gamma ∈ alpha}.

Apply binunionE alpha {gamma '|gamma ∈ alpha} x H2 to the current goal.

Assume H3: x ∈ alpha.

We will prove x ∈ beta ∪ {gamma '|gamma ∈ beta}.

Apply binunionI1 to the current goal.

Apply H1 to the current goal.

An exact proof term for the current goal is H3.

Assume H3: x ∈ {gamma '|gamma ∈ alpha}.

We will prove x ∈ beta ∪ {gamma '|gamma ∈ beta}.

Apply binunionI2 to the current goal.

We will prove x ∈ {gamma '|gamma ∈ beta}.

Apply ReplE_impred alpha (λgamma ⇒ gamma ') x H3 to the current goal.

Let gamma be given.

Assume H4: gamma ∈ alpha.

Assume H5: x = gamma '.

rewrite the current goal using H5 (from left to right).

We will prove gamma ' ∈ {gamma '|gamma ∈ beta}.

An exact proof term for the current goal is ReplI beta (λgamma ⇒ gamma ') gamma (H1 gamma H4).

∎

Definition. We define SNo_ to be λalpha x ⇒ x ⊆ SNoElts_ alpha ∧ ∀beta ∈ alpha, exactly1of2 (beta ' ∈ x) (beta ∈ x) of type set → set → prop.

In Proofgold the corresponding term root is 4ab7e4... and object id is c16a73...

Definition. We define PSNo to be λalpha p ⇒ {beta ∈ alpha|p beta} ∪ {beta '|beta ∈ alpha, ¬ p beta} of type set → (set → prop) → set.

In Proofgold the corresponding term root is 3657ae... and object id is 0a8351...

Theorem. (PNoEq_PSNo)

∀alpha, ordinal alpha → ∀p : set → prop, PNoEq_ alpha (λbeta ⇒ beta ∈ PSNo alpha p) p

In Proofgold the corresponding term root is c12e02... and proposition id is 688518...

Proof:

Let alpha be given.

Assume Ha: ordinal alpha.

Let p be given.

Let beta be given.

Assume Hb: beta ∈ alpha.

We will prove beta ∈ PSNo alpha p ↔ p beta.

Apply iffI to the current goal.

Assume H1: beta ∈ {beta ∈ alpha|p beta} ∪ {beta '|beta ∈ alpha, ¬ p beta}.

Apply binunionE {beta ∈ alpha|p beta} {beta '|beta ∈ alpha, ¬ p beta} beta H1 to the current goal.

Assume H2: beta ∈ {beta ∈ alpha|p beta}.

An exact proof term for the current goal is SepE2 alpha p beta H2.

Assume H2: beta ∈ {beta '|beta ∈ alpha, ¬ p beta}.

We will prove False.

Apply ReplSepE_impred alpha (λbeta ⇒ ¬ p beta) (λx ⇒ x ') beta H2 to the current goal.

Let gamma be given.

Assume Hc: gamma ∈ alpha.

Assume H3: ¬ p gamma.

Assume H4: beta = gamma '.

Apply tagged_notin_ordinal alpha gamma Ha to the current goal.

We will prove gamma ' ∈ alpha.

rewrite the current goal using H4 (from right to left).

An exact proof term for the current goal is Hb.

Assume H1: p beta.

We will prove beta ∈ PSNo alpha p.

We will prove beta ∈ {beta ∈ alpha|p beta} ∪ {beta '|beta ∈ alpha, ¬ p beta}.

Apply binunionI1 to the current goal.

Apply SepI to the current goal.

An exact proof term for the current goal is Hb.

An exact proof term for the current goal is H1.

∎

Theorem. (SNo_PSNo)

∀alpha, ordinal alpha → ∀p : set → prop, SNo_ alpha (PSNo alpha p)

In Proofgold the corresponding term root is 96e4e2... and proposition id is f03db0...

Proof:

Let alpha be given.

Assume Ha.

Let p be given.

We will prove PSNo alpha p ⊆ SNoElts_ alpha ∧ ∀beta ∈ alpha, exactly1of2 (beta ' ∈ PSNo alpha p) (beta ∈ PSNo alpha p).

Apply andI to the current goal.

Let u be given.

Assume Hu: u ∈ PSNo alpha p.

We will prove u ∈ SNoElts_ alpha.

Apply binunionE {beta ∈ alpha|p beta} {beta '|beta ∈ alpha, ¬ p beta} u Hu to the current goal.

Assume H1: u ∈ {beta ∈ alpha|p beta}.

Apply SepE alpha p u H1 to the current goal.

Assume H2: u ∈ alpha.

Assume H3: p u.

We will prove u ∈ alpha ∪ {beta '|beta ∈ alpha}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is H2.

Assume H1: u ∈ {beta '|beta ∈ alpha, ¬ p beta}.

Apply ReplSepE_impred alpha (λbeta ⇒ ¬ p beta) (λbeta ⇒ beta ') u H1 to the current goal.

Let beta be given.

Assume H2: beta ∈ alpha.

Assume H3: ¬ p beta.

Assume H4: u = beta '.

We will prove u ∈ alpha ∪ {beta '|beta ∈ alpha}.

Apply binunionI2 to the current goal.

We will prove u ∈ {beta '|beta ∈ alpha}.

rewrite the current goal using H4 (from left to right).

An exact proof term for the current goal is ReplI alpha (λbeta ⇒ beta ') beta H2.

Let beta be given.

Assume H1: beta ∈ alpha.

We prove the intermediate claim Lbeta: ordinal beta.

An exact proof term for the current goal is ordinal_Hered alpha Ha beta H1.

We will prove exactly1of2 (beta ' ∈ PSNo alpha p) (beta ∈ PSNo alpha p).

Apply xm (p beta) to the current goal.

Assume H2: p beta.

Apply exactly1of2_I2 to the current goal.

We will prove beta ' ∉ PSNo alpha p.

Assume H3: beta ' ∈ PSNo alpha p.

Apply binunionE {beta ∈ alpha|p beta} {beta '|beta ∈ alpha, ¬ p beta} (beta ') H3 to the current goal.

Assume H4: beta ' ∈ {beta ∈ alpha|p beta}.

Apply SepE alpha p (beta ') H4 to the current goal.

Assume H5: beta ' ∈ alpha.

Assume H6: p (beta ').

We will prove False.

Apply tagged_not_ordinal beta to the current goal.

An exact proof term for the current goal is ordinal_Hered alpha Ha (beta ') H5.

Assume H4: beta ' ∈ {beta '|beta ∈ alpha, ¬ p beta}.

Apply ReplSepE_impred alpha (λbeta ⇒ ¬ p beta) (λbeta ⇒ beta ') (beta ') H4 to the current goal.

Let gamma be given.

Assume H5: gamma ∈ alpha.

Assume H6: ¬ p gamma.

Assume H7: beta ' = gamma '.

We prove the intermediate claim Lgamma: ordinal gamma.

An exact proof term for the current goal is ordinal_Hered alpha Ha gamma H5.

We prove the intermediate claim L1: beta = gamma.

An exact proof term for the current goal is tagged_eqE_eq beta gamma Lbeta Lgamma H7.

Apply H6 to the current goal.

We will prove p gamma.

rewrite the current goal using L1 (from right to left).

We will prove p beta.

An exact proof term for the current goal is H2.

We will prove beta ∈ {beta ∈ alpha|p beta} ∪ {beta '|beta ∈ alpha, ¬ p beta}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is SepI alpha p beta H1 H2.

Assume H2: ¬ p beta.

Apply exactly1of2_I1 to the current goal.

We will prove beta ' ∈ {beta ∈ alpha|p beta} ∪ {beta '|beta ∈ alpha, ¬ p beta}.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is ReplSepI alpha (λbeta ⇒ ¬ p beta) (λbeta ⇒ beta ') beta H1 H2.

We will prove beta ∉ PSNo alpha p.

Assume H3: beta ∈ PSNo alpha p.

Apply binunionE {beta ∈ alpha|p beta} {beta '|beta ∈ alpha, ¬ p beta} beta H3 to the current goal.

Assume H4: beta ∈ {beta ∈ alpha|p beta}.

Apply SepE alpha p beta H4 to the current goal.

Assume H5: beta ∈ alpha.

Assume H6: p beta.

We will prove False.

An exact proof term for the current goal is H2 H6.

Assume H4: beta ∈ {beta '|beta ∈ alpha, ¬ p beta}.

Apply ReplSepE_impred alpha (λbeta ⇒ ¬ p beta) (λbeta ⇒ beta ') beta H4 to the current goal.

Let gamma be given.

Assume H5: gamma ∈ alpha.

Assume H6: ¬ p gamma.

Assume H7: beta = gamma '.

Apply tagged_not_ordinal gamma to the current goal.

We will prove ordinal (gamma ').

rewrite the current goal using H7 (from right to left).

An exact proof term for the current goal is Lbeta.

∎

Theorem. (SNo_PSNo_eta_)

∀alpha x, ordinal alpha → SNo_ alpha x → x = PSNo alpha (λbeta ⇒ beta ∈ x)

In Proofgold the corresponding term root is 1642af... and proposition id is 630119...

Proof:

Let alpha and x be given.

Assume Ha Hx.

Apply Hx to the current goal.

Assume Hx1: x ⊆ SNoElts_ alpha.

Assume Hx2: ∀beta ∈ alpha, exactly1of2 (beta ' ∈ x) (beta ∈ x).

Apply set_ext to the current goal.

We will prove x ⊆ PSNo alpha (λbeta ⇒ beta ∈ x).

Let u be given.

Assume Hu: u ∈ x.

Apply binunionE alpha {beta '|beta ∈ alpha} u (Hx1 u Hu) to the current goal.

Assume H1: u ∈ alpha.

We will prove u ∈ {beta ∈ alpha|beta ∈ x} ∪ {beta '|beta ∈ alpha, beta ∉ x}.

Apply binunionI1 to the current goal.

Apply SepI to the current goal.

An exact proof term for the current goal is H1.

An exact proof term for the current goal is Hu.

Assume H1: u ∈ {beta '|beta ∈ alpha}.

Apply ReplE_impred alpha (λbeta ⇒ beta ') u H1 to the current goal.

Let beta be given.

Assume H2: beta ∈ alpha.

Assume H3: u = beta '.

We will prove u ∈ {beta ∈ alpha|beta ∈ x} ∪ {beta '|beta ∈ alpha, beta ∉ x}.

Apply binunionI2 to the current goal.

We will prove u ∈ {beta '|beta ∈ alpha, beta ∉ x}.

rewrite the current goal using H3 (from left to right).

We will prove beta ' ∈ {beta '|beta ∈ alpha, beta ∉ x}.

We prove the intermediate claim L2: beta ∉ x.

Assume H4: beta ∈ x.

Apply exactly1of2_E (beta ' ∈ x) (beta ∈ x) (Hx2 beta H2) to the current goal.

Assume H5: beta ' ∈ x.

Assume H6: beta ∉ x.

An exact proof term for the current goal is H6 H4.

Assume H4: beta ' ∉ x.

Assume H5: beta ∈ x.

Apply H4 to the current goal.

We will prove (beta ') ∈ x.

rewrite the current goal using H3 (from right to left).

We will prove u ∈ x.

An exact proof term for the current goal is Hu.

An exact proof term for the current goal is ReplSepI alpha (λbeta ⇒ beta ∉ x) (λbeta ⇒ beta ') beta H2 L2.

We will prove PSNo alpha (λbeta ⇒ beta ∈ x) ⊆ x.

Let u be given.

Assume Hu: u ∈ PSNo alpha (λbeta ⇒ beta ∈ x).

We will prove u ∈ x.

Apply binunionE {beta ∈ alpha|beta ∈ x} {beta '|beta ∈ alpha, beta ∉ x} u Hu to the current goal.

Assume H1: u ∈ {beta ∈ alpha|beta ∈ x}.

Apply SepE alpha (λbeta ⇒ beta ∈ x) u H1 to the current goal.

Assume H2: u ∈ alpha.

Assume H3: u ∈ x.

An exact proof term for the current goal is H3.

Assume H1: u ∈ {beta '|beta ∈ alpha, beta ∉ x}.

Apply ReplSepE_impred alpha (λbeta ⇒ beta ∉ x) (λbeta ⇒ beta ') u H1 to the current goal.

Let beta be given.

Assume H2: beta ∈ alpha.

Assume H3: beta ∉ x.

Assume H4: u = beta '.

Apply exactly1of2_E (beta ' ∈ x) (beta ∈ x) (Hx2 beta H2) to the current goal.

Assume H5: beta ' ∈ x.

Assume H6: beta ∉ x.

rewrite the current goal using H4 (from left to right).

An exact proof term for the current goal is H5.

Assume H4: beta ' ∉ x.

Assume H5: beta ∈ x.

We will prove False.

An exact proof term for the current goal is H3 H5.

∎

Definition. We define SNo to be λx ⇒ ∃alpha, ordinal alpha ∧ SNo_ alpha x of type set → prop.

In Proofgold the corresponding term root is 11faa7... and object id is 116b76...

Theorem. (SNo_SNo)

∀alpha, ordinal alpha → ∀z, SNo_ alpha z → SNo z

In Proofgold the corresponding term root is 929b7a... and proposition id is a59341...

Proof:

Let alpha be given.

Assume Ha.

Let z be given.

Assume Hz: SNo_ alpha z.

We will prove ∃alpha, ordinal alpha ∧ SNo_ alpha z.

We use alpha to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Ha.

An exact proof term for the current goal is Hz.

∎

Definition. We define SNoLev to be λx ⇒ Eps_i (λalpha ⇒ ordinal alpha ∧ SNo_ alpha x) of type set → set.

In Proofgold the corresponding term root is 293b77... and object id is 83dce3...

Theorem. (SNoLev_uniq_Subq)

∀x alpha beta, ordinal alpha → ordinal beta → SNo_ alpha x → SNo_ beta x → alpha ⊆ beta

In Proofgold the corresponding term root is 2ca114... and proposition id is 65843d...

Proof:

Let x, alpha and beta be given.

Assume Ha Hb Hax Hbx.

Let gamma be given.

Assume Hc: gamma ∈ alpha.

We will prove gamma ∈ beta.

Apply Hax to the current goal.

Assume Hax1 Hax2.

Apply Hbx to the current goal.

Assume Hbx1 Hbx2.

We prove the intermediate claim Lc: ordinal gamma.

An exact proof term for the current goal is ordinal_Hered alpha Ha gamma Hc.

Apply exactly1of2_or (gamma ' ∈ x) (gamma ∈ x) (Hax2 gamma Hc) to the current goal.

Assume H1: gamma ' ∈ x.

We prove the intermediate claim L1: gamma ' ∈ beta ∪ {delta '|delta ∈ beta}.

An exact proof term for the current goal is Hbx1 (gamma ') H1.

We prove the intermediate claim L2: gamma ' ∈ beta ∨ gamma ' ∈ {delta '|delta ∈ beta}.

An exact proof term for the current goal is binunionE beta {delta '|delta ∈ beta} (gamma ') L1.

Apply L2 to the current goal.

Assume H2: gamma ' ∈ beta.

We will prove False.

An exact proof term for the current goal is tagged_notin_ordinal beta gamma Hb H2.

Assume H2: gamma ' ∈ {delta '|delta ∈ beta}.

An exact proof term for the current goal is tagged_ReplE beta gamma Hb Lc H2.

Assume H1: gamma ∈ x.

We prove the intermediate claim L1: gamma ∈ beta ∪ {delta '|delta ∈ beta}.

An exact proof term for the current goal is Hbx1 gamma H1.

We prove the intermediate claim L2: gamma ∈ beta ∨ gamma ∈ {delta '|delta ∈ beta}.

An exact proof term for the current goal is binunionE beta {delta '|delta ∈ beta} gamma L1.

Apply L2 to the current goal.

Assume H2: gamma ∈ beta.

An exact proof term for the current goal is H2.

Assume H2: gamma ∈ {delta '|delta ∈ beta}.

We will prove False.

An exact proof term for the current goal is ordinal_notin_tagged_Repl gamma beta Lc H2.

∎

Theorem. (SNoLev_uniq)

∀x alpha beta, ordinal alpha → ordinal beta → SNo_ alpha x → SNo_ beta x → alpha = beta

In Proofgold the corresponding term root is 68f71d... and proposition id is 5d96d4...

Proof:

Let x, alpha and beta be given.

Assume Ha Hb Hax Hbx.

Apply set_ext to the current goal.

An exact proof term for the current goal is SNoLev_uniq_Subq x alpha beta Ha Hb Hax Hbx.

An exact proof term for the current goal is SNoLev_uniq_Subq x beta alpha Hb Ha Hbx Hax.

∎

Theorem. (SNoLev_prop)

∀x, SNo x → ordinal (SNoLev x) ∧ SNo_ (SNoLev x) x

In Proofgold the corresponding term root is a8afcc... and proposition id is 21761c...

Proof:

Let x be given.

Assume Hx: SNo x.

An exact proof term for the current goal is Eps_i_ex (λalpha ⇒ ordinal alpha ∧ SNo_ alpha x) Hx.

∎

Theorem. (SNoLev_ordinal)

∀x, SNo x → ordinal (SNoLev x)

In Proofgold the corresponding term root is 7cacc5... and proposition id is f0e9f7...

Proof:

Let x be given.

Assume Hx.

Apply SNoLev_prop x Hx to the current goal.

Assume H1 _.

An exact proof term for the current goal is H1.

∎

Theorem. (SNoLev_)

∀x, SNo x → SNo_ (SNoLev x) x

In Proofgold the corresponding term root is 4a1033... and proposition id is 49cd5a...

Proof:

Let x be given.

Assume Hx.

Apply SNoLev_prop x Hx to the current goal.

Assume _ H1.

An exact proof term for the current goal is H1.

∎

Theorem. (SNo_PSNo_eta)

∀x, SNo x → x = PSNo (SNoLev x) (λbeta ⇒ beta ∈ x)

In Proofgold the corresponding term root is 6ffefe... and proposition id is 8c7870...

Proof:

Let x be given.

Assume Hx.

Apply SNoLev_prop x Hx to the current goal.

Assume Hx1: ordinal (SNoLev x).

Assume Hx2: SNo_ (SNoLev x) x.

Apply SNo_PSNo_eta_ to the current goal.

We will prove ordinal (SNoLev x).

An exact proof term for the current goal is Hx1.

We will prove SNo_ (SNoLev x) x.

An exact proof term for the current goal is Hx2.

∎

Theorem. (SNoLev_PSNo)

∀alpha, ordinal alpha → ∀p : set → prop, SNoLev (PSNo alpha p) = alpha

In Proofgold the corresponding term root is 07f1eb... and proposition id is 9c4890...

Proof:

Let alpha be given.

Assume Ha: ordinal alpha.

Let p be given.

We prove the intermediate claim L1: SNo_ alpha (PSNo alpha p).

An exact proof term for the current goal is SNo_PSNo alpha Ha p.

We prove the intermediate claim L2: SNo (PSNo alpha p).

We will prove ∃beta, ordinal beta ∧ SNo_ beta (PSNo alpha p).

We use alpha to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Ha.

An exact proof term for the current goal is L1.

Apply SNoLev_prop (PSNo alpha p) L2 to the current goal.

Assume H2: ordinal (SNoLev (PSNo alpha p)).

Assume H3: SNo_ (SNoLev (PSNo alpha p)) (PSNo alpha p).

An exact proof term for the current goal is SNoLev_uniq (PSNo alpha p) (SNoLev (PSNo alpha p)) alpha H2 Ha H3 L1.

∎

Theorem. (SNo_Subq)

∀x y, SNo x → SNo y → SNoLev x ⊆ SNoLev y → (∀alpha ∈ SNoLev x, alpha ∈ x ↔ alpha ∈ y) → x ⊆ y

In Proofgold the corresponding term root is a244d7... and proposition id is a428af...

Proof:

Let x and y be given.

Assume Hx Hy H1 H2.

Apply SNoLev_ x Hx to the current goal.

Assume Hx2a: x ⊆ SNoElts_ (SNoLev x).

Assume Hx2b: ∀beta ∈ SNoLev x, exactly1of2 (beta ' ∈ x) (beta ∈ x).

Apply SNoLev_ y Hy to the current goal.

Assume Hy2a: y ⊆ SNoElts_ (SNoLev y).

Assume Hy2b: ∀beta ∈ SNoLev y, exactly1of2 (beta ' ∈ y) (beta ∈ y).

Let u be given.

Assume Hu: u ∈ x.

We prove the intermediate claim L1: u ∈ SNoLev x ∪ {beta '|beta ∈ SNoLev x}.

An exact proof term for the current goal is Hx2a u Hu.

Apply binunionE (SNoLev x) {beta '|beta ∈ SNoLev x} u L1 to the current goal.

Assume H3: u ∈ SNoLev x.

Apply H2 u H3 to the current goal.

Assume H4 _.

An exact proof term for the current goal is H4 Hu.

Assume H3: u ∈ {beta '|beta ∈ SNoLev x}.

Apply ReplE_impred (SNoLev x) (λgamma ⇒ gamma ') u H3 to the current goal.

Let beta be given.

Assume H4: beta ∈ SNoLev x.

Assume H5: u = beta '.

We prove the intermediate claim L3: beta ∈ SNoLev y.

An exact proof term for the current goal is H1 beta H4.

Apply exactly1of2_E (beta ' ∈ y) (beta ∈ y) (Hy2b beta L3) to the current goal.

Assume H6: beta ' ∈ y.

Assume H7: beta ∉ y.

We will prove u ∈ y.

rewrite the current goal using H5 (from left to right).

An exact proof term for the current goal is H6.

Assume H6: beta ' ∉ y.

Assume H7: beta ∈ y.

We will prove False.

Apply exactly1of2_E (beta ' ∈ x) (beta ∈ x) (Hx2b beta H4) to the current goal.

Assume H8: beta ' ∈ x.

Assume H9: beta ∉ x.

Apply H9 to the current goal.

Apply H2 beta H4 to the current goal.

Assume _ H10.

An exact proof term for the current goal is H10 H7.

Assume H8: beta ' ∉ x.

Assume H9: beta ∈ x.

Apply H8 to the current goal.

We will prove beta ' ∈ x.

rewrite the current goal using H5 (from right to left).

An exact proof term for the current goal is Hu.

∎

Definition. We define SNoEq_ to be λalpha x y ⇒ PNoEq_ alpha (λbeta ⇒ beta ∈ x) (λbeta ⇒ beta ∈ y) of type set → set → set → prop.

In Proofgold the corresponding term root is 5f11e2... and object id is 12b5f6...

Theorem. (SNoEq_I)

∀alpha x y, (∀beta ∈ alpha, beta ∈ x ↔ beta ∈ y) → SNoEq_ alpha x y

In Proofgold the corresponding term root is a718b1... and proposition id is fdcb78...

Proof:

Let alpha, x and y be given.

Assume Hxy.

An exact proof term for the current goal is Hxy.

∎

Theorem. (SNo_eq)

∀x y, SNo x → SNo y → SNoLev x = SNoLev y → SNoEq_ (SNoLev x) x y → x = y

In Proofgold the corresponding term root is b08bdc... and proposition id is bf4ac3...

Proof:

Let x and y be given.

Assume Hx Hy H1 H2.

Apply set_ext to the current goal.

We will prove x ⊆ y.

Apply SNo_Subq x y Hx Hy to the current goal.

We will prove SNoLev x ⊆ SNoLev y.

rewrite the current goal using H1 (from right to left).

Apply Subq_ref to the current goal.

An exact proof term for the current goal is H2.

We will prove y ⊆ x.

Apply SNo_Subq y x Hy Hx to the current goal.

We will prove SNoLev y ⊆ SNoLev x.

rewrite the current goal using H1 (from left to right).

Apply Subq_ref to the current goal.

Let alpha be given.

Assume H3: alpha ∈ SNoLev y.

We will prove alpha ∈ y ↔ alpha ∈ x.

Apply iff_sym to the current goal.

We will prove alpha ∈ x ↔ alpha ∈ y.

Apply H2 alpha to the current goal.

We will prove alpha ∈ SNoLev x.

rewrite the current goal using H1 (from left to right).

An exact proof term for the current goal is H3.

∎

End of Section TaggedSets

Theorem. (SNoCutP_SNoCut)

∀L R, SNoCutP L R → SNo (SNoCut L R) ∧ SNoLev (SNoCut L R) ∈ ordsucc ((⋃_{x ∈ L}ordsucc (SNoLev x)) ∪ (⋃_{y ∈ R}ordsucc (SNoLev y))) ∧ (∀x ∈ L, x < SNoCut L R) ∧ (∀y ∈ R, SNoCut L R < y) ∧ (∀z, SNo z → (∀x ∈ L, x < z) → (∀y ∈ R, z < y) → SNoLev (SNoCut L R) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) z)

In Proofgold the corresponding term root is 9398b7... and proposition id is 66456c...

Proof:

Let L and R be given.

Assume HC: SNoCutP L R.

Apply HC to the current goal.

Assume HC.

Apply HC to the current goal.

Assume HL: ∀x ∈ L, SNo x.

Assume HR: ∀y ∈ R, SNo y.

Assume HLR: ∀x ∈ L, ∀y ∈ R, x < y.

Set L' to be the term λalpha p ⇒ ordinal alpha ∧ PSNo alpha p ∈ L of type set → (set → prop) → prop.

Set R' to be the term λalpha p ⇒ ordinal alpha ∧ PSNo alpha p ∈ R of type set → (set → prop) → prop.

Set tau to be the term PNo_bd L' R'.

Set w to be the term PNo_pred L' R'.

Set alpha to be the term ⋃_{x ∈ L}ordsucc (SNoLev x).

Set beta to be the term ⋃_{y ∈ R}ordsucc (SNoLev y).

We will prove SNo (SNoCut L R) ∧ SNoLev (SNoCut L R) ∈ ordsucc (alpha ∪ beta) ∧ (∀x ∈ L, x < SNoCut L R) ∧ (∀y ∈ R, SNoCut L R < y) ∧ (∀z, SNo z → (∀x ∈ L, x < z) → (∀y ∈ R, z < y) → SNoLev (SNoCut L R) ⊆ SNoLev z ∧ PNoEq_ (SNoLev (SNoCut L R)) (λgamma ⇒ gamma ∈ SNoCut L R) (λgamma ⇒ gamma ∈ z)).

We prove the intermediate claim LLR: PNoLt_pwise L' R'.

Let gamma be given.

Assume Hc: ordinal gamma.

Let p be given.

Assume H1: L' gamma p.

Apply H1 to the current goal.

Assume _ H1.

Let delta be given.

Assume Hd: ordinal delta.

Let q be given.

Assume H2: R' delta q.

Apply H2 to the current goal.

Assume _ H2.

We will prove PNoLt gamma p delta q.

Apply SNoLt_PSNo_PNoLt gamma delta p q Hc Hd to the current goal.

We will prove PSNo gamma p < PSNo delta q.

An exact proof term for the current goal is HLR (PSNo gamma p) H1 (PSNo delta q) H2.

We prove the intermediate claim La: ordinal alpha.

Apply ordinal_famunion L (λx ⇒ ordsucc (SNoLev x)) to the current goal.

Let x be given.

Assume Hx: x ∈ L.

We will prove ordinal (ordsucc (SNoLev x)).

Apply ordinal_ordsucc to the current goal.

Apply SNoLev_ordinal to the current goal.

We will prove SNo x.

An exact proof term for the current goal is HL x Hx.

We prove the intermediate claim Lb: ordinal beta.

Apply ordinal_famunion R (λy ⇒ ordsucc (SNoLev y)) to the current goal.

Let y be given.

Assume Hy: y ∈ R.

We will prove ordinal (ordsucc (SNoLev y)).

Apply ordinal_ordsucc to the current goal.

Apply SNoLev_ordinal to the current goal.

We will prove SNo y.

An exact proof term for the current goal is HR y Hy.

We prove the intermediate claim Lab: ordinal (alpha ∪ beta).

Apply ordinal_linear alpha beta La Lb to the current goal.

We will prove alpha ⊆ beta → ordinal (alpha ∪ beta).

rewrite the current goal using Subq_binunion_eq alpha beta (from left to right).

We will prove alpha ∪ beta = beta → ordinal (alpha ∪ beta).

Assume H1.

rewrite the current goal using H1 (from left to right).

An exact proof term for the current goal is Lb.

We will prove beta ⊆ alpha → ordinal (alpha ∪ beta).

rewrite the current goal using Subq_binunion_eq beta alpha (from left to right).

We will prove beta ∪ alpha = alpha → ordinal (alpha ∪ beta).

Assume H1.

rewrite the current goal using binunion_com (from left to right).

rewrite the current goal using H1 (from left to right).

An exact proof term for the current goal is La.

We prove the intermediate claim LLab: PNo_lenbdd (alpha ∪ beta) L'.

Let gamma be given.

Let p be given.

Assume H1.

Apply H1 to the current goal.

Assume H1: ordinal gamma.

Assume H2: PSNo gamma p ∈ L.

We will prove gamma ∈ alpha ∪ beta.

Apply binunionI1 to the current goal.

We will prove gamma ∈ ⋃_{x ∈ L}ordsucc (SNoLev x).

Apply famunionI L (λx ⇒ ordsucc (SNoLev x)) (PSNo gamma p) gamma to the current goal.

We will prove PSNo gamma p ∈ L.

An exact proof term for the current goal is H2.

We will prove gamma ∈ ordsucc (SNoLev (PSNo gamma p)).

rewrite the current goal using SNoLev_PSNo gamma H1 p (from left to right).

We will prove gamma ∈ ordsucc gamma.

Apply ordsuccI2 to the current goal.

We prove the intermediate claim LRab: PNo_lenbdd (alpha ∪ beta) R'.

Let gamma be given.

Let p be given.

Assume H1.

Apply H1 to the current goal.

Assume H1: ordinal gamma.

Assume H2: PSNo gamma p ∈ R.

We will prove gamma ∈ alpha ∪ beta.

Apply binunionI2 to the current goal.

We will prove gamma ∈ ⋃_{y ∈ R}ordsucc (SNoLev y).

Apply famunionI R (λy ⇒ ordsucc (SNoLev y)) (PSNo gamma p) gamma to the current goal.

We will prove PSNo gamma p ∈ R.

An exact proof term for the current goal is H2.

We will prove gamma ∈ ordsucc (SNoLev (PSNo gamma p)).

rewrite the current goal using SNoLev_PSNo gamma H1 p (from left to right).

We will prove gamma ∈ ordsucc gamma.

Apply ordsuccI2 to the current goal.

Apply PNo_bd_pred L' R' LLR (alpha ∪ beta) Lab LLab LRab to the current goal.

Assume H1.

Apply H1 to the current goal.

Assume H1: ordinal tau.

Assume H2: PNo_strict_imv L' R' tau w.

Assume H3: ∀gamma ∈ tau, ∀q : set → prop, ¬ PNo_strict_imv L' R' gamma q.

Apply H2 to the current goal.

Assume H4: PNo_strict_upperbd L' tau w.

Assume H5: PNo_strict_lowerbd R' tau w.

We prove the intermediate claim LNoC: SNo (SNoCut L R).

We will prove SNo (PSNo tau w).

We will prove ∃alpha, ordinal alpha ∧ SNo_ alpha (PSNo tau w).

We use tau to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is H1.

We will prove SNo_ tau (PSNo tau w).

Apply SNo_PSNo tau to the current goal.

We will prove ordinal tau.

An exact proof term for the current goal is H1.

We prove the intermediate claim LLleveqtau: SNoLev (SNoCut L R) = tau.

An exact proof term for the current goal is SNoLev_PSNo tau H1 (PNo_pred L' R').

We prove the intermediate claim LLbdtau: tau ∈ ordsucc (alpha ∪ beta).

An exact proof term for the current goal is PNo_bd_In L' R' LLR (alpha ∪ beta) Lab LLab LRab.

We prove the intermediate claim LLbd: SNoLev (SNoCut L R) ∈ ordsucc (alpha ∪ beta).

rewrite the current goal using LLleveqtau (from left to right).

An exact proof term for the current goal is LLbdtau.

We prove the intermediate claim LLecw: PNoEq_ tau (λgamma ⇒ gamma ∈ SNoCut L R) w.

We will prove PNoEq_ tau (λgamma ⇒ gamma ∈ PSNo tau w) w.

An exact proof term for the current goal is PNoEq_PSNo tau H1 w.

We prove the intermediate claim LLC: ordinal (SNoLev (SNoCut L R)).

Apply SNoLev_ordinal to the current goal.

An exact proof term for the current goal is LNoC.

We prove the intermediate claim LL: ∀x ∈ L, x < SNoCut L R.

Let x be given.

Assume Hx: x ∈ L.

We will prove x < SNoCut L R.

We will prove x < PSNo tau w.

We prove the intermediate claim L1: SNo x.

An exact proof term for the current goal is HL x Hx.

We prove the intermediate claim LLx: ordinal (SNoLev x).

An exact proof term for the current goal is SNoLev_ordinal x L1.

We prove the intermediate claim L2: x = PSNo (SNoLev x) (λgamma ⇒ gamma ∈ x).

Apply SNo_PSNo_eta to the current goal.

An exact proof term for the current goal is L1.

We prove the intermediate claim L3: L' (SNoLev x) (λgamma ⇒ gamma ∈ x).

We will prove ordinal (SNoLev x) ∧ PSNo (SNoLev x) (λgamma ⇒ gamma ∈ x) ∈ L.

Apply andI to the current goal.

An exact proof term for the current goal is LLx.

rewrite the current goal using L2 (from right to left).

An exact proof term for the current goal is Hx.

We will prove x < PSNo tau w.

rewrite the current goal using L2 (from left to right).

Apply PNoLt_SNoLt_PSNo (SNoLev x) tau (λgamma ⇒ gamma ∈ x) w LLx H1 to the current goal.

We will prove PNoLt (SNoLev x) (λgamma ⇒ gamma ∈ x) tau w.

An exact proof term for the current goal is H4 (SNoLev x) LLx (λgamma ⇒ gamma ∈ x) L3.

We prove the intermediate claim LR: ∀y ∈ R, SNoCut L R < y.

Let y be given.

Assume Hy: y ∈ R.

We will prove SNoCut L R < y.

We will prove PSNo tau w < y.

We prove the intermediate claim L1: SNo y.

An exact proof term for the current goal is HR y Hy.

We prove the intermediate claim LLy: ordinal (SNoLev y).

An exact proof term for the current goal is SNoLev_ordinal y L1.

We prove the intermediate claim L2: y = PSNo (SNoLev y) (λgamma ⇒ gamma ∈ y).

Apply SNo_PSNo_eta to the current goal.

An exact proof term for the current goal is L1.

We prove the intermediate claim L3: R' (SNoLev y) (λgamma ⇒ gamma ∈ y).

We will prove ordinal (SNoLev y) ∧ PSNo (SNoLev y) (λgamma ⇒ gamma ∈ y) ∈ R.

Apply andI to the current goal.

An exact proof term for the current goal is LLy.

rewrite the current goal using L2 (from right to left).

An exact proof term for the current goal is Hy.

We will prove PSNo tau w < y.

rewrite the current goal using L2 (from left to right).

Apply PNoLt_SNoLt_PSNo tau (SNoLev y) w (λgamma ⇒ gamma ∈ y) H1 LLy to the current goal.

We will prove PNoLt tau w (SNoLev y) (λgamma ⇒ gamma ∈ y).

An exact proof term for the current goal is H5 (SNoLev y) LLy (λgamma ⇒ gamma ∈ y) L3.

Apply and5I to the current goal.

An exact proof term for the current goal is LNoC.

An exact proof term for the current goal is LLbd.

An exact proof term for the current goal is LL.

An exact proof term for the current goal is LR.

We will prove ∀z, SNo z → (∀x ∈ L, x < z) → (∀y ∈ R, z < y) → SNoLev (SNoCut L R) ⊆ SNoLev z ∧ PNoEq_ (SNoLev (SNoCut L R)) (λgamma ⇒ gamma ∈ SNoCut L R) (λgamma ⇒ gamma ∈ z).

Let z be given.

Assume Hz: SNo z.

Assume H10: ∀x ∈ L, x < z.

Assume H11: ∀y ∈ R, z < y.

We prove the intermediate claim LLz: ordinal (SNoLev z).

Apply SNoLev_ordinal to the current goal.

An exact proof term for the current goal is Hz.

We prove the intermediate claim Lzimv: PNo_strict_imv L' R' (SNoLev z) (λgamma ⇒ gamma ∈ z).

We will prove PNo_strict_upperbd L' (SNoLev z) (λgamma ⇒ gamma ∈ z) ∧ PNo_strict_lowerbd R' (SNoLev z) (λgamma ⇒ gamma ∈ z).

Apply andI to the current goal.

Let gamma be given.

Assume Hc: ordinal gamma.

Let q be given.

Assume Hq: L' gamma q.

We will prove PNoLt gamma q (SNoLev z) (λgamma ⇒ gamma ∈ z).

Apply Hq to the current goal.

Assume Hq1: ordinal gamma.

Assume Hq2: PSNo gamma q ∈ L.

Apply SNoLt_PSNo_PNoLt gamma (SNoLev z) q (λgamma ⇒ gamma ∈ z) Hc LLz to the current goal.

We will prove PSNo gamma q < PSNo (SNoLev z) (λgamma ⇒ gamma ∈ z).

rewrite the current goal using SNo_PSNo_eta z Hz (from right to left).

We will prove PSNo gamma q < z.

An exact proof term for the current goal is H10 (PSNo gamma q) Hq2.

Let gamma be given.

Assume Hc: ordinal gamma.

Let q be given.

Assume Hq: R' gamma q.

We will prove PNoLt (SNoLev z) (λgamma ⇒ gamma ∈ z) gamma q.

Apply Hq to the current goal.

Assume Hq1: ordinal gamma.

Assume Hq2: PSNo gamma q ∈ R.

Apply SNoLt_PSNo_PNoLt (SNoLev z) gamma (λgamma ⇒ gamma ∈ z) q LLz Hc to the current goal.

We will prove PSNo (SNoLev z) (λgamma ⇒ gamma ∈ z) < PSNo gamma q.

rewrite the current goal using SNo_PSNo_eta z Hz (from right to left).

We will prove z < PSNo gamma q.

An exact proof term for the current goal is H11 (PSNo gamma q) Hq2.

We prove the intermediate claim LLznt: SNoLev z ∉ tau.

Assume H12: SNoLev z ∈ tau.

An exact proof term for the current goal is H3 (SNoLev z) H12 (λgamma ⇒ gamma ∈ z) Lzimv.

We prove the intermediate claim LLzlet: tau ⊆ SNoLev z.

Apply ordinal_In_Or_Subq (SNoLev z) tau LLz H1 to the current goal.

Assume H12: SNoLev z ∈ tau.

We will prove False.

An exact proof term for the current goal is LLznt H12.

Assume H12.

An exact proof term for the current goal is H12.

We will prove SNoLev (SNoCut L R) ⊆ SNoLev z ∧ PNoEq_ (SNoLev (SNoCut L R)) (λgamma ⇒ gamma ∈ SNoCut L R) (λgamma ⇒ gamma ∈ z).

rewrite the current goal using LLleveqtau (from left to right).

We will prove tau ⊆ SNoLev z ∧ PNoEq_ tau (λgamma ⇒ gamma ∈ SNoCut L R) (λgamma ⇒ gamma ∈ z).

Apply andI to the current goal.

We will prove tau ⊆ SNoLev z.

An exact proof term for the current goal is LLzlet.

We will prove PNoEq_ tau (λgamma ⇒ gamma ∈ SNoCut L R) (λgamma ⇒ gamma ∈ z).

Apply PNoLt_trichotomy_or_ w (λgamma ⇒ gamma ∈ z) tau H1 to the current goal.

Assume H12.

Apply H12 to the current goal.

Assume H12: PNoLt_ tau w (λgamma ⇒ gamma ∈ z).

We will prove False.

Apply H12 to the current goal.

Let delta be given.

Assume H13.

Apply H13 to the current goal.

Assume Hd: delta ∈ tau.

Assume H13.

Apply H13 to the current goal.

Assume H13.

Apply H13 to the current goal.

Assume H13: PNoEq_ delta w (λgamma ⇒ gamma ∈ z).

Assume H14: ¬ w delta.

Assume H15: delta ∈ z.

We prove the intermediate claim Ld: ordinal delta.

An exact proof term for the current goal is ordinal_Hered tau H1 delta Hd.

We prove the intermediate claim Lsd: ordinal (ordsucc delta).

An exact proof term for the current goal is ordinal_ordsucc delta Ld.

Set z0 to be the term λeps ⇒ eps ∈ z ∧ eps ≠ delta of type set → prop.

Set z1 to be the term λeps ⇒ eps ∈ z ∨ eps = delta of type set → prop.

We prove the intermediate claim Lnz0d: ¬ z0 delta.

Assume H10.

Apply H10 to the current goal.

Assume H11: delta ∈ z.

Assume H12: delta ≠ delta.

Apply H12 to the current goal.

Use reflexivity.

We prove the intermediate claim Lz1d: z1 delta.

We will prove delta ∈ z ∨ delta = delta.

Apply orIR to the current goal.

Use reflexivity.

Apply H3 delta Hd (λgamma ⇒ gamma ∈ z) to the current goal.

We will prove PNo_strict_imv L' R' delta (λgamma ⇒ gamma ∈ z).

Apply PNo_rel_split_imv_imp_strict_imv L' R' delta Ld (λgamma ⇒ gamma ∈ z) to the current goal.

We will prove PNo_rel_strict_split_imv L' R' delta (λgamma ⇒ gamma ∈ z).

We will prove PNo_rel_strict_imv L' R' (ordsucc delta) z0 ∧ PNo_rel_strict_imv L' R' (ordsucc delta) z1.

Apply andI to the current goal.

We will prove PNo_rel_strict_imv L' R' (ordsucc delta) z0.

Apply PNoEq_rel_strict_imv L' R' (ordsucc delta) Lsd w z0 to the current goal.

We will prove PNoEq_ (ordsucc delta) w z0.

Let eps be given.

Assume He: eps ∈ ordsucc delta.

Apply ordsuccE delta eps He to the current goal.

Assume He1: eps ∈ delta.

Apply iff_trans (w eps) (eps ∈ z) (z0 eps) to the current goal.

An exact proof term for the current goal is H13 eps He1.

An exact proof term for the current goal is PNo_extend0_eq delta (λgamma ⇒ gamma ∈ z) eps He1.

Assume He1: eps = delta.

We will prove w eps ↔ z0 eps.

rewrite the current goal using He1 (from left to right).

We will prove w delta ↔ z0 delta.

Apply iffI to the current goal.

Assume H16: w delta.

We will prove False.

An exact proof term for the current goal is H14 H16.

Assume H16: z0 delta.

We will prove False.

An exact proof term for the current goal is Lnz0d H16.

We will prove PNo_rel_strict_imv L' R' (ordsucc delta) w.

Apply PNo_strict_imv_imp_rel_strict_imv L' R' tau H1 (ordsucc delta) to the current goal.

We will prove ordsucc delta ∈ ordsucc tau.

Apply ordinal_ordsucc_In tau H1 to the current goal.

An exact proof term for the current goal is Hd.

We will prove PNo_strict_imv L' R' tau w.

An exact proof term for the current goal is H2.

We will prove PNo_rel_strict_imv L' R' (ordsucc delta) z1.

Apply PNoEq_rel_strict_imv L' R' (ordsucc delta) Lsd (λgamma ⇒ gamma ∈ z) z1 to the current goal.

We will prove PNoEq_ (ordsucc delta) (λgamma ⇒ gamma ∈ z) z1.

Let eps be given.

Assume He: eps ∈ ordsucc delta.

Apply ordsuccE delta eps He to the current goal.

Assume He1: eps ∈ delta.

An exact proof term for the current goal is PNo_extend1_eq delta (λgamma ⇒ gamma ∈ z) eps He1.

Assume He1: eps = delta.

We will prove eps ∈ z ↔ z1 eps.

rewrite the current goal using He1 (from left to right).

We will prove delta ∈ z ↔ z1 delta.

Apply iffI to the current goal.

Assume _.

An exact proof term for the current goal is Lz1d.

Assume _.

An exact proof term for the current goal is H15.

We will prove PNo_rel_strict_imv L' R' (ordsucc delta) (λgamma ⇒ gamma ∈ z).

Apply PNo_strict_imv_imp_rel_strict_imv L' R' (SNoLev z) LLz (ordsucc delta) to the current goal.

We will prove ordsucc delta ∈ ordsucc (SNoLev z).

Apply ordinal_ordsucc_In (SNoLev z) LLz to the current goal.

We will prove delta ∈ SNoLev z.

Apply LLzlet to the current goal.

We will prove delta ∈ tau.

An exact proof term for the current goal is Hd.

We will prove PNo_strict_imv L' R' (SNoLev z) (λgamma ⇒ gamma ∈ z).

An exact proof term for the current goal is Lzimv.

Assume H12: PNoEq_ tau w (λgamma ⇒ gamma ∈ z).

Apply PNoEq_tra_ tau (λgamma ⇒ gamma ∈ SNoCut L R) w (λgamma ⇒ gamma ∈ z) to the current goal.

We will prove PNoEq_ tau (λgamma ⇒ gamma ∈ SNoCut L R) w.

An exact proof term for the current goal is LLecw.

We will prove PNoEq_ tau w (λgamma ⇒ gamma ∈ z).

An exact proof term for the current goal is H12.

Assume H12: PNoLt_ tau (λgamma ⇒ gamma ∈ z) w.

We will prove False.

Apply H12 to the current goal.

Let delta be given.

Assume H13.

Apply H13 to the current goal.

Assume Hd: delta ∈ tau.

Assume H13.

Apply H13 to the current goal.

Assume H13.

Apply H13 to the current goal.

Assume H13: PNoEq_ delta (λgamma ⇒ gamma ∈ z) w.

Assume H14: delta ∉ z.

Assume H15: w delta.

We prove the intermediate claim Ld: ordinal delta.

An exact proof term for the current goal is ordinal_Hered tau H1 delta Hd.

We prove the intermediate claim Lsd: ordinal (ordsucc delta).

An exact proof term for the current goal is ordinal_ordsucc delta Ld.

Set z0 to be the term λeps ⇒ eps ∈ z ∧ eps ≠ delta of type set → prop.

Set z1 to be the term λeps ⇒ eps ∈ z ∨ eps = delta of type set → prop.

We prove the intermediate claim Lnz0d: ¬ z0 delta.

Assume H10.

Apply H10 to the current goal.

Assume H11: delta ∈ z.

Assume H12: delta ≠ delta.

Apply H12 to the current goal.

Use reflexivity.

We prove the intermediate claim Lz1d: z1 delta.

We will prove delta ∈ z ∨ delta = delta.

Apply orIR to the current goal.

Use reflexivity.

Apply H3 delta Hd (λgamma ⇒ gamma ∈ z) to the current goal.

We will prove PNo_strict_imv L' R' delta (λgamma ⇒ gamma ∈ z).

Apply PNo_rel_split_imv_imp_strict_imv L' R' delta Ld (λgamma ⇒ gamma ∈ z) to the current goal.

We will prove PNo_rel_strict_split_imv L' R' delta (λgamma ⇒ gamma ∈ z).

We will prove PNo_rel_strict_imv L' R' (ordsucc delta) z0 ∧ PNo_rel_strict_imv L' R' (ordsucc delta) z1.

Apply andI to the current goal.

We will prove PNo_rel_strict_imv L' R' (ordsucc delta) z0.

Apply PNoEq_rel_strict_imv L' R' (ordsucc delta) Lsd (λgamma ⇒ gamma ∈ z) z0 to the current goal.

We will prove PNoEq_ (ordsucc delta) (λgamma ⇒ gamma ∈ z) z0.

Let eps be given.

Assume He: eps ∈ ordsucc delta.

Apply ordsuccE delta eps He to the current goal.

Assume He1: eps ∈ delta.

An exact proof term for the current goal is PNo_extend0_eq delta (λgamma ⇒ gamma ∈ z) eps He1.

Assume He1: eps = delta.

We will prove eps ∈ z ↔ z0 eps.

rewrite the current goal using He1 (from left to right).

We will prove delta ∈ z ↔ z0 delta.

Apply iffI to the current goal.

Assume H16: delta ∈ z.

We will prove False.

An exact proof term for the current goal is H14 H16.

Assume H16: z0 delta.

We will prove False.

An exact proof term for the current goal is Lnz0d H16.

We will prove PNo_rel_strict_imv L' R' (ordsucc delta) (λgamma ⇒ gamma ∈ z).

Apply PNo_strict_imv_imp_rel_strict_imv L' R' (SNoLev z) LLz (ordsucc delta) to the current goal.

We will prove ordsucc delta ∈ ordsucc (SNoLev z).

Apply ordinal_ordsucc_In (SNoLev z) LLz to the current goal.

We will prove delta ∈ SNoLev z.

Apply LLzlet to the current goal.

We will prove delta ∈ tau.

An exact proof term for the current goal is Hd.

We will prove PNo_strict_imv L' R' (SNoLev z) (λgamma ⇒ gamma ∈ z).

An exact proof term for the current goal is Lzimv.

We will prove PNo_rel_strict_imv L' R' (ordsucc delta) z1.

Apply PNoEq_rel_strict_imv L' R' (ordsucc delta) Lsd w z1 to the current goal.

We will prove PNoEq_ (ordsucc delta) w z1.

Let eps be given.

Assume He: eps ∈ ordsucc delta.

Apply ordsuccE delta eps He to the current goal.

Assume He1: eps ∈ delta.

Apply iff_trans (w eps) (eps ∈ z) (z1 eps) to the current goal.

Apply iff_sym to the current goal.

An exact proof term for the current goal is H13 eps He1.

An exact proof term for the current goal is PNo_extend1_eq delta (λgamma ⇒ gamma ∈ z) eps He1.

Assume He1: eps = delta.

We will prove w eps ↔ z1 eps.

rewrite the current goal using He1 (from left to right).

We will prove w delta ↔ z1 delta.

Apply iffI to the current goal.

Assume _.

An exact proof term for the current goal is Lz1d.

Assume _.

An exact proof term for the current goal is H15.

We will prove PNo_rel_strict_imv L' R' (ordsucc delta) w.

Apply PNo_strict_imv_imp_rel_strict_imv L' R' tau H1 (ordsucc delta) to the current goal.

We will prove ordsucc delta ∈ ordsucc tau.

Apply ordinal_ordsucc_In tau H1 to the current goal.

An exact proof term for the current goal is Hd.

We will prove PNo_strict_imv L' R' tau w.

An exact proof term for the current goal is H2.

∎

Beginning of Section TaggedSets2

Let tag : set → set ≝ λalpha ⇒ SetAdjoin alpha {1}

Notation. We use ' as a postfix operator with priority 100 corresponding to applying term tag.

Theorem. (SNoS_I)

∀alpha, ordinal alpha → ∀x, ∀beta ∈ alpha, SNo_ beta x → x ∈ SNoS_ alpha

In Proofgold the corresponding term root is f5227d... and proposition id is 04f24b...

Proof:

Let alpha be given.

Assume Ha: ordinal alpha.

Let x be given.

Let beta be given.

Assume Hb: beta ∈ alpha.

Assume H1: SNo_ beta x.

Apply H1 to the current goal.

Assume H2: x ⊆ SNoElts_ beta.

Assume H3: ∀gamma ∈ beta, exactly1of2 (gamma ' ∈ x) (gamma ∈ x).

We will prove x ∈ SNoS_ alpha.

We will prove x ∈ {x ∈ 𝒫 (SNoElts_ alpha)|∃gamma ∈ alpha, SNo_ gamma x}.

Apply SepI to the current goal.

We will prove x ∈ 𝒫 (SNoElts_ alpha).

Apply PowerI to the current goal.

We will prove x ⊆ SNoElts_ alpha.

Apply Subq_tra x (SNoElts_ beta) (SNoElts_ alpha) H2 to the current goal.

We will prove SNoElts_ beta ⊆ SNoElts_ alpha.

Apply SNoElts_mon to the current goal.

Apply Ha to the current goal.

Assume Ha1 _.

An exact proof term for the current goal is Ha1 beta Hb.

We will prove ∃gamma ∈ alpha, SNo_ gamma x.

We use beta to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hb.

An exact proof term for the current goal is H1.

∎

Theorem. (SNoS_I2)

∀x y, SNo x → SNo y → SNoLev x ∈ SNoLev y → x ∈ SNoS_ (SNoLev y)

In Proofgold the corresponding term root is 7a14c7... and proposition id is b4042d...

Proof:

Let x and y be given.

Assume Hx Hy Hxy.

An exact proof term for the current goal is SNoS_I (SNoLev y) (SNoLev_ordinal y Hy) x (SNoLev x) Hxy (SNoLev_ x Hx).

∎

Theorem. (SNoS_Subq)

∀alpha beta, ordinal alpha → ordinal beta → alpha ⊆ beta → SNoS_ alpha ⊆ SNoS_ beta

In Proofgold the corresponding term root is 6828e7... and proposition id is d928b8...

Proof:

Let alpha and beta be given.

Assume Ha Hb Hab.

Let x be given.

Assume Hx: x ∈ SNoS_ alpha.

Apply SNoS_E alpha Ha x Hx to the current goal.

Let gamma be given.

Assume Hc.

Apply Hc to the current goal.

Assume Hc1: gamma ∈ alpha.

Assume Hc2: SNo_ gamma x.

An exact proof term for the current goal is SNoS_I beta Hb x gamma (Hab gamma Hc1) Hc2.

∎

Theorem. (SNoLev_uniq2)

∀alpha, ordinal alpha → ∀x, SNo_ alpha x → SNoLev x = alpha

In Proofgold the corresponding term root is fbb461... and proposition id is f48d47...

Proof:

Let alpha be given.

Assume Ha.

Let x be given.

Assume Hx.

Apply SNoLev_prop x (SNo_SNo alpha Ha x Hx) to the current goal.

Assume Hx1: ordinal (SNoLev x).

Assume Hx2: SNo_ (SNoLev x) x.

Apply SNoLev_uniq x to the current goal.

An exact proof term for the current goal is Hx1.

An exact proof term for the current goal is Ha.

An exact proof term for the current goal is Hx2.

An exact proof term for the current goal is Hx.

∎

Theorem. (SNoS_E2)

∀alpha, ordinal alpha → ∀x ∈ SNoS_ alpha, ∀p : prop, (SNoLev x ∈ alpha → ordinal (SNoLev x) → SNo x → SNo_ (SNoLev x) x → p) → p

In Proofgold the corresponding term root is deb031... and proposition id is 62b490...

Proof:

Let alpha be given.

Assume Ha.

Let x be given.

Assume Hx.

Let p be given.

Assume Hp.

Apply SNoS_E alpha Ha x Hx to the current goal.

Let beta be given.

Assume H1.

Apply H1 to the current goal.

Assume Hb: beta ∈ alpha.

Assume H1: SNo_ beta x.

We prove the intermediate claim Lb: ordinal beta.

An exact proof term for the current goal is ordinal_Hered alpha Ha beta Hb.

We prove the intermediate claim Lx: SNo x.

An exact proof term for the current goal is SNo_SNo beta Lb x H1.

Apply SNoLev_prop x Lx to the current goal.

Assume Hx1: ordinal (SNoLev x).

Assume Hx2: SNo_ (SNoLev x) x.

We prove the intermediate claim Lxb: SNoLev x = beta.

An exact proof term for the current goal is SNoLev_uniq2 beta Lb x H1.

We prove the intermediate claim Lxa: SNoLev x ∈ alpha.

rewrite the current goal using Lxb (from left to right).

An exact proof term for the current goal is Hb.

An exact proof term for the current goal is Hp Lxa Hx1 Lx Hx2.

∎

Theorem. (SNoS_In_neq)

∀w, SNo w → ∀x ∈ SNoS_ (SNoLev w), x ≠ w

In Proofgold the corresponding term root is ab85fd... and proposition id is d5dbd7...

Proof:

Let w be given.

Assume Hw: SNo w.

Let x be given.

Assume Hx: x ∈ SNoS_ (SNoLev w).

Assume Hxw: x = w.

Apply SNoLev_prop w Hw to the current goal.

Assume Hw1: ordinal (SNoLev w).

Assume Hw2: SNo_ (SNoLev w) w.

Apply SNoS_E2 (SNoLev w) Hw1 x Hx to the current goal.

Assume Hx1: SNoLev x ∈ SNoLev w.

Assume Hx2: ordinal (SNoLev x).

Assume Hx3: SNo x.

Assume Hx4: SNo_ (SNoLev x) x.

We will prove False.

Apply In_irref (SNoLev x) to the current goal.

rewrite the current goal using Hxw (from left to right) at position 2.

An exact proof term for the current goal is Hx1.

∎

Theorem. (SNoS_SNoLev)

∀z, SNo z → z ∈ SNoS_ (ordsucc (SNoLev z))

In Proofgold the corresponding term root is a9ba1f... and proposition id is 8efb88...

Proof:

Let z be given.

Assume Hz: SNo z.

Apply SNoLev_prop z Hz to the current goal.

Assume Hz1: ordinal (SNoLev z).

Assume Hz2: SNo_ (SNoLev z) z.

An exact proof term for the current goal is SNoS_I (ordsucc (SNoLev z)) (ordinal_ordsucc (SNoLev z) Hz1) z (SNoLev z) (ordsuccI2 (SNoLev z)) Hz2.

∎

Definition. We define SNoL to be λz ⇒ {x ∈ SNoS_ (SNoLev z)|x < z} of type set → set.

In Proofgold the corresponding term root is 8cd812... and object id is 48bcf8...

Definition. We define SNoR to be λz ⇒ {y ∈ SNoS_ (SNoLev z)|z < y} of type set → set.

In Proofgold the corresponding term root is 73b2b9... and object id is 0cfe87...

Theorem. (SNoCutP_SNoL_SNoR)

∀z, SNo z → SNoCutP (SNoL z) (SNoR z)

In Proofgold the corresponding term root is 524866... and proposition id is 7aba57...

Proof:

Let z be given.

Assume Hz: SNo z.

Set L to be the term SNoL z.

Set R to be the term SNoR z.

We prove the intermediate claim LLz: ordinal (SNoLev z).

An exact proof term for the current goal is SNoLev_ordinal z Hz.

We prove the intermediate claim L1: ∀x ∈ L, SNo x.

Let x be given.

Assume Hx: x ∈ L.

We will prove ∃alpha, ordinal alpha ∧ SNo_ alpha x.

We prove the intermediate claim L1a: x ∈ SNoS_ (SNoLev z).

An exact proof term for the current goal is SepE1 (SNoS_ (SNoLev z)) (λx ⇒ x < z) x Hx.

Apply SNoS_E (SNoLev z) LLz x L1a to the current goal.

Let beta be given.

Assume H1.

Apply H1 to the current goal.

Assume Hb: beta ∈ SNoLev z.

Assume H1: SNo_ beta x.

We use beta to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is ordinal_Hered (SNoLev z) LLz beta Hb.

An exact proof term for the current goal is H1.

We prove the intermediate claim L2: ∀y ∈ R, SNo y.

Let y be given.

Assume Hy: y ∈ R.

We will prove ∃alpha, ordinal alpha ∧ SNo_ alpha y.

We prove the intermediate claim L2a: y ∈ SNoS_ (SNoLev z).

An exact proof term for the current goal is SepE1 (SNoS_ (SNoLev z)) (λy ⇒ z < y) y Hy.

Apply SNoS_E (SNoLev z) LLz y L2a to the current goal.

Let beta be given.

Assume H1.

Apply H1 to the current goal.

Assume Hb: beta ∈ SNoLev z.

Assume H1: SNo_ beta y.

We use beta to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is ordinal_Hered (SNoLev z) LLz beta Hb.

An exact proof term for the current goal is H1.

We prove the intermediate claim L3: ∀x ∈ L, ∀y ∈ R, x < y.

Let x be given.

Assume Hx.

Let y be given.

Assume Hy.

Apply SNoLt_tra x z y (L1 x Hx) Hz (L2 y Hy) to the current goal.

We will prove x < z.

An exact proof term for the current goal is SepE2 (SNoS_ (SNoLev z)) (λx ⇒ x < z) x Hx.

We will prove z < y.

An exact proof term for the current goal is SepE2 (SNoS_ (SNoLev z)) (λy ⇒ z < y) y Hy.

We will prove SNoCutP L R.

We will prove (∀x ∈ L, SNo x) ∧ (∀y ∈ R, SNo y) ∧ (∀x ∈ L, ∀y ∈ R, x < y).

Apply and3I to the current goal.

An exact proof term for the current goal is L1.

An exact proof term for the current goal is L2.

An exact proof term for the current goal is L3.

∎

Theorem. (SNoL_E)

∀x, SNo x → ∀w ∈ SNoL x, ∀p : prop, (SNo w → SNoLev w ∈ SNoLev x → w < x → p) → p

In Proofgold the corresponding term root is cead4f... and proposition id is 7ccd8b...

Proof:

Let x be given.

Assume Hx: SNo x.

Let w be given.

Assume Hw: w ∈ SNoL x.

Let p be given.

Assume Hp.

Apply SepE (SNoS_ (SNoLev x)) (λw ⇒ w < x) w Hw to the current goal.

Assume Hw1: w ∈ SNoS_ (SNoLev x).

Assume Hw2: w < x.

Apply SNoS_E2 (SNoLev x) (SNoLev_ordinal x Hx) w Hw1 to the current goal.

Assume Hw3: SNoLev w ∈ SNoLev x.

Assume Hw4: ordinal (SNoLev w).

Assume Hw5: SNo w.

Assume Hw6: SNo_ (SNoLev w) w.

An exact proof term for the current goal is Hp Hw5 Hw3 Hw2.

∎

Theorem. (SNoR_E)

∀x, SNo x → ∀z ∈ SNoR x, ∀p : prop, (SNo z → SNoLev z ∈ SNoLev x → x < z → p) → p

In Proofgold the corresponding term root is efca05... and proposition id is 7dca04...

Proof:

Let x be given.

Assume Hx: SNo x.

Let z be given.

Assume Hz: z ∈ SNoR x.

Let p be given.

Assume Hp.

Apply SepE (SNoS_ (SNoLev x)) (λz ⇒ x < z) z Hz to the current goal.

Assume Hz1: z ∈ SNoS_ (SNoLev x).

Assume Hz2: x < z.

Apply SNoS_E2 (SNoLev x) (SNoLev_ordinal x Hx) z Hz1 to the current goal.

Assume Hz3: SNoLev z ∈ SNoLev x.

Assume Hz4: ordinal (SNoLev z).

Assume Hz5: SNo z.

Assume Hz6: SNo_ (SNoLev z) z.

An exact proof term for the current goal is Hp Hz5 Hz3 Hz2.

∎

Theorem. (SNoL_SNoS_)

∀z, SNoL z ⊆ SNoS_ (SNoLev z)

In Proofgold the corresponding term root is 73f5b2... and proposition id is 409713...

Proof:

Let z be given.

An exact proof term for the current goal is Sep_Subq (SNoS_ (SNoLev z)) (λx ⇒ x < z).

∎

Theorem. (SNoR_SNoS_)

∀z, SNoR z ⊆ SNoS_ (SNoLev z)

In Proofgold the corresponding term root is 16bdfc... and proposition id is 2fe1c0...

Proof:

Let z be given.

An exact proof term for the current goal is Sep_Subq (SNoS_ (SNoLev z)) (λy ⇒ z < y).

∎

Theorem. (SNoL_SNoS)

∀x, SNo x → ∀w ∈ SNoL x, w ∈ SNoS_ (SNoLev x)

In Proofgold the corresponding term root is 6e3a22... and proposition id is ded78a...

Proof:

Let x be given.

Assume Hx.

Let w be given.

Assume Hw: w ∈ SNoL x.

Apply SNoL_E x Hx w Hw to the current goal.

Assume Hw1: SNo w.

Assume Hw2: SNoLev w ∈ SNoLev x.

Assume Hw3: w < x.

We will prove w ∈ SNoS_ (SNoLev x).

An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.

∎

Theorem. (SNoR_SNoS)

∀x, SNo x → ∀z ∈ SNoR x, z ∈ SNoS_ (SNoLev x)

In Proofgold the corresponding term root is 98051c... and proposition id is e13f49...

Proof:

Let x be given.

Assume Hx.

Let z be given.

Assume Hz: z ∈ SNoR x.

Apply SNoR_E x Hx z Hz to the current goal.

Assume Hz1: SNo z.

Assume Hz2: SNoLev z ∈ SNoLev x.

Assume Hz3: x < z.

We will prove z ∈ SNoS_ (SNoLev x).

An exact proof term for the current goal is SNoS_I2 z x Hz1 Hx Hz2.

∎

Theorem. (SNoL_I)

∀z, SNo z → ∀x, SNo x → SNoLev x ∈ SNoLev z → x < z → x ∈ SNoL z

In Proofgold the corresponding term root is ddd91b... and proposition id is 4f3d04...

Proof:

Let z be given.

Assume Hz.

Let x be given.

Assume Hx Hxz1 Hxz2.

We will prove x ∈ SNoL z.

We will prove x ∈ {x ∈ SNoS_ (SNoLev z)|x < z}.

Apply SepI to the current goal.

We will prove x ∈ SNoS_ (SNoLev z).

An exact proof term for the current goal is SNoS_I2 x z Hx Hz Hxz1.

We will prove x < z.

An exact proof term for the current goal is Hxz2.

∎

Theorem. (SNoR_I)

∀z, SNo z → ∀y, SNo y → SNoLev y ∈ SNoLev z → z < y → y ∈ SNoR z

In Proofgold the corresponding term root is 97693c... and proposition id is 383e88...

Proof:

Let z be given.

Assume Hz.

Let y be given.

Assume Hy Hyz Hzy.

We will prove y ∈ SNoR z.

We will prove y ∈ {y ∈ SNoS_ (SNoLev z)|z < y}.

Apply SepI to the current goal.

We will prove y ∈ SNoS_ (SNoLev z).

An exact proof term for the current goal is SNoS_I2 y z Hy Hz Hyz.

We will prove z < y.

An exact proof term for the current goal is Hzy.

∎

Theorem. (SNo_eta)

∀z, SNo z → z = SNoCut (SNoL z) (SNoR z)

In Proofgold the corresponding term root is 3cc369... and proposition id is dc9273...

Proof:

Let z be given.

Assume Hz: SNo z.

Set L to be the term SNoL z.

Set R to be the term SNoR z.

We prove the intermediate claim LLz: ordinal (SNoLev z).

An exact proof term for the current goal is SNoLev_ordinal z Hz.

We prove the intermediate claim LC: SNoCutP L R.

An exact proof term for the current goal is SNoCutP_SNoL_SNoR z Hz.

Apply SNoCutP_SNoCut L R LC to the current goal.

Assume H1.

Apply H1 to the current goal.

Assume H1.

Apply H1 to the current goal.

Assume H1.

Apply H1 to the current goal.

Assume H1: SNo (SNoCut L R).

Assume H2: SNoLev (SNoCut L R) ∈ ordsucc ((⋃_{x ∈ L}ordsucc (SNoLev x)) ∪ (⋃_{y ∈ R}ordsucc (SNoLev y))).

Assume H3: ∀x ∈ L, x < SNoCut L R.

Assume H4: ∀y ∈ R, SNoCut L R < y.

Assume H5: ∀z, SNo z → (∀x ∈ L, x < z) → (∀y ∈ R, z < y) → SNoLev (SNoCut L R) ⊆ SNoLev z ∧ PNoEq_ (SNoLev (SNoCut L R)) (λgamma ⇒ gamma ∈ SNoCut L R) (λgamma ⇒ gamma ∈ z).

We prove the intermediate claim L4: ordinal (SNoLev (SNoCut L R)).

Apply SNoLev_ordinal to the current goal.

An exact proof term for the current goal is H1.

We prove the intermediate claim L5: ∀x ∈ L, x < z.

Let x be given.

Assume Hx: x ∈ L.

An exact proof term for the current goal is SepE2 (SNoS_ (SNoLev z)) (λx ⇒ x < z) x Hx.

We prove the intermediate claim L6: ∀y ∈ R, z < y.

Let y be given.

Assume Hy: y ∈ R.

An exact proof term for the current goal is SepE2 (SNoS_ (SNoLev z)) (λy ⇒ z < y) y Hy.

Apply H5 z Hz L5 L6 to the current goal.

Assume H6: SNoLev (SNoCut L R) ⊆ SNoLev z.

Assume H7: PNoEq_ (SNoLev (SNoCut L R)) (λgamma ⇒ gamma ∈ SNoCut L R) (λgamma ⇒ gamma ∈ z).

We prove the intermediate claim L7: SNoLev (SNoCut L R) = SNoLev z.

Apply ordinal_trichotomy_or (SNoLev (SNoCut L R)) (SNoLev z) L4 LLz to the current goal.

Assume H8.

Apply H8 to the current goal.

Assume H8: SNoLev (SNoCut L R) ∈ SNoLev z.

We will prove False.

Apply SNoLt_trichotomy_or z (SNoCut L R) Hz H1 to the current goal.

Assume H9.

Apply H9 to the current goal.

Assume H9: z < SNoCut L R.

Apply SNoLt_irref (SNoCut L R) to the current goal.

Apply H4 to the current goal.

We will prove SNoCut L R ∈ R.

We will prove SNoCut L R ∈ {y ∈ SNoS_ (SNoLev z)|z < y}.

Apply SepI to the current goal.

Apply SNoS_I (SNoLev z) LLz (SNoCut L R) (SNoLev (SNoCut L R)) H8 to the current goal.

We will prove SNo_ (SNoLev (SNoCut L R)) (SNoCut L R).

An exact proof term for the current goal is SNoLev_ (SNoCut L R) H1.

We will prove z < SNoCut L R.

An exact proof term for the current goal is H9.

Assume H9: z = SNoCut L R.

Apply In_irref (SNoLev z) to the current goal.

rewrite the current goal using H9 (from left to right) at position 1.

An exact proof term for the current goal is H8.

Assume H9: SNoCut L R < z.

Apply SNoLt_irref (SNoCut L R) to the current goal.

Apply H3 to the current goal.

We will prove SNoCut L R ∈ L.

We will prove SNoCut L R ∈ {x ∈ SNoS_ (SNoLev z)|x < z}.

Apply SepI to the current goal.

Apply SNoS_I (SNoLev z) LLz (SNoCut L R) (SNoLev (SNoCut L R)) H8 to the current goal.

We will prove SNo_ (SNoLev (SNoCut L R)) (SNoCut L R).

An exact proof term for the current goal is SNoLev_ (SNoCut L R) H1.

We will prove SNoCut L R < z.

An exact proof term for the current goal is H9.

Assume H8: SNoLev (SNoCut L R) = SNoLev z.

An exact proof term for the current goal is H8.

Assume H8: SNoLev z ∈ SNoLev (SNoCut L R).

We will prove False.

Apply In_irref (SNoLev z) to the current goal.

Apply H6 to the current goal.

An exact proof term for the current goal is H8.

We will prove z = SNoCut L R.

Use symmetry.

We will prove SNoCut L R = z.

Apply SNo_eq to the current goal.

We will prove SNo (SNoCut L R).

An exact proof term for the current goal is H1.

We will prove SNo z.

An exact proof term for the current goal is Hz.

We will prove SNoLev (SNoCut L R) = SNoLev z.

An exact proof term for the current goal is L7.

We will prove ∀alpha ∈ SNoLev (SNoCut L R), alpha ∈ SNoCut L R ↔ alpha ∈ z.

An exact proof term for the current goal is H7.

∎

Theorem. (SNoCutP_SNo_SNoCut)

∀L R, SNoCutP L R → SNo (SNoCut L R)

In Proofgold the corresponding term root is 9621aa... and proposition id is ae46e8...

Proof:

Let L and R be given.

Assume H1: SNoCutP L R.

Apply SNoCutP_SNoCut L R H1 to the current goal.

Assume H2 _.

Apply H2 to the current goal.

Assume H2 _.

Apply H2 to the current goal.

Assume H2 _.

Apply H2 to the current goal.

Assume H2 _.

An exact proof term for the current goal is H2.

∎

Theorem. (SNoCutP_SNoCut_L)

∀L R, SNoCutP L R → ∀x ∈ L, x < SNoCut L R

In Proofgold the corresponding term root is 984a30... and proposition id is 4bca14...

Proof:

Let L and R be given.

Assume H1: SNoCutP L R.

Apply SNoCutP_SNoCut L R H1 to the current goal.

Assume H2 _.

Apply H2 to the current goal.

Assume H2 _.

Apply H2 to the current goal.

Assume _ H2.

An exact proof term for the current goal is H2.

∎

Theorem. (SNoCutP_SNoCut_R)

∀L R, SNoCutP L R → ∀y ∈ R, SNoCut L R < y

In Proofgold the corresponding term root is 9161db... and proposition id is 7c3d12...

Proof:

Let L and R be given.

Assume H1: SNoCutP L R.

Apply SNoCutP_SNoCut L R H1 to the current goal.

Assume H2 _.

Apply H2 to the current goal.

Assume _ H2.

An exact proof term for the current goal is H2.

∎

Theorem. (SNoCutP_SNoCut_fst)

∀L R, SNoCutP L R → ∀z, SNo z → (∀x ∈ L, x < z) → (∀y ∈ R, z < y) → SNoLev (SNoCut L R) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) z

In Proofgold the corresponding term root is b52eb7... and proposition id is 8362f8...

Proof:

Let L and R be given.

Assume H1: SNoCutP L R.

Apply SNoCutP_SNoCut L R H1 to the current goal.

Assume _ H2.

An exact proof term for the current goal is H2.

∎

Theorem. (SNoCut_Le)

∀L1 R1 L2 R2, SNoCutP L1 R1 → SNoCutP L2 R2 → (∀w ∈ L1, w < SNoCut L2 R2) → (∀z ∈ R2, SNoCut L1 R1 < z) → SNoCut L1 R1 ≤ SNoCut L2 R2

In Proofgold the corresponding term root is bb8cdc... and proposition id is 423731...

Proof:

Let L1, R1, L2 and R2 be given.

Assume HLR1 HLR2.

Assume H1: ∀w ∈ L1, w < SNoCut L2 R2.

Assume H2: ∀z ∈ R2, SNoCut L1 R1 < z.

Apply HLR1 to the current goal.

Assume HLR1a.

Apply HLR1a to the current goal.

Assume HLR1a: ∀x ∈ L1, SNo x.

Assume HLR1b: ∀y ∈ R1, SNo y.

Assume HLR1c: ∀x ∈ L1, ∀y ∈ R1, x < y.

Apply HLR2 to the current goal.

Assume HLR2a.

Apply HLR2a to the current goal.

Assume HLR2a: ∀x ∈ L2, SNo x.

Assume HLR2b: ∀y ∈ R2, SNo y.

Assume HLR2c: ∀x ∈ L2, ∀y ∈ R2, x < y.

Set alpha to be the term ⋃_{x ∈ L1}ordsucc (SNoLev x).

Set beta to be the term ⋃_{y ∈ R1}ordsucc (SNoLev y).

Set gamma to be the term ⋃_{x ∈ L2}ordsucc (SNoLev x).

Set delta to be the term ⋃_{y ∈ R2}ordsucc (SNoLev y).

Apply SNoCutP_SNoCut L1 R1 HLR1 to the current goal.

Assume H3.

Apply H3 to the current goal.

Assume H3.

Apply H3 to the current goal.

Assume H3.

Apply H3 to the current goal.

Assume H3: SNo (SNoCut L1 R1).

Assume H4: SNoLev (SNoCut L1 R1) ∈ ordsucc (alpha ∪ beta).

Assume H5: ∀x ∈ L1, x < SNoCut L1 R1.

Assume H6: ∀y ∈ R1, SNoCut L1 R1 < y.

Assume H7: ∀z, SNo z → (∀x ∈ L1, x < z) → (∀y ∈ R1, z < y) → SNoLev (SNoCut L1 R1) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (SNoCut L1 R1)) (SNoCut L1 R1) z.

Apply SNoCutP_SNoCut L2 R2 HLR2 to the current goal.

Assume H8.

Apply H8 to the current goal.

Assume H8.

Apply H8 to the current goal.

Assume H8.

Apply H8 to the current goal.

Assume H8: SNo (SNoCut L2 R2).

Assume H9: SNoLev (SNoCut L2 R2) ∈ ordsucc (gamma ∪ delta).

Assume H10: ∀x ∈ L2, x < SNoCut L2 R2.

Assume H11: ∀y ∈ R2, SNoCut L2 R2 < y.

Assume H12: ∀z, SNo z → (∀x ∈ L2, x < z) → (∀y ∈ R2, z < y) → SNoLev (SNoCut L2 R2) ⊆ SNoLev z ∧ SNoEq_ (SNoLev (SNoCut L2 R2)) (SNoCut L2 R2) z.

Apply SNoLtLe_or (SNoCut L2 R2) (SNoCut L1 R1) H8 H3 to the current goal.

Assume H13: SNoCut L2 R2 < SNoCut L1 R1.

We will prove False.

Apply SNoLtE (SNoCut L2 R2) (SNoCut L1 R1) H8 H3 H13 to the current goal.

Let z be given.

Assume Hz1: SNo z.

Assume Hz2: SNoLev z ∈ SNoLev (SNoCut L2 R2) ∩ SNoLev (SNoCut L1 R1).

Assume Hz3: SNoEq_ (SNoLev z) z (SNoCut L2 R2).

Assume Hz4: SNoEq_ (SNoLev z) z (SNoCut L1 R1).

Assume Hz5: (SNoCut L2 R2) < z.

Assume Hz6: z < (SNoCut L1 R1).

Assume Hz7: SNoLev z ∉ (SNoCut L2 R2).

Assume Hz8: SNoLev z ∈ (SNoCut L1 R1).

We prove the intermediate claim LzL1: ∀x ∈ L1, x < z.

Let x be given.

Assume Hx: x ∈ L1.

Apply SNoLt_tra x (SNoCut L2 R2) z (HLR1a x Hx) H8 Hz1 to the current goal.

We will prove x < SNoCut L2 R2.

An exact proof term for the current goal is H1 x Hx.

We will prove SNoCut L2 R2 < z.

An exact proof term for the current goal is Hz5.

We prove the intermediate claim LzR1: ∀y ∈ R1, z < y.

Let y be given.

Assume Hy: y ∈ R1.

Apply SNoLt_tra z (SNoCut L1 R1) y Hz1 H3 (HLR1b y Hy) to the current goal.

We will prove z < SNoCut L1 R1.

An exact proof term for the current goal is Hz6.

We will prove SNoCut L1 R1 < y.

An exact proof term for the current goal is H6 y Hy.

Apply H7 z Hz1 LzL1 LzR1 to the current goal.

Assume H14: SNoLev (SNoCut L1 R1) ⊆ SNoLev z.

Assume _.

Apply In_irref (SNoLev z) to the current goal.

Apply H14 to the current goal.

We will prove SNoLev z ∈ SNoLev (SNoCut L1 R1).

An exact proof term for the current goal is binintersectE2 (SNoLev (SNoCut L2 R2)) (SNoLev (SNoCut L1 R1)) (SNoLev z) Hz2.

Assume H14: SNoLev (SNoCut L2 R2) ∈ SNoLev (SNoCut L1 R1).

Assume H15: SNoEq_ (SNoLev (SNoCut L2 R2)) (SNoCut L2 R2) (SNoCut L1 R1).

Assume H16: SNoLev (SNoCut L2 R2) ∈ (SNoCut L1 R1).

Set z to be the term SNoCut L2 R2.

We prove the intermediate claim LzR1: ∀y ∈ R1, z < y.

Let y be given.

Assume Hy: y ∈ R1.

Apply SNoLt_tra z (SNoCut L1 R1) y H8 H3 (HLR1b y Hy) to the current goal.

We will prove z < SNoCut L1 R1.

An exact proof term for the current goal is H13.

We will prove SNoCut L1 R1 < y.

An exact proof term for the current goal is H6 y Hy.

Apply H7 z H8 H1 LzR1 to the current goal.

Assume H17: SNoLev (SNoCut L1 R1) ⊆ SNoLev z.

Assume _.

Apply In_irref (SNoLev z) to the current goal.

Apply H17 to the current goal.

We will prove SNoLev z ∈ SNoLev (SNoCut L1 R1).

An exact proof term for the current goal is H14.

Assume H14: SNoLev (SNoCut L1 R1) ∈ SNoLev (SNoCut L2 R2).

Assume H15: SNoEq_ (SNoLev (SNoCut L1 R1)) (SNoCut L2 R2) (SNoCut L1 R1).

Assume H16: SNoLev (SNoCut L1 R1) ∉ (SNoCut L2 R2).

Set z to be the term SNoCut L1 R1.

We prove the intermediate claim LzL2: ∀x ∈ L2, x < z.

Let x be given.

Assume Hx: x ∈ L2.

Apply SNoLt_tra x (SNoCut L2 R2) z (HLR2a x Hx) H8 H3 to the current goal.

We will prove x < SNoCut L2 R2.

An exact proof term for the current goal is H10 x Hx.

We will prove SNoCut L2 R2 < z.

An exact proof term for the current goal is H13.

Apply H12 z H3 LzL2 H2 to the current goal.

Assume H17: SNoLev (SNoCut L2 R2) ⊆ SNoLev z.

Assume _.

Apply In_irref (SNoLev z) to the current goal.

Apply H17 to the current goal.

We will prove SNoLev z ∈ SNoLev (SNoCut L2 R2).

An exact proof term for the current goal is H14.

Assume H13: SNoCut L1 R1 ≤ SNoCut L2 R2.

An exact proof term for the current goal is H13.

∎

Theorem. (SNoCut_ext)

∀L1 R1 L2 R2, SNoCutP L1 R1 → SNoCutP L2 R2 → (∀w ∈ L1, w < SNoCut L2 R2) → (∀z ∈ R1, SNoCut L2 R2 < z) → (∀w ∈ L2, w < SNoCut L1 R1) → (∀z ∈ R2, SNoCut L1 R1 < z) → SNoCut L1 R1 = SNoCut L2 R2

In Proofgold the corresponding term root is c1078e... and proposition id is f66618...

Proof:

Let L1, R1, L2 and R2 be given.

Assume HLR1 HLR2.

Assume H1: ∀w ∈ L1, w < SNoCut L2 R2.

Assume H2: ∀z ∈ R1, SNoCut L2 R2 < z.

Assume H3: ∀w ∈ L2, w < SNoCut L1 R1.

Assume H4: ∀z ∈ R2, SNoCut L1 R1 < z.

We prove the intermediate claim LNLR1: SNo (SNoCut L1 R1).

An exact proof term for the current goal is SNoCutP_SNo_SNoCut L1 R1 HLR1.

We prove the intermediate claim LNLR2: SNo (SNoCut L2 R2).

An exact proof term for the current goal is SNoCutP_SNo_SNoCut L2 R2 HLR2.

Apply SNoLe_antisym (SNoCut L1 R1) (SNoCut L2 R2) LNLR1 LNLR2 to the current goal.

We will prove SNoCut L1 R1 ≤ SNoCut L2 R2.

An exact proof term for the current goal is SNoCut_Le L1 R1 L2 R2 HLR1 HLR2 H1 H4.

We will prove SNoCut L2 R2 ≤ SNoCut L1 R1.

An exact proof term for the current goal is SNoCut_Le L2 R2 L1 R1 HLR2 HLR1 H3 H2.

∎

Theorem. (SNoLt_SNoL_or_SNoR_impred)

∀x y, SNo x → SNo y → x < y → ∀p : prop, (∀z ∈ SNoL y, z ∈ SNoR x → p) → (x ∈ SNoL y → p) → (y ∈ SNoR x → p) → p

In Proofgold the corresponding term root is f3b15a... and proposition id is ffc0bf...

Proof:

Let x and y be given.

Assume Hx Hy Hxy.

Let p be given.

Assume Hp1 Hp2 Hp3.

Apply SNoLtE x y Hx Hy Hxy to the current goal.

Let z be given.

Assume Hz1 Hz2 _ _ Hz3 Hz4 _ _.

Apply binintersectE (SNoLev x) (SNoLev y) (SNoLev z) Hz2 to the current goal.

Assume Hz2a Hz2b.

Apply Hp1 z to the current goal.

We will prove z ∈ SNoL y.

An exact proof term for the current goal is SNoL_I y Hy z Hz1 Hz2b Hz4.

We will prove z ∈ SNoR x.

An exact proof term for the current goal is SNoR_I x Hx z Hz1 Hz2a Hz3.

Assume H1 _ _.

Apply Hp2 to the current goal.

An exact proof term for the current goal is SNoL_I y Hy x Hx H1 Hxy.

Assume H1 _ _.

Apply Hp3 to the current goal.

An exact proof term for the current goal is SNoR_I x Hx y Hy H1 Hxy.

∎

Theorem. (SNoL_or_SNoR_impred)

∀x y, SNo x → SNo y → ∀p : prop, (x = y → p) → (∀z ∈ SNoL y, z ∈ SNoR x → p) → (x ∈ SNoL y → p) → (y ∈ SNoR x → p) → (∀z ∈ SNoR y, z ∈ SNoL x → p) → (x ∈ SNoR y → p) → (y ∈ SNoL x → p) → p

In Proofgold the corresponding term root is f8a5e2... and proposition id is 68ba98...

Proof:

Let x and y be given.

Assume Hx Hy.

Let p be given.

Assume Hp1 Hp2 Hp3 Hp4 Hp5 Hp6 Hp7.

Apply SNoLt_trichotomy_or_impred x y Hx Hy to the current goal.

Assume H1: x < y.

Apply SNoLt_SNoL_or_SNoR_impred x y Hx Hy H1 to the current goal.

An exact proof term for the current goal is Hp2.

An exact proof term for the current goal is Hp3.

An exact proof term for the current goal is Hp4.

Assume H1: x = y.

An exact proof term for the current goal is Hp1 H1.

Assume H1: y < x.

Apply SNoLt_SNoL_or_SNoR_impred y x Hy Hx H1 to the current goal.

Let z be given.

Assume H2 H3.

An exact proof term for the current goal is Hp5 z H3 H2.

An exact proof term for the current goal is Hp7.

An exact proof term for the current goal is Hp6.

∎

Theorem. (SNoL_SNoCutP_ex)

∀L R, SNoCutP L R → ∀w ∈ SNoL (SNoCut L R), ∃w' ∈ L, w ≤ w'

In Proofgold the corresponding term root is 3b4695... and proposition id is 6d8af6...

Proof:

Let L and R be given.

Assume HLR.

Set y to be the term SNoCut L R.

Let w be given.

Assume Hw: w ∈ SNoL y.

Apply dneg to the current goal.

Assume HC: ¬ ∃w' ∈ L, w ≤ w'.

Apply HLR to the current goal.

Assume H.

Apply H to the current goal.

Assume HL HR HLR'.

Apply SNoCutP_SNoCut_impred L R HLR to the current goal.

Assume H1: SNo y.

Assume H2: SNoLev y ∈ ordsucc ((⋃_{x ∈ L}ordsucc (SNoLev x)) ∪ (⋃_{y ∈ R}ordsucc (SNoLev y))).

Assume H3: ∀w ∈ L, w < y.

Assume H4: ∀z ∈ R, y < z.

Assume H5: ∀u, SNo u → (∀w ∈ L, w < u) → (∀z ∈ R, u < z) → SNoLev y ⊆ SNoLev u ∧ SNoEq_ (SNoLev y) y u.

Apply SNoL_E y H1 w Hw to the current goal.

Assume Hw1 Hw2 Hw3.

We prove the intermediate claim L1: SNoLev y ⊆ SNoLev w ∧ SNoEq_ (SNoLev y) y w.

Apply H5 w Hw1 to the current goal.

Let w' be given.

Assume Hw': w' ∈ L.

We will prove w' < w.

Apply SNoLtLe_or w' w (HL w' Hw') Hw1 to the current goal.

Assume H6.

An exact proof term for the current goal is H6.

Assume H6: w ≤ w'.

Apply HC to the current goal.

We use w' to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hw'.

An exact proof term for the current goal is H6.

Let z be given.

Assume Hz: z ∈ R.

We will prove w < z.

Apply SNoLt_tra w y z Hw1 H1 (HR z Hz) Hw3 to the current goal.

We will prove y < z.

An exact proof term for the current goal is H4 z Hz.

Apply In_irref (SNoLev w) to the current goal.

We will prove SNoLev w ∈ SNoLev w.

Apply andEL (SNoLev y ⊆ SNoLev w) (SNoEq_ (SNoLev y) y w) L1 to the current goal.

We will prove SNoLev w ∈ SNoLev y.

An exact proof term for the current goal is Hw2.

∎

Theorem. (SNoR_SNoCutP_ex)

∀L R, SNoCutP L R → ∀z ∈ SNoR (SNoCut L R), ∃z' ∈ R, z' ≤ z

In Proofgold the corresponding term root is ca7be2... and proposition id is bb0b53...

Proof:

Let L and R be given.

Assume HLR.

Set y to be the term SNoCut L R.

Let z be given.

Assume Hz: z ∈ SNoR y.

Apply dneg to the current goal.

Assume HC: ¬ ∃z' ∈ R, z' ≤ z.

Apply HLR to the current goal.

Assume H.

Apply H to the current goal.

Assume HL HR HLR'.

Apply SNoCutP_SNoCut_impred L R HLR to the current goal.

Assume H1: SNo y.

Assume H2: SNoLev y ∈ ordsucc ((⋃_{x ∈ L}ordsucc (SNoLev x)) ∪ (⋃_{y ∈ R}ordsucc (SNoLev y))).

Assume H3: ∀w ∈ L, w < y.

Assume H4: ∀z ∈ R, y < z.

Assume H5: ∀u, SNo u → (∀w ∈ L, w < u) → (∀z ∈ R, u < z) → SNoLev y ⊆ SNoLev u ∧ SNoEq_ (SNoLev y) y u.

Apply SNoR_E y H1 z Hz to the current goal.

Assume Hz1 Hz2 Hz3.

We prove the intermediate claim L1: SNoLev y ⊆ SNoLev z ∧ SNoEq_ (SNoLev y) y z.

Apply H5 z Hz1 to the current goal.

Let w be given.

Assume Hw: w ∈ L.

We will prove w < z.

Apply SNoLt_tra w y z (HL w Hw) H1 Hz1 to the current goal.

We will prove w < y.

An exact proof term for the current goal is H3 w Hw.

We will prove y < z.

An exact proof term for the current goal is Hz3.

Let z' be given.

Assume Hz': z' ∈ R.

We will prove z < z'.

Apply SNoLtLe_or z z' Hz1 (HR z' Hz') to the current goal.

Assume H6.

An exact proof term for the current goal is H6.

Assume H6: z' ≤ z.

Apply HC to the current goal.

We use z' to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hz'.

An exact proof term for the current goal is H6.

Apply In_irref (SNoLev z) to the current goal.

We will prove SNoLev z ∈ SNoLev z.

Apply andEL (SNoLev y ⊆ SNoLev z) (SNoEq_ (SNoLev y) y z) L1 to the current goal.

We will prove SNoLev z ∈ SNoLev y.

An exact proof term for the current goal is Hz2.

∎

Theorem. (ordinal_SNo_)

∀alpha, ordinal alpha → SNo_ alpha alpha

In Proofgold the corresponding term root is 4731fd... and proposition id is 7754e5...

Proof:

Let alpha be given.

Assume Ha: ordinal alpha.

We will prove alpha ⊆ SNoElts_ alpha ∧ ∀beta ∈ alpha, exactly1of2 (beta ' ∈ alpha) (beta ∈ alpha).

Apply andI to the current goal.

We will prove alpha ⊆ SNoElts_ alpha.

Let beta be given.

Assume Hb: beta ∈ alpha.

We will prove beta ∈ alpha ∪ {beta '|beta ∈ alpha}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is Hb.

We will prove ∀beta ∈ alpha, exactly1of2 (beta ' ∈ alpha) (beta ∈ alpha).

Let beta be given.

Assume Hb: beta ∈ alpha.

Apply exactly1of2_I2 to the current goal.

We will prove beta ' ∉ alpha.

Assume H1: beta ' ∈ alpha.

We will prove False.

Apply tagged_not_ordinal beta to the current goal.

We will prove ordinal (beta ').

An exact proof term for the current goal is ordinal_Hered alpha Ha (beta ') H1.

We will prove beta ∈ alpha.

An exact proof term for the current goal is Hb.

∎

Theorem. (ordinal_SNo)

∀alpha, ordinal alpha → SNo alpha

In Proofgold the corresponding term root is ac39bc... and proposition id is 1eea33...

Proof:

Let alpha be given.

Assume Ha: ordinal alpha.

We will prove ∃beta, ordinal beta ∧ SNo_ beta alpha.

We use alpha to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Ha.

An exact proof term for the current goal is ordinal_SNo_ alpha Ha.

∎

Theorem. (ordinal_SNoLev)

∀alpha, ordinal alpha → SNoLev alpha = alpha

In Proofgold the corresponding term root is 56f8b0... and proposition id is fea5fc...

Proof:

Let alpha be given.

Assume Ha: ordinal alpha.

Apply SNoLev_prop alpha (ordinal_SNo alpha Ha) to the current goal.

Assume H1: ordinal (SNoLev alpha).

Assume H2: SNo_ (SNoLev alpha) alpha.

An exact proof term for the current goal is SNoLev_uniq alpha (SNoLev alpha) alpha H1 Ha H2 (ordinal_SNo_ alpha Ha).

∎

Theorem. (ordinal_SNoLev_max)

∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ alpha → z < alpha

In Proofgold the corresponding term root is 945794... and proposition id is 51ee47...

Proof:

Let alpha be given.

Assume Ha: ordinal alpha.

Let z be given.

Assume Hz: SNo z.

Assume Hz2: SNoLev z ∈ alpha.

We prove the intermediate claim La1: SNo alpha.

An exact proof term for the current goal is ordinal_SNo alpha Ha.

We prove the intermediate claim La2: SNoLev alpha = alpha.

An exact proof term for the current goal is ordinal_SNoLev alpha Ha.

We will prove z < alpha.

Apply SNoLt_trichotomy_or z alpha Hz (ordinal_SNo alpha Ha) to the current goal.

Assume H1.

Apply H1 to the current goal.

Assume H1: z < alpha.

An exact proof term for the current goal is H1.

Assume H1: z = alpha.

We will prove False.

Apply In_irref alpha to the current goal.

rewrite the current goal using La2 (from right to left) at position 1.

We will prove SNoLev alpha ∈ alpha.

rewrite the current goal using H1 (from right to left) at position 1.

We will prove SNoLev z ∈ alpha.

An exact proof term for the current goal is Hz2.

Assume H1: alpha < z.

We will prove False.

Apply SNoLtE alpha z La1 Hz H1 to the current goal.

Let w be given.

rewrite the current goal using La2 (from left to right).

Assume Hw: SNo w.

Assume H2: SNoLev w ∈ alpha ∩ SNoLev z.

Assume H3: SNoEq_ (SNoLev w) w alpha.

Assume H4: SNoEq_ (SNoLev w) w z.

Assume H5: alpha < w.

Assume H6: w < z.

Assume H7: SNoLev w ∉ alpha.

We will prove False.

Apply H7 to the current goal.

An exact proof term for the current goal is binintersectE1 alpha (SNoLev z) (SNoLev w) H2.

rewrite the current goal using La2 (from left to right).

Assume H2: alpha ∈ SNoLev z.

We will prove False.

An exact proof term for the current goal is In_no2cycle alpha (SNoLev z) H2 Hz2.

rewrite the current goal using La2 (from left to right).

Assume H2: SNoLev z ∈ alpha.

Assume H3: SNoEq_ (SNoLev z) alpha z.

Assume H4: SNoLev z ∉ alpha.

An exact proof term for the current goal is H4 H2.

∎

Theorem. (ordinal_SNoL)

∀alpha, ordinal alpha → SNoL alpha = SNoS_ alpha

In Proofgold the corresponding term root is fef608... and proposition id is 95823e...

Proof:

Let alpha be given.

Assume Ha: ordinal alpha.

We prove the intermediate claim La1: SNo alpha.

An exact proof term for the current goal is ordinal_SNo alpha Ha.

We prove the intermediate claim La2: SNoLev alpha = alpha.

An exact proof term for the current goal is ordinal_SNoLev alpha Ha.

Apply set_ext to the current goal.

Let x be given.

Assume Hx: x ∈ SNoL alpha.

Apply SNoL_E alpha La1 x Hx to the current goal.

Assume Hx1: SNo x.

Assume Hx2: SNoLev x ∈ SNoLev alpha.

Assume Hx3: x < alpha.

We will prove x ∈ SNoS_ alpha.

rewrite the current goal using La2 (from right to left).

We will prove x ∈ SNoS_ (SNoLev alpha).

Apply SNoS_I2 x alpha Hx1 La1 to the current goal.

We will prove SNoLev x ∈ SNoLev alpha.

An exact proof term for the current goal is Hx2.

Let x be given.

Assume Hx: x ∈ SNoS_ alpha.

Apply SNoS_E2 alpha Ha x Hx to the current goal.

Assume Hx1: SNoLev x ∈ alpha.

Assume Hx2: ordinal (SNoLev x).

Assume Hx3: SNo x.

Assume Hx4: SNo_ (SNoLev x) x.

We will prove x ∈ SNoL alpha.

Apply SNoL_I alpha La1 x Hx3 to the current goal.

We will prove SNoLev x ∈ SNoLev alpha.

rewrite the current goal using La2 (from left to right).

An exact proof term for the current goal is Hx1.

We will prove x < alpha.

An exact proof term for the current goal is ordinal_SNoLev_max alpha Ha x Hx3 Hx1.

∎

Theorem. (ordinal_SNoR)

∀alpha, ordinal alpha → SNoR alpha = Empty

In Proofgold the corresponding term root is 07c69a... and proposition id is f853d9...

Proof:

Let alpha be given.

Assume Ha: ordinal alpha.

We prove the intermediate claim La1: SNo alpha.

An exact proof term for the current goal is ordinal_SNo alpha Ha.

We prove the intermediate claim La2: SNoLev alpha = alpha.

An exact proof term for the current goal is ordinal_SNoLev alpha Ha.

Apply Empty_Subq_eq to the current goal.

Let x be given.

Assume Hx: x ∈ SNoR alpha.

Apply SNoR_E alpha La1 x Hx to the current goal.

Assume Hx1: SNo x.

rewrite the current goal using La2 (from left to right).

Assume Hx2: SNoLev x ∈ alpha.

Assume Hx3: alpha < x.

We will prove False.

Apply SNoLt_irref x to the current goal.

Apply SNoLt_tra x alpha x Hx1 La1 Hx1 to the current goal.

We will prove x < alpha.

An exact proof term for the current goal is ordinal_SNoLev_max alpha Ha x Hx1 Hx2.

We will prove alpha < x.

An exact proof term for the current goal is Hx3.

∎

Theorem. (nat_p_SNo)

∀n, nat_p n → SNo n

In Proofgold the corresponding term root is 0644f3... and proposition id is 5fd930...

Proof:

Let n be given.

Assume Hn.

Apply ordinal_SNo to the current goal.

We will prove ordinal n.

Apply nat_p_ordinal to the current goal.

An exact proof term for the current goal is Hn.

∎

Theorem. (omega_SNo)

∀n ∈ ω, SNo n

In Proofgold the corresponding term root is d32269... and proposition id is d0f9c6...

Proof:

Let n be given.

Assume Hn.

Apply nat_p_SNo to the current goal.

Apply omega_nat_p to the current goal.

An exact proof term for the current goal is Hn.

∎

Theorem. (omega_SNoS_omega)

ω ⊆ SNoS_ ω

In Proofgold the corresponding term root is 4ba265... and proposition id is 2ccf7a...

Proof:

Let n be given.

Assume Hn: n ∈ ω.

Apply SNoS_I ω omega_ordinal n n to the current goal.

An exact proof term for the current goal is Hn.

We will prove SNo_ n n.

rewrite the current goal using ordinal_SNoLev n (nat_p_ordinal n (omega_nat_p n Hn)) (from right to left) at position 1.

We will prove SNo_ (SNoLev n) n.

Apply SNoLev_ to the current goal.

Apply omega_SNo to the current goal.

An exact proof term for the current goal is Hn.

∎

Theorem. (ordinal_In_SNoLt)

∀alpha, ordinal alpha → ∀beta ∈ alpha, beta < alpha

In Proofgold the corresponding term root is e37d00... and proposition id is ced78e...

Proof:

Let alpha be given.

Assume Ha: ordinal alpha.

Let beta be given.

Assume Hb: beta ∈ alpha.

We prove the intermediate claim Lb: ordinal beta.

An exact proof term for the current goal is ordinal_Hered alpha Ha beta Hb.

We prove the intermediate claim Lb1: SNo beta.

An exact proof term for the current goal is ordinal_SNo beta Lb.

We prove the intermediate claim Lb2: SNoLev beta = beta.

An exact proof term for the current goal is ordinal_SNoLev beta Lb.

Apply ordinal_SNoLev_max alpha Ha beta Lb1 to the current goal.

We will prove SNoLev beta ∈ alpha.

rewrite the current goal using Lb2 (from left to right).

An exact proof term for the current goal is Hb.

∎

Theorem. (ordinal_SNoLev_max_2)

∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ ordsucc alpha → z ≤ alpha

In Proofgold the corresponding term root is 72c5eb... and proposition id is c9a731...

Proof:

Let alpha be given.

Assume Ha: ordinal alpha.

Apply Ha to the current goal.

Assume Ha1 _.

Let z be given.

Assume Hz: SNo z.

Assume Hz2: SNoLev z ∈ ordsucc alpha.

We prove the intermediate claim La1: SNo alpha.

An exact proof term for the current goal is ordinal_SNo alpha Ha.

We prove the intermediate claim La2: SNoLev alpha = alpha.

An exact proof term for the current goal is ordinal_SNoLev alpha Ha.

Apply ordsuccE alpha (SNoLev z) Hz2 to the current goal.

Assume Hz3: SNoLev z ∈ alpha.

We will prove z ≤ alpha.

Apply SNoLtLe to the current goal.

We will prove z < alpha.

An exact proof term for the current goal is ordinal_SNoLev_max alpha Ha z Hz Hz3.

Assume Hz3: SNoLev z = alpha.

Apply dneg to the current goal.

Assume H1: ¬ (z ≤ alpha).

We prove the intermediate claim L1: ∀beta, ordinal beta → beta ∈ alpha → beta ∈ z.

Apply ordinal_ind to the current goal.

Let beta be given.

Assume Hb: ordinal beta.

Assume IH: ∀gamma ∈ beta, gamma ∈ alpha → gamma ∈ z.

Assume Hb2: beta ∈ alpha.

Apply dneg to the current goal.

Assume H2: beta ∉ z.

Apply H1 to the current goal.

Apply SNoLtLe to the current goal.

We will prove z < alpha.

We prove the intermediate claim Lb1: SNo beta.

An exact proof term for the current goal is ordinal_SNo beta Hb.

We prove the intermediate claim Lb2: SNoLev beta = beta.

An exact proof term for the current goal is ordinal_SNoLev beta Hb.

Apply SNoLt_tra z beta alpha Hz Lb1 La1 to the current goal.

We will prove z < beta.

Apply SNoLtI3 to the current goal.

We will prove SNoLev beta ∈ SNoLev z.

rewrite the current goal using Lb2 (from left to right).

rewrite the current goal using Hz3 (from left to right).

We will prove beta ∈ alpha.

An exact proof term for the current goal is Hb2.

We will prove SNoEq_ (SNoLev beta) z beta.

rewrite the current goal using Lb2 (from left to right).

Let gamma be given.

Assume Hc: gamma ∈ beta.

We will prove gamma ∈ z ↔ gamma ∈ beta.

Apply iffI to the current goal.

Assume _.

An exact proof term for the current goal is Hc.

Assume _.

We will prove gamma ∈ z.

Apply IH gamma Hc to the current goal.

We will prove gamma ∈ alpha.

An exact proof term for the current goal is Ha1 beta Hb2 gamma Hc.

We will prove SNoLev beta ∉ z.

rewrite the current goal using Lb2 (from left to right).

We will prove beta ∉ z.

An exact proof term for the current goal is H2.

We will prove beta < alpha.

An exact proof term for the current goal is ordinal_In_SNoLt alpha Ha beta Hb2.

We prove the intermediate claim L2: alpha ⊆ z.

Let beta be given.

Assume Hb: beta ∈ alpha.

An exact proof term for the current goal is L1 beta (ordinal_Hered alpha Ha beta Hb) Hb.

We prove the intermediate claim L3: z = alpha.

Apply SNo_eq z alpha Hz La1 to the current goal.

We will prove SNoLev z = SNoLev alpha.

rewrite the current goal using La2 (from left to right).

An exact proof term for the current goal is Hz3.

We will prove SNoEq_ (SNoLev z) z alpha.

rewrite the current goal using Hz3 (from left to right).

Let beta be given.

Assume Hb: beta ∈ alpha.

We will prove beta ∈ z ↔ beta ∈ alpha.

Apply iffI to the current goal.

Assume _.

An exact proof term for the current goal is Hb.

Assume _.

An exact proof term for the current goal is L2 beta Hb.

Apply H1 to the current goal.

We will prove z ≤ alpha.

rewrite the current goal using L3 (from left to right).

We will prove alpha ≤ alpha.

Apply SNoLe_ref to the current goal.

∎

Theorem. (ordinal_Subq_SNoLe)

∀alpha beta, ordinal alpha → ordinal beta → alpha ⊆ beta → alpha ≤ beta

In Proofgold the corresponding term root is 7558ba... and proposition id is 15c58a...

Proof:

Let alpha and beta be given.

Assume Ha Hb Hab.

We prove the intermediate claim L1: alpha ∈ ordsucc beta.

Apply ordinal_In_Or_Subq alpha beta Ha Hb to the current goal.

Assume H1: alpha ∈ beta.

Apply ordsuccI1 to the current goal.

An exact proof term for the current goal is H1.

Assume H1: beta ⊆ alpha.

We prove the intermediate claim L1a: alpha = beta.

Apply set_ext to the current goal.

An exact proof term for the current goal is Hab.

An exact proof term for the current goal is H1.

rewrite the current goal using L1a (from left to right).

Apply ordsuccI2 to the current goal.

We prove the intermediate claim La1: SNo alpha.

An exact proof term for the current goal is ordinal_SNo alpha Ha.

We prove the intermediate claim La2: SNoLev alpha = alpha.

An exact proof term for the current goal is ordinal_SNoLev alpha Ha.

Apply ordinal_SNoLev_max_2 beta Hb alpha La1 to the current goal.

We will prove SNoLev alpha ∈ ordsucc beta.

rewrite the current goal using La2 (from left to right).

An exact proof term for the current goal is L1.

∎

Theorem. (ordinal_SNoLt_In)

∀alpha beta, ordinal alpha → ordinal beta → alpha < beta → alpha ∈ beta

In Proofgold the corresponding term root is d6f066... and proposition id is de775b...

Proof:

Let alpha and beta be given.

Assume Ha Hb.

Assume H1.

Apply ordinal_In_Or_Subq alpha beta Ha Hb to the current goal.

Assume H2.

An exact proof term for the current goal is H2.

Assume H2: beta ⊆ alpha.

We will prove False.

Apply SNoLt_irref alpha to the current goal.

We will prove alpha < alpha.

Apply SNoLtLe_tra alpha beta alpha (ordinal_SNo alpha Ha) (ordinal_SNo beta Hb) (ordinal_SNo alpha Ha) H1 to the current goal.

We will prove beta ≤ alpha.

An exact proof term for the current goal is ordinal_Subq_SNoLe beta alpha Hb Ha H2.

∎

Theorem. (omega_nonneg)

∀m ∈ ω, 0 ≤ m

In Proofgold the corresponding term root is ee67c9... and proposition id is eaf06b...

Proof:

Let m be given.

Assume Hm.

Apply ordinal_Subq_SNoLe 0 m ordinal_Empty (nat_p_ordinal m (omega_nat_p m Hm)) to the current goal.

We will prove 0 ⊆ m.

Apply Subq_Empty to the current goal.

∎

Theorem. (SNo_0)

SNo 0

In Proofgold the corresponding term root is c8204b... and proposition id is 94a310...

Proof:

An exact proof term for the current goal is ordinal_SNo 0 ordinal_Empty.

∎

Theorem. (SNo_1)

SNo 1

In Proofgold the corresponding term root is ac50d7... and proposition id is 9a733a...

Proof:

Apply ordinal_SNo to the current goal.

Apply nat_p_ordinal to the current goal.

An exact proof term for the current goal is nat_1.

∎

Theorem. (SNo_2)

SNo 2

In Proofgold the corresponding term root is 487591... and proposition id is c524a4...

Proof:

Apply ordinal_SNo to the current goal.

Apply nat_p_ordinal to the current goal.

An exact proof term for the current goal is nat_2.

∎

Theorem. (SNoLev_0)

SNoLev 0 = 0

In Proofgold the corresponding term root is 45a0f7... and proposition id is 3527a4...

Proof:

An exact proof term for the current goal is ordinal_SNoLev 0 ordinal_Empty.

∎

Theorem. (SNoCut_0_0)

SNoCut 0 0 = 0

In Proofgold the corresponding term root is 6a1f81... and proposition id is abbffb...

Proof:

Apply SNoCutP_SNoCut_impred 0 0 SNoCutP_0_0 to the current goal.

Assume H1: SNo (SNoCut 0 0).

rewrite the current goal using famunion_Empty (λx ⇒ ordsucc (SNoLev x)) (from left to right).

rewrite the current goal using binunion_idl 0 (from left to right).

Assume H2: SNoLev (SNoCut 0 0) ∈ 1.

Assume _ _ _.

We prove the intermediate claim L1: SNoLev (SNoCut 0 0) = 0.

Apply cases_1 (SNoLev (SNoCut 0 0)) H2 (λu ⇒ u = 0) to the current goal.

We will prove 0 = 0.

Use reflexivity.

Apply SNo_eq (SNoCut 0 0) 0 H1 SNo_0 to the current goal.

We will prove SNoLev (SNoCut 0 0) = SNoLev 0.

Use transitivity with and 0.

An exact proof term for the current goal is L1.

Use symmetry.

An exact proof term for the current goal is SNoLev_0.

We will prove SNoEq_ (SNoLev (SNoCut 0 0)) (SNoCut 0 0) 0.

rewrite the current goal using L1 (from left to right).

We will prove SNoEq_ 0 (SNoCut 0 0) 0.

Apply SNoEq_I to the current goal.

Let beta be given.

Assume Hb: beta ∈ 0.

We will prove False.

An exact proof term for the current goal is EmptyE beta Hb.

∎

Theorem. (SNoL_0)

SNoL 0 = 0

In Proofgold the corresponding term root is c01c2b... and proposition id is fdaa69...

Proof:

Apply Empty_Subq_eq to the current goal.

We will prove SNoL 0 ⊆ Empty.

Let z be given.

Assume Hz: z ∈ SNoL 0.

We prove the intermediate claim Lz: z ∈ SNoS_ 0.

rewrite the current goal using SNoLev_0 (from right to left).

We will prove z ∈ SNoS_ (SNoLev 0).

An exact proof term for the current goal is SNoL_SNoS_ 0 z Hz.

Apply SNoS_E2 0 ordinal_Empty z Lz to the current goal.

Assume Hz1: SNoLev z ∈ 0.

We will prove False.

An exact proof term for the current goal is EmptyE (SNoLev z) Hz1.

∎

Theorem. (SNoR_0)

SNoR 0 = 0

In Proofgold the corresponding term root is 7329c7... and proposition id is 510751...

Proof:

Apply Empty_Subq_eq to the current goal.

We will prove SNoR 0 ⊆ Empty.

Let z be given.

Assume Hz: z ∈ SNoR 0.

We prove the intermediate claim Lz: z ∈ SNoS_ 0.

rewrite the current goal using SNoLev_0 (from right to left).

We will prove z ∈ SNoS_ (SNoLev 0).

An exact proof term for the current goal is SNoR_SNoS_ 0 z Hz.

Apply SNoS_E2 0 ordinal_Empty z Lz to the current goal.

Assume Hz1: SNoLev z ∈ 0.

We will prove False.

An exact proof term for the current goal is EmptyE (SNoLev z) Hz1.

∎

Theorem. (SNoL_1)

SNoL 1 = 1

In Proofgold the corresponding term root is 84d688... and proposition id is 15aa79...

Proof:

Apply set_ext to the current goal.

Let x be given.

Assume Hx: x ∈ SNoL 1.

We will prove x ∈ 1.

Apply SNoL_E 1 SNo_1 x Hx to the current goal.

Assume Hxa: SNo x.

rewrite the current goal using ordinal_SNoLev 1 (nat_p_ordinal 1 nat_1) (from left to right).

Assume Hxb: SNoLev x ∈ 1.

Assume _.

We prove the intermediate claim L1: 0 = x.

Apply SNo_eq 0 x SNo_0 Hxa to the current goal.

We will prove SNoLev 0 = SNoLev x.

rewrite the current goal using SNoLev_0 (from left to right).

We will prove 0 = SNoLev x.

Apply cases_1 (SNoLev x) Hxb (λu ⇒ 0 = u) to the current goal.

We will prove 0 = 0.

Use reflexivity.

We will prove SNoEq_ (SNoLev 0) 0 x.

rewrite the current goal using SNoLev_0 (from left to right).

We will prove SNoEq_ 0 0 x.

Apply SNoEq_I to the current goal.

Let beta be given.

Assume Hb: beta ∈ 0.

We will prove False.

An exact proof term for the current goal is EmptyE beta Hb.

rewrite the current goal using L1 (from right to left).

An exact proof term for the current goal is In_0_1.

Let x be given.

Assume Hx: x ∈ 1.

We will prove x ∈ SNoL 1.

Apply cases_1 x Hx (λx ⇒ x ∈ SNoL 1) to the current goal.

We will prove 0 ∈ SNoL 1.

Apply SNoL_I 1 SNo_1 0 SNo_0 to the current goal.

We will prove SNoLev 0 ∈ SNoLev 1.

rewrite the current goal using SNoLev_0 (from left to right).

rewrite the current goal using ordinal_SNoLev 1 (nat_p_ordinal 1 nat_1) (from left to right).

An exact proof term for the current goal is In_0_1.

We will prove 0 < 1.

An exact proof term for the current goal is ordinal_In_SNoLt 1 (nat_p_ordinal 1 nat_1) 0 In_0_1.

∎

Theorem. (SNoR_1)

SNoR 1 = 0

In Proofgold the corresponding term root is e6a83a... and proposition id is 8da427...

Proof:

An exact proof term for the current goal is ordinal_SNoR 1 (nat_p_ordinal 1 nat_1).

∎

Theorem. (SNo_max_SNoLev)

∀x, SNo x → (∀y ∈ SNoS_ (SNoLev x), y < x) → SNoLev x = x

In Proofgold the corresponding term root is ff019e... and proposition id is 3be246...

Proof:

Let x be given.

Assume Hx: SNo x.

Assume H2: ∀y ∈ SNoS_ (SNoLev x), y < x.

We prove the intermediate claim LLx1: ordinal (SNoLev x).

An exact proof term for the current goal is SNoLev_ordinal x Hx.

We prove the intermediate claim LLx2: SNo (SNoLev x).

An exact proof term for the current goal is ordinal_SNo (SNoLev x) LLx1.

We prove the intermediate claim L3: x ≤ SNoLev x.

Apply ordinal_SNoLev_max_2 (SNoLev x) LLx1 x Hx to the current goal.

We will prove SNoLev x ∈ ordsucc (SNoLev x).

Apply ordsuccI2 to the current goal.

Apply SNoLeE x (SNoLev x) Hx LLx2 L3 to the current goal.

Assume H3: x < SNoLev x.

We will prove False.

Apply SNoLtE x (SNoLev x) Hx LLx2 H3 to the current goal.

Let z be given.

Assume Hz: SNo z.

Assume Hz1: SNoLev z ∈ SNoLev x ∩ SNoLev (SNoLev x).

Assume Hz2: SNoEq_ (SNoLev z) z x.

Assume Hz3: SNoEq_ (SNoLev z) z (SNoLev x).

Assume Hz4: x < z.

Assume Hz5: z < SNoLev x.

Assume Hz6: SNoLev z ∉ x.

Assume Hz7: SNoLev z ∈ SNoLev x.

Apply SNoLt_irref z to the current goal.

Apply SNoLt_tra z x z Hz Hx Hz to the current goal.

We will prove z < x.

Apply H2 to the current goal.

We will prove z ∈ SNoS_ (SNoLev x).

Apply SNoS_I (SNoLev x) LLx1 z (SNoLev z) to the current goal.

We will prove SNoLev z ∈ SNoLev x.

An exact proof term for the current goal is Hz7.

We will prove SNo_ (SNoLev z) z.

Apply SNoLev_ to the current goal.

An exact proof term for the current goal is Hz.

We will prove x < z.

An exact proof term for the current goal is Hz4.

Assume H4: SNoLev x ∈ SNoLev (SNoLev x).

We will prove False.

Apply In_irref (SNoLev x) to the current goal.

rewrite the current goal using ordinal_SNoLev (SNoLev x) LLx1 (from right to left) at position 2.

An exact proof term for the current goal is H4.

Assume H4: SNoLev (SNoLev x) ∈ SNoLev x.

We will prove False.

Apply In_irref (SNoLev x) to the current goal.

rewrite the current goal using ordinal_SNoLev (SNoLev x) LLx1 (from right to left) at position 1.

An exact proof term for the current goal is H4.

Assume H3: x = SNoLev x.

Use symmetry.

An exact proof term for the current goal is H3.

∎

Theorem. (SNo_max_ordinal)

∀x, SNo x → (∀y ∈ SNoS_ (SNoLev x), y < x) → ordinal x

In Proofgold the corresponding term root is 0b230c... and proposition id is f28b9a...

Proof:

Let x be given.

Assume Hx: SNo x.

Assume H2: ∀y ∈ SNoS_ (SNoLev x), y < x.

We will prove ordinal x.

rewrite the current goal using SNo_max_SNoLev x Hx H2 (from right to left).

We will prove ordinal (SNoLev x).

An exact proof term for the current goal is SNoLev_ordinal x Hx.

∎

Theorem. (pos_low_eq_one)

∀x, SNo x → 0 < x → SNoLev x ⊆ 1 → x = 1

In Proofgold the corresponding term root is 7c84ef... and proposition id is db40ad...

Proof:

Let x be given.

Assume Hx Hxpos Hxlow.

Apply SNoLtE 0 x SNo_0 Hx Hxpos to the current goal.

Let y be given.

Assume Hy1: SNo y.

Assume Hy2: SNoLev y ∈ SNoLev 0 ∩ SNoLev x.

We will prove False.

Apply EmptyE (SNoLev y) to the current goal.

We will prove SNoLev y ∈ 0.

rewrite the current goal using ordinal_SNoLev 0 ordinal_Empty (from right to left).

We will prove SNoLev y ∈ SNoLev 0.

An exact proof term for the current goal is binintersectE1 (SNoLev 0) (SNoLev x) (SNoLev y) Hy2.

rewrite the current goal using ordinal_SNoLev 0 ordinal_Empty (from left to right).

Assume H1: 0 ∈ SNoLev x.

Assume _.

Assume H2: 0 ∈ x.

We prove the intermediate claim L1: SNoLev x = 1.

Apply set_ext to the current goal.

An exact proof term for the current goal is Hxlow.

Let n be given.

Assume Hn: n ∈ 1.

Apply cases_1 n Hn to the current goal.

We will prove 0 ∈ SNoLev x.

An exact proof term for the current goal is H1.

Apply SNo_eq x 1 Hx SNo_1 to the current goal.

We will prove SNoLev x = SNoLev 1.

rewrite the current goal using ordinal_SNoLev 1 (nat_p_ordinal 1 nat_1) (from left to right).

We will prove SNoLev x = 1.

An exact proof term for the current goal is L1.

We will prove SNoEq_ (SNoLev x) x 1.

rewrite the current goal using L1 (from left to right).

We will prove SNoEq_ 1 x 1.

Let n be given.

Assume Hn: n ∈ 1.

We will prove n ∈ x ↔ n ∈ 1.

Apply cases_1 n Hn (λn ⇒ n ∈ x ↔ n ∈ 1) to the current goal.

We will prove 0 ∈ x ↔ 0 ∈ 1.

Apply iffI to the current goal.

Assume _.

An exact proof term for the current goal is In_0_1.

Assume _.

An exact proof term for the current goal is H2.

Assume H1: SNoLev x ∈ SNoLev 0.

We will prove False.

Apply EmptyE (SNoLev x) to the current goal.

We will prove SNoLev x ∈ 0.

rewrite the current goal using ordinal_SNoLev 0 ordinal_Empty (from right to left).

We will prove SNoLev x ∈ SNoLev 0.

An exact proof term for the current goal is H1.

∎

Definition. We define SNo_extend0 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λdelta ⇒ delta ∈ x ∧ delta ≠ SNoLev x) of type set → set.

In Proofgold the corresponding term root is 997d91... and object id is ff4161...

Definition. We define SNo_extend1 to be λx ⇒ PSNo (ordsucc (SNoLev x)) (λdelta ⇒ delta ∈ x ∨ delta = SNoLev x) of type set → set.

In Proofgold the corresponding term root is 464e47... and object id is 8c551b...

Theorem. (SNo_extend0_SNo_)

∀x, SNo x → SNo_ (ordsucc (SNoLev x)) (SNo_extend0 x)

In Proofgold the corresponding term root is d41d3e... and proposition id is c8f8ea...

Proof:

Let x be given.

Assume Hx: SNo x.

Set alpha to be the term SNoLev x.

We prove the intermediate claim La: ordinal alpha.

An exact proof term for the current goal is SNoLev_ordinal x Hx.

An exact proof term for the current goal is SNo_PSNo (ordsucc alpha) (ordinal_ordsucc alpha La) (λdelta ⇒ delta ∈ x ∧ delta ≠ alpha).

∎

Theorem. (SNo_extend1_SNo_)

∀x, SNo x → SNo_ (ordsucc (SNoLev x)) (SNo_extend1 x)

In Proofgold the corresponding term root is b7b866... and proposition id is 73bbf2...

Proof:

Let x be given.

Assume Hx: SNo x.

Set alpha to be the term SNoLev x.

We prove the intermediate claim La: ordinal alpha.

An exact proof term for the current goal is SNoLev_ordinal x Hx.

An exact proof term for the current goal is SNo_PSNo (ordsucc alpha) (ordinal_ordsucc alpha La) (λdelta ⇒ delta ∈ x ∨ delta = alpha).

∎

Theorem. (SNo_extend0_SNo)

∀x, SNo x → SNo (SNo_extend0 x)

In Proofgold the corresponding term root is b353a2... and proposition id is 76562c...

Proof:

Let x be given.

Assume Hx.

An exact proof term for the current goal is SNo_SNo (ordsucc (SNoLev x)) (ordinal_ordsucc (SNoLev x) (SNoLev_ordinal x Hx)) (SNo_extend0 x) (SNo_extend0_SNo_ x Hx).

∎

Theorem. (SNo_extend1_SNo)

∀x, SNo x → SNo (SNo_extend1 x)

In Proofgold the corresponding term root is fa323a... and proposition id is 5345a7...

Proof:

Let x be given.

Assume Hx.

An exact proof term for the current goal is SNo_SNo (ordsucc (SNoLev x)) (ordinal_ordsucc (SNoLev x) (SNoLev_ordinal x Hx)) (SNo_extend1 x) (SNo_extend1_SNo_ x Hx).

∎

Theorem. (SNo_extend0_SNoLev)

∀x, SNo x → SNoLev (SNo_extend0 x) = ordsucc (SNoLev x)

In Proofgold the corresponding term root is 26efcd... and proposition id is 5aa0af...

Proof:

Let x be given.

Assume Hx.

An exact proof term for the current goal is SNoLev_uniq2 (ordsucc (SNoLev x)) (ordinal_ordsucc (SNoLev x) (SNoLev_ordinal x Hx)) (SNo_extend0 x) (SNo_extend0_SNo_ x Hx).

∎

Theorem. (SNo_extend1_SNoLev)

∀x, SNo x → SNoLev (SNo_extend1 x) = ordsucc (SNoLev x)

In Proofgold the corresponding term root is 33cf60... and proposition id is 529347...

Proof:

Let x be given.

Assume Hx.

An exact proof term for the current goal is SNoLev_uniq2 (ordsucc (SNoLev x)) (ordinal_ordsucc (SNoLev x) (SNoLev_ordinal x Hx)) (SNo_extend1 x) (SNo_extend1_SNo_ x Hx).

∎

Theorem. (SNo_extend0_nIn)

∀x, SNo x → SNoLev x ∉ SNo_extend0 x

In Proofgold the corresponding term root is 217cff... and proposition id is 0dfd17...

Proof:

Let x be given.

Assume Hx: SNo x.

Set alpha to be the term SNoLev x.

Assume H2: alpha ∈ PSNo (ordsucc alpha) (λdelta ⇒ delta ∈ x ∧ delta ≠ alpha).

Set p to be the term λdelta ⇒ delta ∈ x ∧ delta ≠ alpha of type set → prop.

Apply binunionE {beta ∈ ordsucc alpha|p beta} {beta '|beta ∈ ordsucc alpha, ¬ p beta} alpha H2 to the current goal.

Assume H3: alpha ∈ {beta ∈ ordsucc alpha|p beta}.

Apply SepE2 (ordsucc alpha) p alpha H3 to the current goal.

Assume _.

Assume H4: alpha ≠ alpha.

Apply H4 to the current goal.

Use reflexivity.

Assume H3: alpha ∈ {beta '|beta ∈ ordsucc alpha, ¬ p beta}.

Apply ReplSepE_impred (ordsucc alpha) (λbeta ⇒ ¬ p beta) (λx ⇒ x ') alpha H3 to the current goal.

Let beta be given.

Assume Hb: beta ∈ ordsucc alpha.

Assume H4: ¬ p beta.

Assume H5: alpha = beta '.

Apply tagged_not_ordinal beta to the current goal.

We will prove ordinal (beta ').

rewrite the current goal using H5 (from right to left).

We will prove ordinal alpha.

An exact proof term for the current goal is SNoLev_ordinal x Hx.

∎

Theorem. (SNo_extend1_In)

∀x, SNo x → SNoLev x ∈ SNo_extend1 x

In Proofgold the corresponding term root is ac9570... and proposition id is 8ca372...

Proof:

Let x be given.

Assume Hx: SNo x.

Set alpha to be the term SNoLev x.

Set p to be the term λdelta ⇒ delta ∈ x ∨ delta = alpha of type set → prop.

We will prove alpha ∈ {beta ∈ ordsucc alpha|p beta} ∪ {beta '|beta ∈ ordsucc alpha, ¬ p beta}.

Apply binunionI1 to the current goal.

Apply SepI to the current goal.

We will prove alpha ∈ ordsucc alpha.

Apply ordsuccI2 to the current goal.

We will prove alpha ∈ x ∨ alpha = alpha.

Apply orIR to the current goal.

Use reflexivity.

∎

Theorem. (SNo_extend0_SNoEq)

∀x, SNo x → SNoEq_ (SNoLev x) (SNo_extend0 x) x

In Proofgold the corresponding term root is bd4a27... and proposition id is 129986...

Proof:

Let x be given.

Assume Hx: SNo x.

Set alpha to be the term SNoLev x.

We prove the intermediate claim La: ordinal alpha.

An exact proof term for the current goal is SNoLev_ordinal x Hx.

We will prove SNoEq_ alpha (SNo_extend0 x) x.

Set p to be the term λbeta ⇒ beta ∈ x of type set → prop.

Set q to be the term λbeta ⇒ beta ∈ x ∧ beta ≠ alpha of type set → prop.

We will prove PNoEq_ alpha (λbeta ⇒ beta ∈ PSNo (ordsucc alpha) q) p.

Apply PNoEq_tra_ alpha (λbeta ⇒ beta ∈ PSNo (ordsucc alpha) q) q p to the current goal.

We will prove PNoEq_ alpha (λbeta ⇒ beta ∈ PSNo (ordsucc alpha) q) q.

Apply PNoEq_antimon_ (λbeta ⇒ beta ∈ PSNo (ordsucc alpha) q) q (ordsucc alpha) (ordinal_ordsucc alpha La) alpha (ordsuccI2 alpha) to the current goal.

We will prove PNoEq_ (ordsucc alpha) (λbeta ⇒ beta ∈ PSNo (ordsucc alpha) q) q.

An exact proof term for the current goal is PNoEq_PSNo (ordsucc alpha) (ordinal_ordsucc alpha La) q.

We will prove PNoEq_ alpha q p.

Apply PNoEq_sym_ to the current goal.

An exact proof term for the current goal is PNo_extend0_eq alpha p.

∎

Theorem. (SNo_extend1_SNoEq)

∀x, SNo x → SNoEq_ (SNoLev x) (SNo_extend1 x) x

In Proofgold the corresponding term root is ba974f... and proposition id is d6f8bb...

Proof:

Let x be given.

Assume Hx: SNo x.

Set alpha to be the term SNoLev x.

We prove the intermediate claim La: ordinal alpha.

An exact proof term for the current goal is SNoLev_ordinal x Hx.

We will prove SNoEq_ alpha (SNo_extend1 x) x.

Set p to be the term λbeta ⇒ beta ∈ x of type set → prop.

Set q to be the term λbeta ⇒ beta ∈ x ∨ beta = alpha of type set → prop.

We will prove PNoEq_ alpha (λbeta ⇒ beta ∈ PSNo (ordsucc alpha) q) p.

Apply PNoEq_tra_ alpha (λbeta ⇒ beta ∈ PSNo (ordsucc alpha) q) q p to the current goal.

We will prove PNoEq_ alpha (λbeta ⇒ beta ∈ PSNo (ordsucc alpha) q) q.

Apply PNoEq_antimon_ (λbeta ⇒ beta ∈ PSNo (ordsucc alpha) q) q (ordsucc alpha) (ordinal_ordsucc alpha La) alpha (ordsuccI2 alpha) to the current goal.

We will prove PNoEq_ (ordsucc alpha) (λbeta ⇒ beta ∈ PSNo (ordsucc alpha) q) q.

An exact proof term for the current goal is PNoEq_PSNo (ordsucc alpha) (ordinal_ordsucc alpha La) q.

We will prove PNoEq_ alpha q p.

Apply PNoEq_sym_ to the current goal.

An exact proof term for the current goal is PNo_extend1_eq alpha p.

∎

Theorem. (SNoLev_0_eq_0)

∀x, SNo x → SNoLev x = 0 → x = 0

In Proofgold the corresponding term root is fe0bc4... and proposition id is dfcf39...

Proof:

Let x be given.

Assume Hx Hx0.

Apply SNo_eq x 0 Hx SNo_0 to the current goal.

We will prove SNoLev x = SNoLev 0.

rewrite the current goal using SNoLev_0 (from left to right).

An exact proof term for the current goal is Hx0.

We will prove SNoEq_ (SNoLev x) x 0.

rewrite the current goal using Hx0 (from left to right).

Let alpha be given.

Assume Ha: alpha ∈ 0.

We will prove False.

An exact proof term for the current goal is EmptyE alpha Ha.

∎

Theorem. (SNo_0_eq_0)

∀q, SNo_ 0 q → q = 0

In Proofgold the corresponding term root is 72efa8... and proposition id is 7bd751...

Proof:

Let q be given.

Assume H1: SNo_ 0 q.

Apply SNoLev_0_eq_0 to the current goal.

An exact proof term for the current goal is SNo_SNo 0 ordinal_Empty q H1.

An exact proof term for the current goal is SNoLev_uniq2 0 ordinal_Empty q H1.

∎

Definition. We define eps_ to be λn ⇒ {0} ∪ {(ordsucc m) '|m ∈ n} of type set → set.

In Proofgold the corresponding term root is 5e992a... and object id is ffee2b...

Theorem. (eps_ordinal_In_eq_0)

∀n alpha, ordinal alpha → alpha ∈ eps_ n → alpha = 0

In Proofgold the corresponding term root is 3046fd... and proposition id is 1190f3...

Proof:

Let n and alpha be given.

Assume Ha.

Assume H1: alpha ∈ {0} ∪ {(ordsucc m) '|m ∈ n}.

Apply binunionE {0} {(ordsucc m) '|m ∈ n} alpha H1 to the current goal.

Assume H2: alpha ∈ {0}.

An exact proof term for the current goal is SingE 0 alpha H2.

Assume H2: alpha ∈ {(ordsucc m) '|m ∈ n}.

We will prove False.

Apply ReplE_impred n (λm ⇒ (ordsucc m) ') alpha H2 to the current goal.

Let m be given.

Assume Hm: m ∈ n.

Assume H3: alpha = (ordsucc m) '.

Apply tagged_not_ordinal (ordsucc m) to the current goal.

We will prove ordinal ((ordsucc m) ').

rewrite the current goal using H3 (from right to left).

An exact proof term for the current goal is Ha.

∎

Theorem. (eps_0_1)

eps_ 0 = 1

In Proofgold the corresponding term root is 5bbce1... and proposition id is d073f0...

Proof:

Apply set_ext to the current goal.

Let x be given.

Assume Hx: x ∈ {0} ∪ {(ordsucc m) '|m ∈ 0}.

Apply binunionE {0} {(ordsucc m) '|m ∈ 0} x Hx to the current goal.

Assume Hx: x ∈ {0}.

rewrite the current goal using SingE 0 x Hx (from left to right).

We will prove 0 ∈ 1.

An exact proof term for the current goal is In_0_1.

Assume Hx: x ∈ {(ordsucc m) '|m ∈ 0}.

Apply ReplE_impred 0 (λm ⇒ (ordsucc m) ') x Hx to the current goal.

Let m be given.

Assume Hm: m ∈ 0.

We will prove False.

An exact proof term for the current goal is EmptyE m Hm.

Let x be given.

Assume Hx: x ∈ 1.

Apply cases_1 x Hx (λx ⇒ x ∈ eps_ 0) to the current goal.

We will prove 0 ∈ {0} ∪ {(ordsucc m) '|m ∈ 0}.

Apply binunionI1 to the current goal.

Apply SingI to the current goal.

∎

Theorem. (SNo__eps_)

∀n ∈ ω, SNo_ (ordsucc n) (eps_ n)

In Proofgold the corresponding term root is e9c4d9... and proposition id is 1c1428...

Proof:

Let n be given.

Assume Hn.

We prove the intermediate claim Ln: nat_p n.

An exact proof term for the current goal is omega_nat_p n Hn.

We will prove eps_ n ⊆ SNoElts_ (ordsucc n) ∧ ∀m ∈ ordsucc n, exactly1of2 (m ' ∈ eps_ n) (m ∈ eps_ n).

Apply andI to the current goal.

Let x be given.

Assume Hx: x ∈ {0} ∪ {(ordsucc m) '|m ∈ n}.

Apply binunionE {0} {(ordsucc m) '|m ∈ n} x Hx to the current goal.

Assume Hx: x ∈ {0}.

rewrite the current goal using SingE 0 x Hx (from left to right).

We will prove 0 ∈ SNoElts_ (ordsucc n).

We will prove 0 ∈ ordsucc n ∪ {beta '|beta ∈ ordsucc n}.

Apply binunionI1 to the current goal.

We will prove 0 ∈ ordsucc n.

An exact proof term for the current goal is nat_0_in_ordsucc n Ln.

Assume Hx: x ∈ {(ordsucc m) '|m ∈ n}.

Apply ReplE_impred n (λm ⇒ (ordsucc m) ') x Hx to the current goal.

Let m be given.

Assume Hm: m ∈ n.

Assume Hxm: x = (ordsucc m) '.

We will prove x ∈ SNoElts_ (ordsucc n).

We will prove x ∈ ordsucc n ∪ {beta '|beta ∈ ordsucc n}.

Apply binunionI2 to the current goal.

We will prove x ∈ {beta '|beta ∈ ordsucc n}.

rewrite the current goal using Hxm (from left to right).

We will prove (ordsucc m) ' ∈ {beta '|beta ∈ ordsucc n}.

An exact proof term for the current goal is ReplI (ordsucc n) (λbeta ⇒ beta ') (ordsucc m) (nat_ordsucc_in_ordsucc n Ln m Hm).

Let m be given.

Assume Hm: m ∈ ordsucc n.

We prove the intermediate claim Lm: nat_p m.

An exact proof term for the current goal is nat_p_trans (ordsucc n) (nat_ordsucc n Ln) m Hm.

Apply nat_inv m Lm to the current goal.

Assume Hm: m = 0.

rewrite the current goal using Hm (from left to right).

Apply exactly1of2_I2 to the current goal.

We will prove 0 ' ∉ eps_ n.

Assume H1: 0 ' ∈ {0} ∪ {(ordsucc m) '|m ∈ n}.

Apply binunionE {0} {(ordsucc m) '|m ∈ n} (0 ') H1 to the current goal.

Assume H2: 0 ' ∈ {0}.

Apply EmptyE {1} to the current goal.

We will prove {1} ∈ 0.

rewrite the current goal using SingE 0 (0 ') H2 (from right to left) at position 2.

We will prove {1} ∈ 0 '.

We will prove {1} ∈ 0 ∪ {{1}}.

Apply binunionI2 to the current goal.

We will prove {1} ∈ {{1}}.

Apply SingI to the current goal.

Assume H2: 0 ' ∈ {(ordsucc m) '|m ∈ n}.

Apply ReplE_impred n (λm ⇒ (ordsucc m) ') (0 ') H2 to the current goal.

Let m be given.

Assume Hm: m ∈ n.

Assume H3: 0 ' = (ordsucc m) '.

Apply neq_0_ordsucc m to the current goal.

We will prove 0 = ordsucc m.

Apply tagged_eqE_eq to the current goal.

We will prove ordinal 0.

An exact proof term for the current goal is ordinal_Empty.

We will prove ordinal (ordsucc m).

An exact proof term for the current goal is (nat_p_ordinal (ordsucc m) (nat_ordsucc m (nat_p_trans n Ln m Hm))).

We will prove 0 ' = (ordsucc m) '.

An exact proof term for the current goal is H3.

We will prove 0 ∈ eps_ n.

We will prove 0 ∈ {0} ∪ {(ordsucc m) '|m ∈ n}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is SingI 0.

Assume H1.

Apply H1 to the current goal.

Let k be given.

Assume H1.

Apply H1 to the current goal.

Assume Hk: nat_p k.

Assume Hmk: m = ordsucc k.

We prove the intermediate claim Lm: nat_p m.

rewrite the current goal using Hmk (from left to right).

An exact proof term for the current goal is nat_ordsucc k Hk.

We prove the intermediate claim LSk: ordsucc k ∈ ordsucc n.

rewrite the current goal using Hmk (from right to left).

An exact proof term for the current goal is Hm.

We prove the intermediate claim Lk: k ∈ n.

Apply ordsuccE n (ordsucc k) LSk to the current goal.

Assume H2: ordsucc k ∈ n.

Apply nat_trans n Ln (ordsucc k) H2 to the current goal.

We will prove k ∈ ordsucc k.

Apply ordsuccI2 to the current goal.

Assume H2: ordsucc k = n.

rewrite the current goal using H2 (from right to left).

Apply ordsuccI2 to the current goal.

Apply exactly1of2_I1 to the current goal.

We will prove m ' ∈ eps_ n.

We will prove m ' ∈ {0} ∪ {(ordsucc m) '|m ∈ n}.

Apply binunionI2 to the current goal.

rewrite the current goal using Hmk (from left to right).

We will prove (ordsucc k) ' ∈ {(ordsucc m) '|m ∈ n}.

An exact proof term for the current goal is ReplI n (λk ⇒ (ordsucc k) ') k Lk.

We will prove m ∉ eps_ n.

Assume H1: m ∈ {0} ∪ {(ordsucc m) '|m ∈ n}.

Apply binunionE {0} {(ordsucc m) '|m ∈ n} m H1 to the current goal.

Assume H2: m ∈ {0}.

Apply EmptyE 0 to the current goal.

We will prove 0 ∈ 0.

rewrite the current goal using SingE 0 m H2 (from right to left) at position 2.

We will prove 0 ∈ m.

rewrite the current goal using Hmk (from left to right).

An exact proof term for the current goal is nat_0_in_ordsucc k Hk.

Assume H2: m ∈ {(ordsucc j) '|j ∈ n}.

Apply ReplE_impred n (λj ⇒ (ordsucc j) ') m H2 to the current goal.

Let j be given.

Assume Hj: j ∈ n.

Assume Hmj: m = (ordsucc j) '.

Apply tagged_not_ordinal (ordsucc j) to the current goal.

We will prove ordinal ((ordsucc j) ').

rewrite the current goal using Hmj (from right to left).

We will prove ordinal m.

An exact proof term for the current goal is nat_p_ordinal m Lm.

∎

Theorem. (SNo_eps_)

∀n ∈ ω, SNo (eps_ n)

In Proofgold the corresponding term root is 9fb700... and proposition id is 006b0f...

Proof:

Let n be given.

Assume Hn.

We prove the intermediate claim Ln: nat_p n.

An exact proof term for the current goal is omega_nat_p n Hn.

An exact proof term for the current goal is SNo_SNo (ordsucc n) (ordinal_ordsucc n (nat_p_ordinal n Ln)) (eps_ n) (SNo__eps_ n Hn).

∎

Theorem. (SNo_eps_1)

SNo (eps_ 1)

In Proofgold the corresponding term root is 17c276... and proposition id is 8b78d7...

Proof:

An exact proof term for the current goal is SNo_eps_ 1 (nat_p_omega 1 nat_1).

∎

Theorem. (SNoLev_eps_)

∀n ∈ ω, SNoLev (eps_ n) = ordsucc n

In Proofgold the corresponding term root is 6891e3... and proposition id is 75efd1...

Proof:

Let n be given.

Assume Hn.

We prove the intermediate claim Ln: nat_p n.

An exact proof term for the current goal is omega_nat_p n Hn.

Apply SNoLev_uniq2 (ordsucc n) (ordinal_ordsucc n (nat_p_ordinal n Ln)) (eps_ n) (SNo__eps_ n Hn) to the current goal.

∎

Theorem. (SNo_eps_SNoS_omega)

∀n ∈ ω, eps_ n ∈ SNoS_ ω

In Proofgold the corresponding term root is 736d2a... and proposition id is 52da18...

Proof:

Let n be given.

Assume Hn.

Apply SNoS_I ω omega_ordinal (eps_ n) (ordsucc n) to the current goal.

We will prove ordsucc n ∈ ω.

An exact proof term for the current goal is omega_ordsucc n Hn.

We will prove SNo_ (ordsucc n) (eps_ n).

An exact proof term for the current goal is SNo__eps_ n Hn.

∎

Theorem. (SNo_eps_decr)

∀n ∈ ω, ∀m ∈ n, eps_ n < eps_ m

In Proofgold the corresponding term root is d6a46a... and proposition id is 67c76a...

Proof:

Let n be given.

Assume Hn.

Let m be given.

Assume Hm.

We prove the intermediate claim Lnn: nat_p n.

An exact proof term for the current goal is omega_nat_p n Hn.

We prove the intermediate claim Lmn: nat_p m.

An exact proof term for the current goal is nat_p_trans n Lnn m Hm.

We prove the intermediate claim Lm: m ∈ ω.

An exact proof term for the current goal is nat_p_omega m Lmn.

Apply SNoLtI3 to the current goal.

We will prove SNoLev (eps_ m) ∈ SNoLev (eps_ n).

rewrite the current goal using SNoLev_eps_ m Lm (from left to right).

rewrite the current goal using SNoLev_eps_ n Hn (from left to right).

We will prove ordsucc m ∈ ordsucc n.

An exact proof term for the current goal is nat_ordsucc_in_ordsucc n Lnn m Hm.

We will prove SNoEq_ (SNoLev (eps_ m)) (eps_ n) (eps_ m).

rewrite the current goal using SNoLev_eps_ m Lm (from left to right).

We will prove SNoEq_ (ordsucc m) (eps_ n) (eps_ m).

Let k be given.

Assume Hk: k ∈ ordsucc m.

We will prove k ∈ eps_ n ↔ k ∈ eps_ m.

We prove the intermediate claim Lk: ordinal k.

An exact proof term for the current goal is nat_p_ordinal k (nat_p_trans (ordsucc m) (nat_ordsucc m Lmn) k Hk).

Apply iffI to the current goal.

Assume H1: k ∈ eps_ n.

rewrite the current goal using eps_ordinal_In_eq_0 n k Lk H1 (from left to right).

We will prove 0 ∈ eps_ m.

We will prove 0 ∈ {0} ∪ {(ordsucc j) '|j ∈ m}.

Apply binunionI1 to the current goal.

Apply SingI to the current goal.

Assume H1: k ∈ eps_ m.

rewrite the current goal using eps_ordinal_In_eq_0 m k Lk H1 (from left to right).

We will prove 0 ∈ eps_ n.

We will prove 0 ∈ {0} ∪ {(ordsucc j) '|j ∈ n}.

Apply binunionI1 to the current goal.

Apply SingI to the current goal.

We will prove SNoLev (eps_ m) ∉ eps_ n.

rewrite the current goal using SNoLev_eps_ m Lm (from left to right).

Assume H1: ordsucc m ∈ eps_ n.

Apply neq_ordsucc_0 m to the current goal.

We will prove ordsucc m = 0.

An exact proof term for the current goal is eps_ordinal_In_eq_0 n (ordsucc m) (ordinal_ordsucc m (nat_p_ordinal m Lmn)) H1.

∎

Theorem. (SNo_eps_pos)

∀n ∈ ω, 0 < eps_ n

In Proofgold the corresponding term root is 8b75de... and proposition id is 760b4a...

Proof:

Let n be given.

Assume Hn.

Apply SNoLtI2 0 (eps_ n) to the current goal.

We will prove SNoLev 0 ∈ SNoLev (eps_ n).

rewrite the current goal using SNoLev_0 (from left to right).

rewrite the current goal using SNoLev_eps_ n Hn (from left to right).

We will prove 0 ∈ ordsucc n.

An exact proof term for the current goal is nat_0_in_ordsucc n (omega_nat_p n Hn).

We will prove SNoEq_ (SNoLev 0) 0 (eps_ n).

rewrite the current goal using SNoLev_0 (from left to right).

Let alpha be given.

Assume Ha: alpha ∈ 0.

We will prove False.

An exact proof term for the current goal is EmptyE alpha Ha.

We will prove SNoLev 0 ∈ eps_ n.

rewrite the current goal using SNoLev_0 (from left to right).

We will prove 0 ∈ eps_ n.

We will prove 0 ∈ {0} ∪ {(ordsucc m) '|m ∈ n}.

Apply binunionI1 to the current goal.

Apply SingI to the current goal.

∎

Theorem. (SNo_pos_eps_Lt)

∀n, nat_p n → ∀x ∈ SNoS_ (ordsucc n), 0 < x → eps_ n < x

In Proofgold the corresponding term root is 72974f... and proposition id is 771b0e...

Proof:

Let n be given.

Assume Hn: nat_p n.

Let x be given.

Assume Hx: x ∈ SNoS_ (ordsucc n).

Assume Hxpos: 0 < x.

We prove the intermediate claim Ln: n ∈ ω.

An exact proof term for the current goal is nat_p_omega n Hn.

Apply SNoS_E2 (ordsucc n) (nat_p_ordinal (ordsucc n) (nat_ordsucc n Hn)) x Hx to the current goal.

Assume Hx1: SNoLev x ∈ ordsucc n.

Assume Hx2: ordinal (SNoLev x).

Assume Hx3: SNo x.

Assume Hx4: SNo_ (SNoLev x) x.

We will prove eps_ n < x.

Apply SNoLt_trichotomy_or_impred (eps_ n) x (SNo_eps_ n Ln) Hx3 to the current goal.

Assume H2: eps_ n < x.

An exact proof term for the current goal is H2.

Assume H2: eps_ n = x.

We will prove False.

Apply In_irref (ordsucc n) to the current goal.

rewrite the current goal using SNoLev_eps_ n Ln (from right to left) at position 1.

We will prove SNoLev (eps_ n) ∈ ordsucc n.

rewrite the current goal using H2 (from left to right).

An exact proof term for the current goal is Hx1.

Assume H2: x < eps_ n.

We will prove False.

Apply SNoLtE x (eps_ n) Hx3 (SNo_eps_ n Ln) H2 to the current goal.

Let z be given.

Assume Hz1: SNo z.

Assume Hz2: SNoLev z ∈ SNoLev x ∩ SNoLev (eps_ n).

Assume Hz3: SNoEq_ (SNoLev z) z x.

Assume Hz4: SNoEq_ (SNoLev z) z (eps_ n).

Assume Hz5: x < z.

Assume Hz6: z < eps_ n.

Assume Hz7: SNoLev z ∉ x.

Assume Hz8: SNoLev z ∈ eps_ n.

We prove the intermediate claim Lz0: z = 0.

Apply SNoLev_0_eq_0 z Hz1 to the current goal.

An exact proof term for the current goal is eps_ordinal_In_eq_0 n (SNoLev z) (SNoLev_ordinal z Hz1) Hz8.

Apply SNoLt_irref x to the current goal.

We will prove x < x.

Apply SNoLt_tra x z x Hx3 Hz1 Hx3 Hz5 to the current goal.

We will prove z < x.

rewrite the current goal using Lz0 (from left to right).

An exact proof term for the current goal is Hxpos.

Assume H1: SNoLev x ∈ SNoLev (eps_ n).

Assume H2: SNoEq_ (SNoLev x) x (eps_ n).

Assume H3: SNoLev x ∈ (eps_ n).

We prove the intermediate claim Lx0: x = 0.

Apply SNoLev_0_eq_0 x Hx3 to the current goal.

An exact proof term for the current goal is eps_ordinal_In_eq_0 n (SNoLev x) Hx2 H3.

Apply SNoLt_irref x to the current goal.

rewrite the current goal using Lx0 (from left to right) at position 1.

An exact proof term for the current goal is Hxpos.

rewrite the current goal using SNoLev_eps_ n Ln (from left to right).

Assume H1: ordsucc n ∈ SNoLev x.

We will prove False.

An exact proof term for the current goal is In_no2cycle (SNoLev x) (ordsucc n) Hx1 H1.

∎

Theorem. (SNo_pos_eps_Le)

∀n, nat_p n → ∀x ∈ SNoS_ (ordsucc (ordsucc n)), 0 < x → eps_ n ≤ x

In Proofgold the corresponding term root is f1e297... and proposition id is 6658de...

Proof:

Let n be given.

Assume Hn.

Let x be given.

Assume Hx: x ∈ SNoS_ (ordsucc (ordsucc n)).

Assume Hxpos: 0 < x.

We prove the intermediate claim Ln: n ∈ ω.

An exact proof term for the current goal is nat_p_omega n Hn.

Apply SNoS_E2 (ordsucc (ordsucc n)) (nat_p_ordinal (ordsucc (ordsucc n)) (nat_ordsucc (ordsucc n) (nat_ordsucc n Hn))) x Hx to the current goal.

Assume Hx1: SNoLev x ∈ ordsucc (ordsucc n).

Assume Hx2: ordinal (SNoLev x).

Assume Hx3: SNo x.

Assume Hx4: SNo_ (SNoLev x) x.

We will prove eps_ n ≤ x.

Apply SNoLtLe_or x (eps_ n) Hx3 (SNo_eps_ n Ln) to the current goal.

Assume H2: x < eps_ n.

We will prove False.

Apply SNoLtE x (eps_ n) Hx3 (SNo_eps_ n Ln) H2 to the current goal.

Let z be given.

Assume Hz1: SNo z.

Assume Hz2: SNoLev z ∈ SNoLev x ∩ SNoLev (eps_ n).

Assume Hz3: SNoEq_ (SNoLev z) z x.

Assume Hz4: SNoEq_ (SNoLev z) z (eps_ n).

Assume Hz5: x < z.

Assume Hz6: z < eps_ n.

Assume Hz7: SNoLev z ∉ x.

Assume Hz8: SNoLev z ∈ eps_ n.

We prove the intermediate claim Lz0: z = 0.

Apply SNoLev_0_eq_0 z Hz1 to the current goal.

An exact proof term for the current goal is eps_ordinal_In_eq_0 n (SNoLev z) (SNoLev_ordinal z Hz1) Hz8.

Apply SNoLt_irref x to the current goal.

We will prove x < x.

Apply SNoLt_tra x z x Hx3 Hz1 Hx3 Hz5 to the current goal.

We will prove z < x.

rewrite the current goal using Lz0 (from left to right).

An exact proof term for the current goal is Hxpos.

Assume H1: SNoLev x ∈ SNoLev (eps_ n).

Assume H2: SNoEq_ (SNoLev x) x (eps_ n).

Assume H3: SNoLev x ∈ (eps_ n).

We prove the intermediate claim Lx0: x = 0.

Apply SNoLev_0_eq_0 x Hx3 to the current goal.

An exact proof term for the current goal is eps_ordinal_In_eq_0 n (SNoLev x) Hx2 H3.

Apply SNoLt_irref x to the current goal.

rewrite the current goal using Lx0 (from left to right) at position 1.

An exact proof term for the current goal is Hxpos.

rewrite the current goal using SNoLev_eps_ n Ln (from left to right).

Assume H3: ordsucc n ∈ SNoLev x.

We will prove False.

Apply ordsuccE (ordsucc n) (SNoLev x) Hx1 to the current goal.

Assume H4: SNoLev x ∈ ordsucc n.

An exact proof term for the current goal is In_no2cycle (SNoLev x) (ordsucc n) H4 H3.

Assume H4: SNoLev x = ordsucc n.

Apply In_irref (SNoLev x) to the current goal.

rewrite the current goal using H4 (from left to right) at position 1.

An exact proof term for the current goal is H3.

Assume H2: eps_ n ≤ x.

An exact proof term for the current goal is H2.

∎

Theorem. (eps_SNo_eq)

∀n, nat_p n → ∀x ∈ SNoS_ (ordsucc n), 0 < x → SNoEq_ (SNoLev x) (eps_ n) x → ∃m ∈ n, x = eps_ m

In Proofgold the corresponding term root is 8c2587... and proposition id is 8515ac...

Proof:

Let n be given.

Assume Hn.

Let x be given.

Assume Hx1: x ∈ SNoS_ (ordsucc n).

Assume Hx2: 0 < x.

Assume Hx3: SNoEq_ (SNoLev x) (eps_ n) x.

Apply SNoS_E2 (ordsucc n) (nat_p_ordinal (ordsucc n) (nat_ordsucc n Hn)) x Hx1 to the current goal.

Assume Hx1a: SNoLev x ∈ ordsucc n.

Assume Hx1b: ordinal (SNoLev x).

Assume Hx1c: SNo x.

Assume Hx1d: SNo_ (SNoLev x) x.

We prove the intermediate claim L1: nat_p (SNoLev x).

Apply nat_p_trans (ordsucc n) (nat_ordsucc n Hn) to the current goal.

We will prove SNoLev x ∈ ordsucc n.

An exact proof term for the current goal is Hx1a.

Apply nat_inv (SNoLev x) L1 to the current goal.

Assume H1: SNoLev x = 0.

We will prove False.

We prove the intermediate claim L2: x = 0.

An exact proof term for the current goal is SNoLev_0_eq_0 x Hx1c H1.

Apply SNoLt_irref x to the current goal.

rewrite the current goal using L2 (from left to right) at position 1.

An exact proof term for the current goal is Hx2.

Assume H1.

Apply H1 to the current goal.

Let m be given.

Assume H1.

Apply H1 to the current goal.

Assume Hm1: nat_p m.

Assume Hm2: SNoLev x = ordsucc m.

We use m to witness the existential quantifier.

Apply andI to the current goal.

We will prove m ∈ n.

Apply nat_ordsucc_trans n Hn (SNoLev x) Hx1a to the current goal.

We will prove m ∈ SNoLev x.

rewrite the current goal using Hm2 (from left to right).

Apply ordsuccI2 to the current goal.

We will prove x = eps_ m.

Apply SNo_eq x (eps_ m) Hx1c (SNo_eps_ m (nat_p_omega m Hm1)) to the current goal.

We will prove SNoLev x = SNoLev (eps_ m).

rewrite the current goal using SNoLev_eps_ m (nat_p_omega m Hm1) (from left to right).

An exact proof term for the current goal is Hm2.

We will prove SNoEq_ (SNoLev x) x (eps_ m).

Apply SNoEq_tra_ (SNoLev x) x (eps_ n) (eps_ m) to the current goal.

Apply SNoEq_sym_ to the current goal.

An exact proof term for the current goal is Hx3.

We will prove SNoEq_ (SNoLev x) (eps_ n) (eps_ m).

rewrite the current goal using Hm2 (from left to right).

We will prove SNoEq_ (ordsucc m) (eps_ n) (eps_ m).

Apply SNoEq_I to the current goal.

Let k be given.

Assume Hk: k ∈ ordsucc m.

We prove the intermediate claim L3: ordinal k.

An exact proof term for the current goal is nat_p_ordinal k (nat_p_trans (ordsucc m) (nat_ordsucc m Hm1) k Hk).

Apply iffI to the current goal.

Assume H2: k ∈ eps_ n.

rewrite the current goal using eps_ordinal_In_eq_0 n k L3 H2 (from left to right).

We will prove 0 ∈ eps_ m.

We will prove 0 ∈ {0} ∪ {SetAdjoin (ordsucc k) {1}|k ∈ m}.

Apply binunionI1 to the current goal.

Apply SingI to the current goal.

Assume H2: k ∈ eps_ m.

rewrite the current goal using eps_ordinal_In_eq_0 m k L3 H2 (from left to right).

We will prove 0 ∈ eps_ n.

We will prove 0 ∈ {0} ∪ {SetAdjoin (ordsucc k) {1}|k ∈ n}.

Apply binunionI1 to the current goal.

Apply SingI to the current goal.

∎

Theorem. (eps_SNoCutP)

∀n ∈ ω, SNoCutP {0} {eps_ m|m ∈ n}

In Proofgold the corresponding term root is 545873... and proposition id is 30edf9...

Proof:

Let n be given.

Assume Hn.

Set L to be the term {0}.

Set R to be the term {eps_ m|m ∈ n}.

We prove the intermediate claim Ln: nat_p n.

An exact proof term for the current goal is omega_nat_p n Hn.

We will prove (∀w ∈ L, SNo w) ∧ (∀z ∈ R, SNo z) ∧ (∀w ∈ L, ∀z ∈ R, w < z).

Apply and3I to the current goal.

Let w be given.

Assume Hw.

rewrite the current goal using SingE 0 w Hw (from left to right).

An exact proof term for the current goal is SNo_0.

Let z be given.

Assume Hz.

Apply ReplE_impred n eps_ z Hz to the current goal.

Let m be given.

Assume Hm1: m ∈ n.

Assume Hm2: z = eps_ m.

rewrite the current goal using Hm2 (from left to right).

Apply SNo_eps_ to the current goal.

We will prove m ∈ ω.

Apply nat_p_omega to the current goal.

An exact proof term for the current goal is nat_p_trans n Ln m Hm1.

Let w be given.

Assume Hw.

Let z be given.

Assume Hz.

Apply ReplE_impred n eps_ z Hz to the current goal.

Let m be given.

Assume Hm1: m ∈ n.

Assume Hm2: z = eps_ m.

rewrite the current goal using SingE 0 w Hw (from left to right).

rewrite the current goal using Hm2 (from left to right).

We will prove 0 < eps_ m.

Apply SNo_eps_pos to the current goal.

We will prove m ∈ ω.

Apply nat_p_omega to the current goal.

An exact proof term for the current goal is nat_p_trans n Ln m Hm1.

∎

Theorem. (eps_SNoCut)

∀n ∈ ω, eps_ n = SNoCut {0} {eps_ m|m ∈ n}

In Proofgold the corresponding term root is 06d6c5... and proposition id is eba0c6...

Proof:

Let n be given.

Assume Hn.

Set L to be the term {0}.

Set R to be the term {eps_ m|m ∈ n}.

We prove the intermediate claim Ln: nat_p n.

An exact proof term for the current goal is omega_nat_p n Hn.

We prove the intermediate claim L1: SNoCutP L R.

An exact proof term for the current goal is eps_SNoCutP n Hn.

We prove the intermediate claim LRS: ∀z ∈ R, SNo z.

Apply L1 to the current goal.

Assume H _.

Apply H to the current goal.

Assume _ H.

An exact proof term for the current goal is H.

We prove the intermediate claim L2: (⋃_{x ∈ L}ordsucc (SNoLev x)) = 1.

Apply set_ext to the current goal.

Let k be given.

Assume Hk.

Apply famunionE_impred L (λx ⇒ ordsucc (SNoLev x)) k Hk to the current goal.

Let w be given.

Assume Hw: w ∈ L.

rewrite the current goal using SingE 0 w Hw (from left to right).

rewrite the current goal using SNoLev_0 (from left to right).

Assume H2: k ∈ 1.

We will prove k ∈ 1.

An exact proof term for the current goal is H2.

Let i be given.

Assume Hi.

Apply cases_1 i Hi (λi ⇒ i ∈ ⋃_{x ∈ L}ordsucc (SNoLev x)) to the current goal.

We will prove 0 ∈ ⋃_{x ∈ L}ordsucc (SNoLev x).

Apply famunionI L (λx ⇒ ordsucc (SNoLev x)) 0 0 (SingI 0) to the current goal.

We will prove 0 ∈ ordsucc (SNoLev 0).

rewrite the current goal using SNoLev_0 (from left to right).

An exact proof term for the current goal is In_0_1.

We prove the intermediate claim L3: n ≠ 0 → (⋃_{y ∈ R}ordsucc (SNoLev y)) = ordsucc n.

Assume Hn0: n ≠ 0.

Apply set_ext to the current goal.

Let k be given.

Assume Hk.

Apply famunionE_impred R (λy ⇒ ordsucc (SNoLev y)) k Hk to the current goal.

Let z be given.

Assume Hz: z ∈ R.

Apply ReplE_impred n eps_ z Hz to the current goal.

Let m be given.

Assume Hm1: m ∈ n.

Assume Hm2: z = eps_ m.

rewrite the current goal using Hm2 (from left to right).

rewrite the current goal using SNoLev_eps_ m (nat_p_omega m (nat_p_trans n Ln m Hm1)) (from left to right).

Assume H2: k ∈ ordsucc (ordsucc m).

We will prove k ∈ ordsucc n.

We prove the intermediate claim L3a: ordsucc m ∈ ordsucc n.

Apply ordinal_ordsucc_In to the current goal.

We will prove ordinal n.

Apply nat_p_ordinal n to the current goal.

An exact proof term for the current goal is Ln.

An exact proof term for the current goal is Hm1.

We prove the intermediate claim L3b: ordsucc m ⊆ ordsucc n.

An exact proof term for the current goal is nat_trans (ordsucc n) (nat_ordsucc n Ln) (ordsucc m) L3a.

Apply ordsuccE (ordsucc m) k H2 to the current goal.

Assume H3: k ∈ ordsucc m.

Apply L3b to the current goal.

An exact proof term for the current goal is H3.

Assume H3: k = ordsucc m.

rewrite the current goal using H3 (from left to right).

An exact proof term for the current goal is L3a.

Let i be given.

Assume Hi: i ∈ ordsucc n.

We will prove i ∈ ⋃_{y ∈ R}ordsucc (SNoLev y).

Apply nat_inv n Ln to the current goal.

Assume H2: n = 0.

We will prove False.

An exact proof term for the current goal is Hn0 H2.

Assume H2.

Apply H2 to the current goal.

Let n' be given.

Assume H2.

Apply H2 to the current goal.

Assume Hn'1: nat_p n'.

Assume Hn'2: n = ordsucc n'.

Apply famunionI R (λy ⇒ ordsucc (SNoLev y)) (eps_ n') i to the current goal.

We will prove eps_ n' ∈ R.

Apply ReplI to the current goal.

We will prove n' ∈ n.

rewrite the current goal using Hn'2 (from left to right).

Apply ordsuccI2 to the current goal.

We will prove i ∈ ordsucc (SNoLev (eps_ n')).

rewrite the current goal using SNoLev_eps_ n' (nat_p_omega n' Hn'1) (from left to right).

We will prove i ∈ ordsucc (ordsucc n').

rewrite the current goal using Hn'2 (from right to left).

An exact proof term for the current goal is Hi.

We prove the intermediate claim L4: (⋃_{x ∈ L}ordsucc (SNoLev x)) ∪ (⋃_{y ∈ R}ordsucc (SNoLev y)) = ordsucc n.

Apply xm (n = 0) to the current goal.

Assume H2: n = 0.

We prove the intermediate claim L4a: R = 0.

Apply Empty_eq to the current goal.

Let z be given.

Assume Hz.

Apply ReplE_impred n eps_ z Hz to the current goal.

Let m be given.

rewrite the current goal using H2 (from left to right).

Assume Hm1: m ∈ 0.

We will prove False.

An exact proof term for the current goal is EmptyE m Hm1.

rewrite the current goal using L4a (from left to right).

rewrite the current goal using famunion_Empty (λy ⇒ ordsucc (SNoLev y)) (from left to right).

We will prove (⋃_{x ∈ L}ordsucc (SNoLev x)) ∪ 0 = ordsucc n.

rewrite the current goal using binunion_idr (from left to right).

We will prove (⋃_{x ∈ L}ordsucc (SNoLev x)) = ordsucc n.

rewrite the current goal using H2 (from left to right).

An exact proof term for the current goal is L2.

Assume H2: n ≠ 0.

rewrite the current goal using L3 H2 (from right to left).

rewrite the current goal using Subq_binunion_eq (from right to left).

rewrite the current goal using L2 (from left to right).

rewrite the current goal using L3 H2 (from left to right).

We will prove 1 ⊆ ordsucc n.

Let i be given.

Assume Hi.

Apply cases_1 i Hi (λi ⇒ i ∈ ordsucc n) to the current goal.

We will prove 0 ∈ ordsucc n.

Apply nat_0_in_ordsucc to the current goal.

An exact proof term for the current goal is Ln.

Apply SNoCutP_SNoCut_impred L R L1 to the current goal.

Assume H1: SNo (SNoCut L R).

rewrite the current goal using L4 (from left to right).

Assume H2: SNoLev (SNoCut L R) ∈ ordsucc (ordsucc n).

Assume H3: ∀w ∈ L, w < SNoCut L R.

Assume H4: ∀z ∈ R, SNoCut L R < z.

Assume H5: ∀u, SNo u → (∀w ∈ L, w < u) → (∀z ∈ R, u < z) → SNoLev (SNoCut L R) ⊆ SNoLev u ∧ SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) u.

We prove the intermediate claim L5: SNo (eps_ n).

An exact proof term for the current goal is SNo_eps_ n Hn.

We prove the intermediate claim L6: ∀w ∈ L, w < eps_ n.

Let w be given.

Assume Hw.

rewrite the current goal using SingE 0 w Hw (from left to right).

We will prove 0 < eps_ n.

An exact proof term for the current goal is SNo_eps_pos n Hn.

We prove the intermediate claim L7: ∀z ∈ R, eps_ n < z.

Let z be given.

Assume Hz.

Apply ReplE_impred n eps_ z Hz to the current goal.

Let m be given.

Assume Hm1: m ∈ n.

Assume Hm2: z = eps_ m.

rewrite the current goal using Hm2 (from left to right).

We will prove eps_ n < eps_ m.

An exact proof term for the current goal is SNo_eps_decr n Hn m Hm1.

Apply H5 (eps_ n) L5 L6 L7 to the current goal.

Assume H6: SNoLev (SNoCut L R) ⊆ SNoLev (eps_ n).

Assume H7: SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) (eps_ n).

Use symmetry.

Apply SNo_eq (SNoCut L R) (eps_ n) H1 L5 to the current goal.

We will prove SNoLev (SNoCut L R) = SNoLev (eps_ n).

rewrite the current goal using SNoLev_eps_ n Hn (from left to right).

We will prove SNoLev (SNoCut L R) = ordsucc n.

Apply ordsuccE (ordsucc n) (SNoLev (SNoCut L R)) H2 to the current goal.

Assume H8: SNoLev (SNoCut L R) ∈ ordsucc n.

We will prove False.

We prove the intermediate claim L8: eps_ n < SNoCut L R.

Apply SNo_pos_eps_Lt n (omega_nat_p n Hn) (SNoCut L R) to the current goal.

We will prove SNoCut L R ∈ SNoS_ (ordsucc n).

Apply SNoS_I (ordsucc n) (nat_p_ordinal (ordsucc n) (nat_ordsucc n (omega_nat_p n Hn))) (SNoCut L R) (SNoLev (SNoCut L R)) H8 to the current goal.

We will prove SNo_ (SNoLev (SNoCut L R)) (SNoCut L R).

An exact proof term for the current goal is SNoLev_ (SNoCut L R) H1.

We will prove 0 < SNoCut L R.

Apply H3 to the current goal.

Apply SingI to the current goal.

Apply SNoLtE (eps_ n) (SNoCut L R) (SNo_eps_ n Hn) H1 L8 to the current goal.

Let z be given.

Assume Hz1: SNo z.

Assume Hz2: SNoLev z ∈ SNoLev (eps_ n) ∩ SNoLev (SNoCut L R).

Assume Hz3: SNoEq_ (SNoLev z) z (eps_ n).

Assume Hz4: SNoEq_ (SNoLev z) z (SNoCut L R).

Assume Hz5: eps_ n < z.

Assume Hz6: z < SNoCut L R.

Assume Hz7: SNoLev z ∉ eps_ n.

Assume Hz8: SNoLev z ∈ SNoCut L R.

We prove the intermediate claim L9: ∀w ∈ L, w < z.

Let w be given.

Assume Hw.

rewrite the current goal using SingE 0 w Hw (from left to right).

We will prove 0 < z.

Apply SNoLt_tra 0 (eps_ n) z SNo_0 (SNo_eps_ n Hn) Hz1 to the current goal.

An exact proof term for the current goal is SNo_eps_pos n Hn.

An exact proof term for the current goal is Hz5.

We prove the intermediate claim L10: ∀v ∈ R, z < v.

Let v be given.

Assume Hv.

Apply SNoLt_tra z (SNoCut L R) v Hz1 H1 (LRS v Hv) Hz6 to the current goal.

We will prove SNoCut L R < v.

Apply H4 to the current goal.

An exact proof term for the current goal is Hv.

Apply H5 z Hz1 L9 L10 to the current goal.

Assume H9: SNoLev (SNoCut L R) ⊆ SNoLev z.

We will prove False.

Apply In_irref (SNoLev z) to the current goal.

Apply H9 to the current goal.

An exact proof term for the current goal is binintersectE2 (SNoLev (eps_ n)) (SNoLev (SNoCut L R)) (SNoLev z) Hz2.

rewrite the current goal using SNoLev_eps_ n Hn (from left to right).

Assume H9: ordsucc n ∈ SNoLev (SNoCut L R).

We will prove False.

An exact proof term for the current goal is In_no2cycle (SNoLev (SNoCut L R)) (ordsucc n) H8 H9.

rewrite the current goal using SNoLev_eps_ n Hn (from left to right).

Assume H9: SNoLev (SNoCut L R) ∈ ordsucc n.

Assume H10: SNoEq_ (SNoLev (SNoCut L R)) (eps_ n) (SNoCut L R).

Assume H11: SNoLev (SNoCut L R) ∉ eps_ n.

We prove the intermediate claim L11: ∃m ∈ n, SNoCut L R = eps_ m.

Apply eps_SNo_eq n (omega_nat_p n Hn) (SNoCut L R) to the current goal.

We will prove SNoCut L R ∈ SNoS_ (ordsucc n).

Apply SNoS_I (ordsucc n) (nat_p_ordinal (ordsucc n) (nat_ordsucc n (omega_nat_p n Hn))) (SNoCut L R) (SNoLev (SNoCut L R)) to the current goal.

We will prove SNoLev (SNoCut L R) ∈ ordsucc n.

An exact proof term for the current goal is H9.

We will prove SNo_ (SNoLev (SNoCut L R)) (SNoCut L R).

Apply SNoLev_ to the current goal.

An exact proof term for the current goal is H1.

We will prove 0 < SNoCut L R.

Apply H3 to the current goal.

Apply SingI to the current goal.

We will prove SNoEq_ (SNoLev (SNoCut L R)) (eps_ n) (SNoCut L R).

An exact proof term for the current goal is H10.

Apply L11 to the current goal.

Let m be given.

Assume H12.

Apply H12 to the current goal.

Assume Hm1: m ∈ n.

Assume Hm2: SNoCut L R = eps_ m.

Apply SNoLt_irref (eps_ m) to the current goal.

We will prove eps_ m < eps_ m.

rewrite the current goal using Hm2 (from right to left) at position 1.

We will prove SNoCut L R < eps_ m.

Apply H4 to the current goal.

We will prove eps_ m ∈ {eps_ m|m ∈ n}.

Apply ReplI to the current goal.

An exact proof term for the current goal is Hm1.

Assume H8: SNoLev (SNoCut L R) = ordsucc n.

An exact proof term for the current goal is H8.

An exact proof term for the current goal is H7.

∎

End of Section TaggedSets2