Surreal Numbers as Ordinals Paired with Predicates
From Part 1
Object . The name
Eps_i is a term of type
(set → prop ) → set .
Axiom. (
Eps_i_ax ) We take the following as an axiom:
∀P : set → prop , ∀x : set , P x → P (Eps_i P )
Definition. We define
True to be
∀p : prop , p → p of type
prop .
Definition. We define
False to be
∀p : prop , p of type
prop .
Definition. We define
not to be
λA : prop ⇒ A → False of type
prop → prop .
Notation . We use
¬ as a prefix operator with priority 700 corresponding to applying term
not .
Definition. We define
and to be
λA B : prop ⇒ ∀p : prop , (A → B → p ) → p of type
prop → prop → prop .
Notation . We use
∧ as an infix operator with priority 780 and which associates to the left corresponding to applying term
and .
Definition. We define
or to be
λA B : prop ⇒ ∀p : prop , (A → p ) → (B → p ) → p of type
prop → prop → prop .
Notation . We use
∨ as an infix operator with priority 785 and which associates to the left corresponding to applying term
or .
Definition. We define
iff to be
λA B : prop ⇒ and (A → B ) (B → A ) of type
prop → prop → prop .
Notation . We use
↔ as an infix operator with priority 805 and no associativity corresponding to applying term
iff .
Beginning of Section Eq
Variable A : SType
Definition. We define
eq to be
λx y : A ⇒ ∀Q : A → A → prop , Q x y → Q y x of type
A → A → prop .
Definition. We define
neq to be
λx y : A ⇒ ¬ eq x y of type
A → A → prop .
End of Section Eq
Notation . We use
= as an infix operator with priority 502 and no associativity corresponding to applying term
eq .
Notation . We use
≠ as an infix operator with priority 502 and no associativity corresponding to applying term
neq .
Beginning of Section FE
Variable A B : SType
Axiom. (
func_ext ) We take the following as an axiom:
∀f g : A → B , (∀x : A , f x = g x ) → f = g
End of Section FE
Beginning of Section Ex
Variable A : SType
Definition. We define
ex to be
λQ : A → prop ⇒ ∀P : prop , (∀x : A , Q x → P ) → P of type
(A → prop ) → prop .
End of Section Ex
Notation . We use
∃ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
ex .
Axiom. (
prop_ext ) We take the following as an axiom:
∀p q : prop , iff p q → p = q
Object . The name
In is a term of type
set → set → prop .
Notation . We use
∈ as an infix operator with priority 500 and no associativity corresponding to applying term
In . Furthermore, we may write
∀ x ∈ A , B to mean
∀ x : set, x ∈ A → B .
Definition. We define
Subq to be
λA B ⇒ ∀x ∈ A , x ∈ B of type
set → set → prop .
Notation . We use
⊆ as an infix operator with priority 500 and no associativity corresponding to applying term
Subq . Furthermore, we may write
∀ x ⊆ A , B to mean
∀ x : set, x ⊆ A → B .
Axiom. (
set_ext ) We take the following as an axiom:
∀X Y : set , X ⊆ Y → Y ⊆ X → X = Y
Axiom. (
In_ind ) We take the following as an axiom:
∀P : set → prop , (∀X : set , (∀x ∈ X , P x ) → P X ) → ∀X : set , P X
Notation . We use
∃ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
ex and handling ∈ or ⊆ ascriptions using
and .
Object . The name
Empty is a term of type
set .
Axiom. (
EmptyAx ) We take the following as an axiom:
Object . The name
⋃ is a term of type
set → set .
Axiom. (
UnionEq ) We take the following as an axiom:
∀X x, x ∈ ⋃ X ↔ ∃Y, x ∈ Y ∧ Y ∈ X
Object . The name
𝒫 is a term of type
set → set .
Axiom. (
PowerEq ) We take the following as an axiom:
∀X Y : set , Y ∈ 𝒫 X ↔ Y ⊆ X
Object . The name
Repl is a term of type
set → (set → set ) → set .
Notation .
{B | x ∈ A } is notation for
Repl A (λ x . B ).
Axiom. (
ReplEq ) We take the following as an axiom:
∀A : set , ∀F : set → set , ∀y : set , y ∈ {F x |x ∈ A } ↔ ∃x ∈ A , y = F x
Definition. We define
TransSet to be
λU : set ⇒ ∀x ∈ U , x ⊆ U of type
set → prop .
Definition. We define
Union_closed to be
λU : set ⇒ ∀X : set , X ∈ U → ⋃ X ∈ U of type
set → prop .
Definition. We define
Power_closed to be
λU : set ⇒ ∀X : set , X ∈ U → 𝒫 X ∈ U of type
set → prop .
Definition. We define
Repl_closed to be
λU : set ⇒ ∀X : set , X ∈ U → ∀F : set → set , (∀x : set , x ∈ X → F x ∈ U ) → {F x |x ∈ X } ∈ U of type
set → prop .
Object . The name
UnivOf is a term of type
set → set .
Axiom. (
UnivOf_In ) We take the following as an axiom:
Axiom. (
UnivOf_Min ) We take the following as an axiom:
Axiom. (
FalseE ) We take the following as an axiom:
Axiom. (
TrueI ) We take the following as an axiom:
Axiom. (
andI ) We take the following as an axiom:
∀A B : prop , A → B → A ∧ B
Axiom. (
andEL ) We take the following as an axiom:
∀A B : prop , A ∧ B → A
Axiom. (
andER ) We take the following as an axiom:
∀A B : prop , A ∧ B → B
Axiom. (
orIL ) We take the following as an axiom:
∀A B : prop , A → A ∨ B
Axiom. (
orIR ) We take the following as an axiom:
∀A B : prop , B → A ∨ B
Beginning of Section PropN
Variable P1 P2 P3 : prop
Axiom. (
and3I ) We take the following as an axiom:
P1 → P2 → P3 → P1 ∧ P2 ∧ P3
Axiom. (
and3E ) We take the following as an axiom:
P1 ∧ P2 ∧ P3 → (∀p : prop , (P1 → P2 → P3 → p ) → p )
Axiom. (
or3I1 ) We take the following as an axiom:
P1 → P1 ∨ P2 ∨ P3
Axiom. (
or3I2 ) We take the following as an axiom:
P2 → P1 ∨ P2 ∨ P3
Axiom. (
or3I3 ) We take the following as an axiom:
P3 → P1 ∨ P2 ∨ P3
Axiom. (
or3E ) We take the following as an axiom:
P1 ∨ P2 ∨ P3 → (∀p : prop , (P1 → p ) → (P2 → p ) → (P3 → p ) → p )
Variable P4 : prop
Axiom. (
and4I ) We take the following as an axiom:
P1 → P2 → P3 → P4 → P1 ∧ P2 ∧ P3 ∧ P4
Variable P5 : prop
Axiom. (
and5I ) We take the following as an axiom:
P1 → P2 → P3 → P4 → P5 → P1 ∧ P2 ∧ P3 ∧ P4 ∧ P5
End of Section PropN
Axiom. (
not_or_and_demorgan ) We take the following as an axiom:
∀A B : prop , ¬ (A ∨ B ) → ¬ A ∧ ¬ B
Axiom. (
not_ex_all_demorgan_i ) We take the following as an axiom:
∀P : set → prop , (¬ ∃x, P x ) → ∀x, ¬ P x
Axiom. (
iffI ) We take the following as an axiom:
∀A B : prop , (A → B ) → (B → A ) → (A ↔ B )
Axiom. (
iffEL ) We take the following as an axiom:
∀A B : prop , (A ↔ B ) → A → B
Axiom. (
iffER ) We take the following as an axiom:
∀A B : prop , (A ↔ B ) → B → A
Axiom. (
iff_refl ) We take the following as an axiom:
∀A : prop , A ↔ A
Axiom. (
iff_sym ) We take the following as an axiom:
∀A B : prop , (A ↔ B ) → (B ↔ A )
Axiom. (
iff_trans ) We take the following as an axiom:
∀A B C : prop , (A ↔ B ) → (B ↔ C ) → (A ↔ C )
Axiom. (
eq_i_tra ) We take the following as an axiom:
∀x y z, x = y → y = z → x = z
Axiom. (
f_eq_i ) We take the following as an axiom:
∀f : set → set , ∀x y, x = y → f x = f y
Axiom. (
neq_i_sym ) We take the following as an axiom:
∀x y, x ≠ y → y ≠ x
Definition. We define
nIn to be
λx X ⇒ ¬ In x X of type
set → set → prop .
Notation . We use
∉ as an infix operator with priority 502 and no associativity corresponding to applying term
nIn .
Axiom. (
Eps_i_ex ) We take the following as an axiom:
∀P : set → prop , (∃x, P x ) → P (Eps_i P )
Axiom. (
pred_ext ) We take the following as an axiom:
∀P Q : set → prop , (∀x, P x ↔ Q x ) → P = Q
Axiom. (
prop_ext_2 ) We take the following as an axiom:
∀p q : prop , (p → q ) → (q → p ) → p = q
Axiom. (
Subq_ref ) We take the following as an axiom:
∀X : set , X ⊆ X
Axiom. (
Subq_tra ) We take the following as an axiom:
∀X Y Z : set , X ⊆ Y → Y ⊆ Z → X ⊆ Z
Axiom. (
Subq_contra ) We take the following as an axiom:
∀X Y z : set , X ⊆ Y → z ∉ Y → z ∉ X
Axiom. (
EmptyE ) We take the following as an axiom:
Axiom. (
Subq_Empty ) We take the following as an axiom:
Axiom. (
Empty_eq ) We take the following as an axiom:
∀X : set , (∀x, x ∉ X ) → X = Empty
Axiom. (
UnionI ) We take the following as an axiom:
∀X x Y : set , x ∈ Y → Y ∈ X → x ∈ ⋃ X
Axiom. (
UnionE ) We take the following as an axiom:
∀X x : set , x ∈ ⋃ X → ∃Y : set , x ∈ Y ∧ Y ∈ X
Axiom. (
UnionE_impred ) We take the following as an axiom:
∀X x : set , x ∈ ⋃ X → ∀p : prop , (∀Y : set , x ∈ Y → Y ∈ X → p ) → p
Axiom. (
PowerI ) We take the following as an axiom:
∀X Y : set , Y ⊆ X → Y ∈ 𝒫 X
Axiom. (
PowerE ) We take the following as an axiom:
∀X Y : set , Y ∈ 𝒫 X → Y ⊆ X
Axiom. (
xm ) We take the following as an axiom:
∀P : prop , P ∨ ¬ P
Axiom. (
dneg ) We take the following as an axiom:
∀P : prop , ¬ ¬ P → P
Axiom. (
not_all_ex_demorgan_i ) We take the following as an axiom:
∀P : set → prop , ¬ (∀x, P x ) → ∃x, ¬ P x
Axiom. (
eq_or_nand ) We take the following as an axiom:
or = (λx y : prop ⇒ ¬ (¬ x ∧ ¬ y ) )
Object . The name
exactly1of2 is a term of type
prop → prop → prop .
Axiom. (
exactly1of2_E ) We take the following as an axiom:
∀A B : prop , exactly1of2 A B → ∀p : prop , (A → ¬ B → p ) → (¬ A → B → p ) → p
Axiom. (
ReplI ) We take the following as an axiom:
∀A : set , ∀F : set → set , ∀x : set , x ∈ A → F x ∈ {F x |x ∈ A }
Axiom. (
ReplE ) We take the following as an axiom:
∀A : set , ∀F : set → set , ∀y : set , y ∈ {F x |x ∈ A } → ∃x ∈ A , y = F x
Axiom. (
ReplE_impred ) We take the following as an axiom:
∀A : set , ∀F : set → set , ∀y : set , y ∈ {F x |x ∈ A } → ∀p : prop , (∀x : set , x ∈ A → y = F x → p ) → p
Axiom. (
ReplE' ) We take the following as an axiom:
∀X, ∀f : set → set , ∀p : set → prop , (∀x ∈ X , p (f x ) ) → ∀y ∈ {f x |x ∈ X } , p y
Axiom. (
Repl_Empty ) We take the following as an axiom:
Axiom. (
ReplEq_ext_sub ) We take the following as an axiom:
∀X, ∀F G : set → set , (∀x ∈ X , F x = G x ) → {F x |x ∈ X } ⊆ {G x |x ∈ X }
Axiom. (
ReplEq_ext ) We take the following as an axiom:
∀X, ∀F G : set → set , (∀x ∈ X , F x = G x ) → {F x |x ∈ X } = {G x |x ∈ X }
Axiom. (
Repl_inv_eq ) We take the following as an axiom:
∀P : set → prop , ∀f g : set → set , (∀x, P x → g (f x ) = x ) → ∀X, (∀x ∈ X , P x ) → {g y |y ∈ {f x |x ∈ X } } = X
Axiom. (
Repl_invol_eq ) We take the following as an axiom:
∀P : set → prop , ∀f : set → set , (∀x, P x → f (f x ) = x ) → ∀X, (∀x ∈ X , P x ) → {f y |y ∈ {f x |x ∈ X } } = X
Object . The name
If_i is a term of type
prop → set → set → set .
Notation . if cond then T else E is notation corresponding to If_i type cond T E where type is the inferred type of T .
Axiom. (
If_i_correct ) We take the following as an axiom:
∀p : prop , ∀x y : set , p ∧ (if p then x else y ) = x ∨ ¬ p ∧ (if p then x else y ) = y
Axiom. (
If_i_0 ) We take the following as an axiom:
∀p : prop , ∀x y : set , ¬ p → (if p then x else y ) = y
Axiom. (
If_i_1 ) We take the following as an axiom:
∀p : prop , ∀x y : set , p → (if p then x else y ) = x
Axiom. (
If_i_or ) We take the following as an axiom:
∀p : prop , ∀x y : set , (if p then x else y ) = x ∨ (if p then x else y ) = y
Object . The name
UPair is a term of type
set → set → set .
Notation .
{x ,y } is notation for
UPair x y .
Axiom. (
UPairE ) We take the following as an axiom:
∀x y z : set , x ∈ {y ,z } → x = y ∨ x = z
Axiom. (
UPairI1 ) We take the following as an axiom:
∀y z : set , y ∈ {y ,z }
Axiom. (
UPairI2 ) We take the following as an axiom:
∀y z : set , z ∈ {y ,z }
Object . The name
Sing is a term of type
set → set .
Notation .
{x } is notation for
Sing x .
Axiom. (
SingI ) We take the following as an axiom:
∀x : set , x ∈ {x }
Axiom. (
SingE ) We take the following as an axiom:
∀x y : set , y ∈ {x } → y = x
Object . The name
binunion is a term of type
set → set → set .
Notation . We use
∪ as an infix operator with priority 345 and which associates to the left corresponding to applying term
binunion .
Axiom. (
binunionI1 ) We take the following as an axiom:
∀X Y z : set , z ∈ X → z ∈ X ∪ Y
Axiom. (
binunionI2 ) We take the following as an axiom:
∀X Y z : set , z ∈ Y → z ∈ X ∪ Y
Axiom. (
binunionE ) We take the following as an axiom:
∀X Y z : set , z ∈ X ∪ Y → z ∈ X ∨ z ∈ Y
Axiom. (
binunionE' ) We take the following as an axiom:
∀X Y z, ∀p : prop , (z ∈ X → p ) → (z ∈ Y → p ) → (z ∈ X ∪ Y → p )
Axiom. (
binunion_asso ) We take the following as an axiom:
∀X Y Z : set , X ∪ (Y ∪ Z ) = (X ∪ Y ) ∪ Z
Axiom. (
binunion_com_Subq ) We take the following as an axiom:
∀X Y : set , X ∪ Y ⊆ Y ∪ X
Axiom. (
binunion_com ) We take the following as an axiom:
∀X Y : set , X ∪ Y = Y ∪ X
Axiom. (
binunion_Subq_1 ) We take the following as an axiom:
∀X Y : set , X ⊆ X ∪ Y
Axiom. (
binunion_Subq_2 ) We take the following as an axiom:
∀X Y : set , Y ⊆ X ∪ Y
Axiom. (
binunion_Subq_min ) We take the following as an axiom:
∀X Y Z : set , X ⊆ Z → Y ⊆ Z → X ∪ Y ⊆ Z
Axiom. (
Subq_binunion_eq ) We take the following as an axiom:
∀X Y, (X ⊆ Y ) = (X ∪ Y = Y )
Definition. We define
SetAdjoin to be
λX y ⇒ X ∪ {y } of type
set → set → set .
Notation . We now use the set enumeration notation
{...,...,...} in general. If 0 elements are given, then
Empty is used to form the corresponding term. If 1 element is given, then
Sing is used to form the corresponding term. If 2 elements are given, then
UPair is used to form the corresponding term. If more than elements are given, then
SetAdjoin is used to reduce to the case with one fewer elements.
Object . The name
famunion is a term of type
set → (set → set ) → set .
Notation . We use
⋃ x [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
famunion .
Axiom. (
famunionI ) We take the following as an axiom:
∀X : set , ∀F : (set → set ) , ∀x y : set , x ∈ X → y ∈ F x → y ∈ ⋃x ∈ X F x
Axiom. (
famunionE ) We take the following as an axiom:
∀X : set , ∀F : (set → set ) , ∀y : set , y ∈ (⋃x ∈ X F x ) → ∃x ∈ X , y ∈ F x
Axiom. (
famunionE_impred ) We take the following as an axiom:
∀X : set , ∀F : (set → set ) , ∀y : set , y ∈ (⋃x ∈ X F x ) → ∀p : prop , (∀x, x ∈ X → y ∈ F x → p ) → p
Beginning of Section SepSec
Variable X : set
Variable P : set → prop
Let z : set ≝ Eps_i (λz ⇒ z ∈ X ∧ P z )
Let F : set → set ≝ λx ⇒ if P x then x else z
Object . The name
Sep is a term of type
set .
End of Section SepSec
Notation .
{x ∈ A | B } is notation for
Sep A (λ x . B ).
Axiom. (
SepI ) We take the following as an axiom:
∀X : set , ∀P : (set → prop ) , ∀x : set , x ∈ X → P x → x ∈ {x ∈ X |P x }
Axiom. (
SepE ) We take the following as an axiom:
∀X : set , ∀P : (set → prop ) , ∀x : set , x ∈ {x ∈ X |P x } → x ∈ X ∧ P x
Axiom. (
SepE1 ) We take the following as an axiom:
∀X : set , ∀P : (set → prop ) , ∀x : set , x ∈ {x ∈ X |P x } → x ∈ X
Axiom. (
SepE2 ) We take the following as an axiom:
∀X : set , ∀P : (set → prop ) , ∀x : set , x ∈ {x ∈ X |P x } → P x
Axiom. (
Sep_Subq ) We take the following as an axiom:
∀X : set , ∀P : set → prop , {x ∈ X |P x } ⊆ X
Axiom. (
Sep_In_Power ) We take the following as an axiom:
∀X : set , ∀P : set → prop , {x ∈ X |P x } ∈ 𝒫 X
Object . The name
ReplSep is a term of type
set → (set → prop ) → (set → set ) → set .
Notation .
{B | x ∈ A , C } is notation for
ReplSep A (λ x . C ) (λ x . B ).
Axiom. (
ReplSepI ) We take the following as an axiom:
∀X : set , ∀P : set → prop , ∀F : set → set , ∀x : set , x ∈ X → P x → F x ∈ {F x |x ∈ X , P x }
Axiom. (
ReplSepE ) We take the following as an axiom:
∀X : set , ∀P : set → prop , ∀F : set → set , ∀y : set , y ∈ {F x |x ∈ X , P x } → ∃x : set , x ∈ X ∧ P x ∧ y = F x
Axiom. (
ReplSepE_impred ) We take the following as an axiom:
∀X : set , ∀P : set → prop , ∀F : set → set , ∀y : set , y ∈ {F x |x ∈ X , P x } → ∀p : prop , (∀x ∈ X , P x → y = F x → p ) → p
Object . The name
binintersect is a term of type
set → set → set .
Notation . We use
∩ as an infix operator with priority 340 and which associates to the left corresponding to applying term
binintersect .
Axiom. (
binintersectI ) We take the following as an axiom:
∀X Y z, z ∈ X → z ∈ Y → z ∈ X ∩ Y
Axiom. (
binintersectE ) We take the following as an axiom:
∀X Y z, z ∈ X ∩ Y → z ∈ X ∧ z ∈ Y
Axiom. (
binintersectE1 ) We take the following as an axiom:
∀X Y z, z ∈ X ∩ Y → z ∈ X
Axiom. (
binintersectE2 ) We take the following as an axiom:
∀X Y z, z ∈ X ∩ Y → z ∈ Y
Axiom. (
binintersect_Subq_max ) We take the following as an axiom:
∀X Y Z : set , Z ⊆ X → Z ⊆ Y → Z ⊆ X ∩ Y
Axiom. (
binintersect_com ) We take the following as an axiom:
∀X Y : set , X ∩ Y = Y ∩ X
Object . The name
setminus is a term of type
set → set → set .
Notation . We use
∖ as an infix operator with priority 350 and no associativity corresponding to applying term
setminus .
Axiom. (
setminusI ) We take the following as an axiom:
∀X Y z, (z ∈ X ) → (z ∉ Y ) → z ∈ X ∖ Y
Axiom. (
setminusE ) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y ) → z ∈ X ∧ z ∉ Y
Axiom. (
setminusE1 ) We take the following as an axiom:
∀X Y z, (z ∈ X ∖ Y ) → z ∈ X
Axiom. (
setminus_Subq ) We take the following as an axiom:
∀X Y : set , X ∖ Y ⊆ X
Axiom. (
setminus_Subq_contra ) We take the following as an axiom:
∀X Y Z : set , Z ⊆ Y → X ∖ Y ⊆ X ∖ Z
Axiom. (
In_irref ) We take the following as an axiom:
∀x, x ∉ x
Axiom. (
In_no2cycle ) We take the following as an axiom:
∀x y, x ∈ y → y ∈ x → False
Object . The name
ordsucc is a term of type
set → set .
Axiom. (
ordsuccI1 ) We take the following as an axiom:
Axiom. (
ordsuccI2 ) We take the following as an axiom:
Axiom. (
ordsuccE ) We take the following as an axiom:
∀x y : set , y ∈ ordsucc x → y ∈ x ∨ y = x
Notation . Natural numbers 0,1,2,... are notation for the terms formed using
Empty as 0 and forming successors with
ordsucc .
Axiom. (
ordsucc_inj ) We take the following as an axiom:
Axiom. (
In_0_1 ) We take the following as an axiom:
0 ∈ 1
Axiom. (
In_0_2 ) We take the following as an axiom:
0 ∈ 2
Axiom. (
In_1_2 ) We take the following as an axiom:
1 ∈ 2
Definition. We define
nat_p to be
λn : set ⇒ ∀p : set → prop , p 0 → (∀x : set , p x → p (ordsucc x ) ) → p n of type
set → prop .
Axiom. (
nat_0 ) We take the following as an axiom:
Axiom. (
nat_ordsucc ) We take the following as an axiom:
Axiom. (
nat_1 ) We take the following as an axiom:
Axiom. (
nat_2 ) We take the following as an axiom:
Axiom. (
nat_ind ) We take the following as an axiom:
Axiom. (
nat_inv ) We take the following as an axiom:
Axiom. (
nat_complete_ind ) We take the following as an axiom:
∀p : set → prop , (∀n, nat_p n → (∀m ∈ n , p m ) → p n ) → ∀n, nat_p n → p n
Axiom. (
nat_p_trans ) We take the following as an axiom:
Axiom. (
nat_trans ) We take the following as an axiom:
∀n, nat_p n → ∀m ∈ n , m ⊆ n
Axiom. (
cases_1 ) We take the following as an axiom:
∀i ∈ 1 , ∀p : set → prop , p 0 → p i
Axiom. (
cases_2 ) We take the following as an axiom:
∀i ∈ 2 , ∀p : set → prop , p 0 → p 1 → p i
Axiom. (
cases_3 ) We take the following as an axiom:
∀i ∈ 3 , ∀p : set → prop , p 0 → p 1 → p 2 → p i
Axiom. (
neq_0_1 ) We take the following as an axiom:
0 ≠ 1
Axiom. (
neq_1_0 ) We take the following as an axiom:
1 ≠ 0
Axiom. (
neq_0_2 ) We take the following as an axiom:
0 ≠ 2
Axiom. (
neq_2_0 ) We take the following as an axiom:
2 ≠ 0
Axiom. (
neq_1_2 ) We take the following as an axiom:
1 ≠ 2
Axiom. (
ZF_closed_E ) We take the following as an axiom:
Axiom. (
ZF_Repl_closed ) We take the following as an axiom:
∀U, ZF_closed U → ∀X ∈ U , ∀F : set → set , (∀x ∈ X , F x ∈ U ) → {F x |x ∈ X } ∈ U
Object . The name
ω is a term of type
set .
Axiom. (
omega_nat_p ) We take the following as an axiom:
Axiom. (
nat_p_omega ) We take the following as an axiom:
Definition. We define
ordinal to be
λalpha : set ⇒ TransSet alpha ∧ ∀beta ∈ alpha , TransSet beta of type
set → prop .
Axiom. (
ordinal_1 ) We take the following as an axiom:
Axiom. (
ordinal_2 ) We take the following as an axiom:
Axiom. (
ordinal_ind ) We take the following as an axiom:
∀p : set → prop , (∀alpha, ordinal alpha → (∀beta ∈ alpha , p beta ) → p alpha ) → ∀alpha, ordinal alpha → p alpha
Axiom. (
least_ordinal_ex ) We take the following as an axiom:
∀p : set → prop , (∃alpha, ordinal alpha ∧ p alpha ) → ∃alpha, ordinal alpha ∧ p alpha ∧ ∀beta ∈ alpha , ¬ p beta
Definition. We define
inj to be
λX Y f ⇒ (∀u ∈ X , f u ∈ Y ) ∧ (∀u v ∈ X , f u = f v → u = v ) of type
set → set → (set → set ) → prop .
Definition. We define
bij to be
λX Y f ⇒ (∀u ∈ X , f u ∈ Y ) ∧ (∀u v ∈ X , f u = f v → u = v ) ∧ (∀w ∈ Y , ∃u ∈ X , f u = w ) of type
set → set → (set → set ) → prop .
Axiom. (
bijI ) We take the following as an axiom:
∀X Y, ∀f : set → set , (∀u ∈ X , f u ∈ Y ) → (∀u v ∈ X , f u = f v → u = v ) → (∀w ∈ Y , ∃u ∈ X , f u = w ) → bij X Y f
Axiom. (
bijE ) We take the following as an axiom:
∀X Y, ∀f : set → set , bij X Y f → ∀p : prop , ((∀u ∈ X , f u ∈ Y ) → (∀u v ∈ X , f u = f v → u = v ) → (∀w ∈ Y , ∃u ∈ X , f u = w ) → p ) → p
Object . The name
inv is a term of type
set → (set → set ) → set → set .
Axiom. (
surj_rinv ) We take the following as an axiom:
∀X Y, ∀f : set → set , (∀w ∈ Y , ∃u ∈ X , f u = w ) → ∀y ∈ Y , inv X f y ∈ X ∧ f (inv X f y ) = y
Axiom. (
inj_linv ) We take the following as an axiom:
∀X, ∀f : set → set , (∀u v ∈ X , f u = f v → u = v ) → ∀x ∈ X , inv X f (f x ) = x
Axiom. (
bij_inv ) We take the following as an axiom:
∀X Y, ∀f : set → set , bij X Y f → bij Y X (inv X f )
Axiom. (
bij_id ) We take the following as an axiom:
Axiom. (
bij_comp ) We take the following as an axiom:
∀X Y Z : set , ∀f g : set → set , bij X Y f → bij Y Z g → bij X Z (λx ⇒ g (f x ) )
Definition. We define
equip to be
λX Y : set ⇒ ∃f : set → set , bij X Y f of type
set → set → prop .
Axiom. (
equip_ref ) We take the following as an axiom:
Axiom. (
equip_sym ) We take the following as an axiom:
Axiom. (
equip_tra ) We take the following as an axiom:
Beginning of Section SchroederBernstein
Axiom. (
KnasterTarski_set ) We take the following as an axiom:
∀A, ∀F : set → set , (∀U ∈ 𝒫 A , F U ∈ 𝒫 A ) → (∀U V ∈ 𝒫 A , U ⊆ V → F U ⊆ F V ) → ∃Y ∈ 𝒫 A , F Y = Y
Axiom. (
image_In_Power ) We take the following as an axiom:
∀A B, ∀f : set → set , (∀x ∈ A , f x ∈ B ) → ∀U ∈ 𝒫 A , {f x |x ∈ U } ∈ 𝒫 B
Axiom. (
image_monotone ) We take the following as an axiom:
∀f : set → set , ∀U V, U ⊆ V → {f x |x ∈ U } ⊆ {f x |x ∈ V }
End of Section SchroederBernstein
Beginning of Section PigeonHole
Axiom. (
PigeonHole_nat_bij ) We take the following as an axiom:
∀n, nat_p n → ∀f : set → set , (∀i ∈ n , f i ∈ n ) → (∀i j ∈ n , f i = f j → i = j ) → bij n n f
End of Section PigeonHole
Definition. We define
finite to be
λX ⇒ ∃n ∈ ω , equip X n of type
set → prop .
Axiom. (
finite_ind ) We take the following as an axiom:
∀p : set → prop , p Empty → (∀X y, finite X → y ∉ X → p X → p (X ∪ {y } ) ) → ∀X, finite X → p X
Axiom. (
Subq_finite ) We take the following as an axiom:
Axiom. (
exandE_i ) We take the following as an axiom:
∀P Q : set → prop , (∃x, P x ∧ Q x ) → ∀r : prop , (∀x, P x → Q x → r ) → r
Axiom. (
exandE_ii ) We take the following as an axiom:
∀P Q : (set → set ) → prop , (∃x : set → set , P x ∧ Q x ) → ∀p : prop , (∀x : set → set , P x → Q x → p ) → p
Axiom. (
exandE_iii ) We take the following as an axiom:
∀P Q : (set → set → set ) → prop , (∃x : set → set → set , P x ∧ Q x ) → ∀p : prop , (∀x : set → set → set , P x → Q x → p ) → p
Axiom. (
exandE_iiii ) We take the following as an axiom:
∀P Q : (set → set → set → set ) → prop , (∃x : set → set → set → set , P x ∧ Q x ) → ∀p : prop , (∀x : set → set → set → set , P x → Q x → p ) → p
Beginning of Section Descr_ii
Variable P : (set → set ) → prop
Object . The name
Descr_ii is a term of type
set → set .
Hypothesis Pex : ∃f : set → set , P f
Hypothesis Puniq : ∀f g : set → set , P f → P g → f = g
End of Section Descr_ii
Beginning of Section Descr_iii
Variable P : (set → set → set ) → prop
Object . The name
Descr_iii is a term of type
set → set → set .
Hypothesis Pex : ∃f : set → set → set , P f
Hypothesis Puniq : ∀f g : set → set → set , P f → P g → f = g
End of Section Descr_iii
Beginning of Section Descr_Vo1
Variable P : Vo 1 → prop
Object . The name
Descr_Vo1 is a term of type
Vo 1 .
Hypothesis Pex : ∃f : Vo 1 , P f
Hypothesis Puniq : ∀f g : Vo 1 , P f → P g → f = g
End of Section Descr_Vo1
Beginning of Section If_ii
Variable p : prop
Variable f g : set → set
Object . The name
If_ii is a term of type
set → set .
Axiom. (
If_ii_1 ) We take the following as an axiom:
Axiom. (
If_ii_0 ) We take the following as an axiom:
End of Section If_ii
Beginning of Section If_iii
Variable p : prop
Variable f g : set → set → set
Object . The name
If_iii is a term of type
set → set → set .
Axiom. (
If_iii_1 ) We take the following as an axiom:
Axiom. (
If_iii_0 ) We take the following as an axiom:
End of Section If_iii
Beginning of Section EpsilonRec_i
Variable F : set → (set → set ) → set
Object . The name
In_rec_i is a term of type
set → set .
Hypothesis Fr : ∀X : set , ∀g h : set → set , (∀x ∈ X , g x = h x ) → F X g = F X h
Axiom. (
In_rec_i_eq ) We take the following as an axiom:
End of Section EpsilonRec_i
Beginning of Section EpsilonRec_ii
Variable F : set → (set → (set → set ) ) → (set → set )
Object . The name
In_rec_ii is a term of type
set → (set → set ) .
Hypothesis Fr : ∀X : set , ∀g h : set → (set → set ) , (∀x ∈ X , g x = h x ) → F X g = F X h
End of Section EpsilonRec_ii
Beginning of Section EpsilonRec_iii
Variable F : set → (set → (set → set → set ) ) → (set → set → set )
Object . The name
In_rec_iii is a term of type
set → (set → set → set ) .
Hypothesis Fr : ∀X : set , ∀g h : set → (set → set → set ) , (∀x ∈ X , g x = h x ) → F X g = F X h
End of Section EpsilonRec_iii
Beginning of Section NatRec
Variable z : set
Variable f : set → set → set
Let F : set → (set → set ) → set ≝ λn g ⇒ if ⋃ n ∈ n then f (⋃ n ) (g (⋃ n ) ) else z
Axiom. (
nat_primrec_r ) We take the following as an axiom:
∀X : set , ∀g h : set → set , (∀x ∈ X , g x = h x ) → F X g = F X h
End of Section NatRec
Beginning of Section NatArith
Notation . We use
+ as an infix operator with priority 360 and which associates to the right corresponding to applying term
add_nat .
Axiom. (
add_nat_0R ) We take the following as an axiom:
∀n : set , n + 0 = n
Axiom. (
add_nat_SR ) We take the following as an axiom:
Axiom. (
add_nat_p ) We take the following as an axiom:
Axiom. (
add_nat_1_1_2 ) We take the following as an axiom:
1 + 1 = 2
Definition. We define
mul_nat to be
λn m : set ⇒ nat_primrec 0 (λ_ r ⇒ n + r ) m of type
set → set → set .
Notation . We use
* as an infix operator with priority 355 and which associates to the right corresponding to applying term
mul_nat .
Axiom. (
mul_nat_0R ) We take the following as an axiom:
∀n : set , n * 0 = 0
Axiom. (
mul_nat_SR ) We take the following as an axiom:
Axiom. (
mul_nat_p ) We take the following as an axiom:
End of Section NatArith
Definition. We define
Inj1 to be
In_rec_i (λX f ⇒ {0 } ∪ {f x |x ∈ X } ) of type
set → set .
Axiom. (
Inj1_eq ) We take the following as an axiom:
Axiom. (
Inj1I1 ) We take the following as an axiom:
Axiom. (
Inj1I2 ) We take the following as an axiom:
Axiom. (
Inj1E ) We take the following as an axiom:
∀X y : set , y ∈ Inj1 X → y = 0 ∨ ∃x ∈ X , y = Inj1 x
Axiom. (
Inj1NE1 ) We take the following as an axiom:
Axiom. (
Inj1NE2 ) We take the following as an axiom:
Definition. We define
Inj0 to be
λX ⇒ {Inj1 x |x ∈ X } of type
set → set .
Axiom. (
Inj0I ) We take the following as an axiom:
Axiom. (
Inj0E ) We take the following as an axiom:
∀X y : set , y ∈ Inj0 X → ∃x : set , x ∈ X ∧ y = Inj1 x
Definition. We define
Unj to be
In_rec_i (λX f ⇒ {f x |x ∈ X ∖ {0 } } ) of type
set → set .
Axiom. (
Unj_eq ) We take the following as an axiom:
∀X : set , Unj X = {Unj x |x ∈ X ∖ {0 } }
Axiom. (
Unj_Inj1_eq ) We take the following as an axiom:
Axiom. (
Inj1_inj ) We take the following as an axiom:
Axiom. (
Unj_Inj0_eq ) We take the following as an axiom:
Axiom. (
Inj0_inj ) We take the following as an axiom:
Axiom. (
Inj0_0 ) We take the following as an axiom:
Definition. We define
setsum to be
λX Y ⇒ {Inj0 x |x ∈ X } ∪ {Inj1 y |y ∈ Y } of type
set → set → set .
Notation . We use
+ as an infix operator with priority 450 and which associates to the left corresponding to applying term
setsum .
Axiom. (
Inj0_setsum ) We take the following as an axiom:
∀X Y x : set , x ∈ X → Inj0 x ∈ X + Y
Axiom. (
Inj1_setsum ) We take the following as an axiom:
∀X Y y : set , y ∈ Y → Inj1 y ∈ X + Y
Axiom. (
setsum_Inj_inv ) We take the following as an axiom:
∀X Y z : set , z ∈ X + Y → (∃x ∈ X , z = Inj0 x ) ∨ (∃y ∈ Y , z = Inj1 y )
Axiom. (
Subq_1_Sing0 ) We take the following as an axiom:
1 ⊆ {0 }
Axiom. (
setsum_0_0 ) We take the following as an axiom:
0 + 0 = 0
Axiom. (
setsum_1_0_1 ) We take the following as an axiom:
1 + 0 = 1
Axiom. (
setsum_1_1_2 ) We take the following as an axiom:
1 + 1 = 2
Beginning of Section pair_setsum
Definition. We define
proj0 to be
λZ ⇒ {Unj z |z ∈ Z , ∃x : set , Inj0 x = z } of type
set → set .
Definition. We define
proj1 to be
λZ ⇒ {Unj z |z ∈ Z , ∃y : set , Inj1 y = z } of type
set → set .
Axiom. (
pairI0 ) We take the following as an axiom:
∀X Y x, x ∈ X → pair 0 x ∈ pair X Y
Axiom. (
pairI1 ) We take the following as an axiom:
∀X Y y, y ∈ Y → pair 1 y ∈ pair X Y
Axiom. (
pairE ) We take the following as an axiom:
∀X Y z, z ∈ pair X Y → (∃x ∈ X , z = pair 0 x ) ∨ (∃y ∈ Y , z = pair 1 y )
Axiom. (
pairE0 ) We take the following as an axiom:
∀X Y x, pair 0 x ∈ pair X Y → x ∈ X
Axiom. (
pairE1 ) We take the following as an axiom:
∀X Y y, pair 1 y ∈ pair X Y → y ∈ Y
Axiom. (
proj0I ) We take the following as an axiom:
∀w u : set , pair 0 u ∈ w → u ∈ proj0 w
Axiom. (
proj0E ) We take the following as an axiom:
∀w u : set , u ∈ proj0 w → pair 0 u ∈ w
Axiom. (
proj1I ) We take the following as an axiom:
∀w u : set , pair 1 u ∈ w → u ∈ proj1 w
Axiom. (
proj1E ) We take the following as an axiom:
∀w u : set , u ∈ proj1 w → pair 1 u ∈ w
Axiom. (
proj0_pair_eq ) We take the following as an axiom:
∀X Y : set , proj0 (pair X Y ) = X
Axiom. (
proj1_pair_eq ) We take the following as an axiom:
∀X Y : set , proj1 (pair X Y ) = Y
Definition. We define
Sigma to be
λX Y ⇒ ⋃x ∈ X {pair x y |y ∈ Y x } of type
set → (set → set ) → set .
Notation . We use
∑ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Sigma .
Axiom. (
pair_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀x ∈ X , ∀y ∈ Y x , pair x y ∈ ∑x ∈ X , Y x
Axiom. (
proj_Sigma_eta ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀z ∈ (∑x ∈ X , Y x ) , pair (proj0 z ) (proj1 z ) = z
Axiom. (
proj0_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀z : set , z ∈ (∑x ∈ X , Y x ) → proj0 z ∈ X
Axiom. (
proj1_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀z : set , z ∈ (∑x ∈ X , Y x ) → proj1 z ∈ Y (proj0 z )
Axiom. (
pair_Sigma_E1 ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀x y : set , pair x y ∈ (∑x ∈ X , Y x ) → y ∈ Y x
Axiom. (
Sigma_E ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀z : set , z ∈ (∑x ∈ X , Y x ) → ∃x ∈ X , ∃y ∈ Y x , z = pair x y
Definition. We define
setprod to be
λX Y : set ⇒ ∑x ∈ X , Y of type
set → set → set .
Notation . We use
⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term
setprod .
Let lam : set → (set → set ) → set ≝ Sigma
Definition. We define
ap to be
λf x ⇒ {proj1 z |z ∈ f , ∃y : set , z = pair x y } of type
set → set → set .
Notation . When
x is a set, a term
x y is notation for
ap x y .
Notation .
λ x ∈ A ⇒ B is notation for the set
Sigma A (λ x : set ⇒ B ).
Axiom. (
lamI ) We take the following as an axiom:
∀X : set , ∀F : set → set , ∀x ∈ X , ∀y ∈ F x , pair x y ∈ λx ∈ X ⇒ F x
Axiom. (
lamE ) We take the following as an axiom:
∀X : set , ∀F : set → set , ∀z : set , z ∈ (λx ∈ X ⇒ F x ) → ∃x ∈ X , ∃y ∈ F x , z = pair x y
Axiom. (
apI ) We take the following as an axiom:
∀f x y, pair x y ∈ f → y ∈ f x
Axiom. (
apE ) We take the following as an axiom:
∀f x y, y ∈ f x → pair x y ∈ f
Axiom. (
beta ) We take the following as an axiom:
∀X : set , ∀F : set → set , ∀x : set , x ∈ X → (λx ∈ X ⇒ F x ) x = F x
Axiom. (
proj0_ap_0 ) We take the following as an axiom:
Axiom. (
proj1_ap_1 ) We take the following as an axiom:
Axiom. (
pair_ap_0 ) We take the following as an axiom:
∀x y : set , (pair x y ) 0 = x
Axiom. (
pair_ap_1 ) We take the following as an axiom:
∀x y : set , (pair x y ) 1 = y
Axiom. (
ap0_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀z : set , z ∈ (∑x ∈ X , Y x ) → (z 0 ) ∈ X
Axiom. (
ap1_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀z : set , z ∈ (∑x ∈ X , Y x ) → (z 1 ) ∈ (Y (z 0 ) )
Definition. We define
pair_p to be
λu : set ⇒ pair (u 0 ) (u 1 ) = u of type
set → prop .
Axiom. (
pair_p_I ) We take the following as an axiom:
Axiom. (
tuple_pair ) We take the following as an axiom:
∀x y : set , pair x y = (x ,y )
Definition. We define
Pi to be
λX Y ⇒ {f ∈ 𝒫 (∑x ∈ X , ⋃ (Y x ) ) |∀x ∈ X , f x ∈ Y x } of type
set → (set → set ) → set .
Notation . We use
∏ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Pi .
Axiom. (
PiI ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀f : set , (∀u ∈ f , pair_p u ∧ u 0 ∈ X ) → (∀x ∈ X , f x ∈ Y x ) → f ∈ ∏x ∈ X , Y x
Axiom. (
lam_Pi ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀F : set → set , (∀x ∈ X , F x ∈ Y x ) → (λx ∈ X ⇒ F x ) ∈ (∏x ∈ X , Y x )
Axiom. (
ap_Pi ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀f : set , ∀x : set , f ∈ (∏x ∈ X , Y x ) → x ∈ X → f x ∈ Y x
Definition. We define
setexp to be
λX Y : set ⇒ ∏y ∈ Y , X of type
set → set → set .
Notation . We use
:^: as an infix operator with priority 430 and which associates to the left corresponding to applying term
setexp .
Axiom. (
pair_tuple_fun ) We take the following as an axiom:
pair = (λx y ⇒ (x ,y ) )
Axiom. (
lamI2 ) We take the following as an axiom:
∀X, ∀F : set → set , ∀x ∈ X , ∀y ∈ F x , (x ,y ) ∈ λx ∈ X ⇒ F x
Beginning of Section Tuples
Variable x0 x1 : set
Axiom. (
tuple_2_0_eq ) We take the following as an axiom:
(x0 ,x1 ) 0 = x0
Axiom. (
tuple_2_1_eq ) We take the following as an axiom:
(x0 ,x1 ) 1 = x1
End of Section Tuples
Axiom. (
ReplEq_setprod_ext ) We take the following as an axiom:
∀X Y, ∀F G : set → set → set , (∀x ∈ X , ∀y ∈ Y , F x y = G x y ) → {F (w 0 ) (w 1 ) |w ∈ X ⨯ Y } = {G (w 0 ) (w 1 ) |w ∈ X ⨯ Y }
Axiom. (
tuple_2_Sigma ) We take the following as an axiom:
∀X : set , ∀Y : set → set , ∀x ∈ X , ∀y ∈ Y x , (x ,y ) ∈ ∑x ∈ X , Y x
Axiom. (
tuple_2_setprod ) We take the following as an axiom:
∀X : set , ∀Y : set , ∀x ∈ X , ∀y ∈ Y , (x ,y ) ∈ X ⨯ Y
End of Section pair_setsum
Notation . We use
∑ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Sigma .
Notation . We use
⨯ as an infix operator with priority 440 and which associates to the left corresponding to applying term
setprod .
Notation . We use
∏ x ...y [possibly with ascriptions] , B as a binder notation corresponding to a term constructed using
Pi .
Notation . We use
:^: as an infix operator with priority 430 and which associates to the left corresponding to applying term
setexp .
New In Part 2
Definition. We define
DescrR_i_io_1 to be
λR ⇒ Eps_i (λx ⇒ (∃y : set → prop , R x y ) ∧ (∀y z : set → prop , R x y → R x z → y = z ) ) of type
(set → (set → prop ) → prop ) → set .
Theorem. (
DescrR_i_io_12 ) The following is provable:
∀R : set → (set → prop ) → prop , (∃x, (∃y : set → prop , R x y ) ∧ (∀y z : set → prop , R x y → R x z → y = z ) ) → R (DescrR_i_io_1 R ) (DescrR_i_io_2 R )
Proof: Let R be given.
Assume H1 : ∃x, (∃y : set → prop , R x y ) ∧ (∀y z : set → prop , R x y → R x z → y = z ) .
An
exact proof term for the current goal is
(Eps_i_ex (λx ⇒ (∃y : set → prop , R x y ) ∧ (∀y z : set → prop , R x y → R x z → y = z ) ) H1 ) .
Apply L1 to the current goal.
Assume H2 H3 .
∎
Definition. We define
PNoEq_ to be
λalpha p q ⇒ ∀beta ∈ alpha , p beta ↔ q beta of type
set → (set → prop ) → (set → prop ) → prop .
Theorem. (
PNoEq_ref_ ) The following is provable:
∀alpha, ∀p : set → prop , PNoEq_ alpha p p
Proof: Let alpha, p and beta be given.
Assume H2 .
∎
Theorem. (
PNoEq_sym_ ) The following is provable:
∀alpha, ∀p q : set → prop , PNoEq_ alpha p q → PNoEq_ alpha q p
Proof: Let alpha, p and q be given.
Assume H1 .
Let beta be given.
Assume H2 .
An
exact proof term for the current goal is
H1 beta H2 .
∎
Proof: Let alpha, p, q and r be given.
Assume H1 H2 .
Let beta be given.
Assume H3 .
An
exact proof term for the current goal is
H1 beta H3 .
An
exact proof term for the current goal is
H2 beta H3 .
∎
Proof: Let p, q and alpha be given.
Assume Ha .
Let beta be given.
Assume Hb H1 .
Let gamma be given.
We will prove p gamma ↔ q gamma .
Apply H1 to the current goal.
We will prove gamma ∈ alpha .
Apply Ha to the current goal.
Assume Ha1 _ .
An
exact proof term for the current goal is
Ha1 beta Hb gamma H2 .
∎
Definition. We define
PNoLt_ to be
λalpha p q ⇒ ∃beta ∈ alpha , PNoEq_ beta p q ∧ ¬ p beta ∧ q beta of type
set → (set → prop ) → (set → prop ) → prop .
Theorem. (
PNoLt_E_ ) The following is provable:
Proof: Let alpha, p and q be given.
Assume H1 .
Let R be given.
Assume H2 .
Apply H1 to the current goal.
Let beta be given.
Assume H3 .
Apply H3 to the current goal.
Assume H5 .
Apply H5 to the current goal.
Assume H5 .
Apply H5 to the current goal.
Assume H6 H7 H8 .
An
exact proof term for the current goal is
H2 beta H4 H6 H7 H8 .
∎
Theorem. (
PNoLt_irref_ ) The following is provable:
∀alpha, ∀p : set → prop , ¬ PNoLt_ alpha p p
Proof: Let alpha and p be given.
Assume H1 .
Apply H1 to the current goal.
Let beta be given.
Assume H2 .
Apply H2 to the current goal.
Assume _ H3 .
Apply H3 to the current goal.
Assume H3 .
Apply H3 to the current goal.
Assume _ H4 H5 .
An exact proof term for the current goal is H4 H5 .
∎
Proof: Let p, q and alpha be given.
Assume Ha .
Let beta be given.
Assume Hb H1 .
Apply H1 to the current goal.
Let gamma be given.
Assume H2 .
Apply H2 to the current goal.
Assume H3 .
We use gamma to witness the existential quantifier.
Apply andI to the current goal.
We will prove gamma ∈ alpha .
Apply Ha to the current goal.
Assume Ha1 _ .
An
exact proof term for the current goal is
Ha1 beta Hb gamma H2 .
An exact proof term for the current goal is H3 .
∎
Proof: Let p and q be given.
Let alpha be given.
Assume Ha .
Apply xm (PNoEq_ alpha p q ) to the current goal.
Apply orIL to the current goal.
Apply orIR to the current goal.
An exact proof term for the current goal is H1 .
We prove the intermediate
claim L1 :
∃beta, ¬ (beta ∈ alpha → (p beta ↔ q beta ) ) .
Apply L1 to the current goal.
Let beta be given.
We prove the intermediate
claim L2 :
beta ∈ alpha ∧ ¬ (p beta ↔ q beta ) .
Apply xm (beta ∈ alpha ) to the current goal.
Apply H2 to the current goal.
Assume _ .
An exact proof term for the current goal is H4 .
Apply andI to the current goal.
An exact proof term for the current goal is H3 .
An exact proof term for the current goal is H4 .
Apply H2 to the current goal.
Assume H4 .
An exact proof term for the current goal is H3 H4 .
Apply L2 to the current goal.
Apply IH beta H3 to the current goal.
Assume H5 .
Apply H5 to the current goal.
Apply orIL to the current goal.
Apply orIL to the current goal.
An
exact proof term for the current goal is
PNoLt_mon_ p q alpha Ha beta H3 H5 .
Apply xm (p beta ) to the current goal.
Apply xm (q beta ) to the current goal.
Apply H4 to the current goal.
Apply iffI to the current goal.
Assume _ .
An exact proof term for the current goal is H7 .
Assume _ .
An exact proof term for the current goal is H6 .
Apply orIR to the current goal.
We use
beta to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H3 .
Apply and3I to the current goal.
An exact proof term for the current goal is H5 .
An exact proof term for the current goal is H7 .
An exact proof term for the current goal is H6 .
Apply xm (q beta ) to the current goal.
Apply orIL to the current goal.
Apply orIL to the current goal.
We use
beta to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H3 .
Apply and3I to the current goal.
An exact proof term for the current goal is H5 .
An exact proof term for the current goal is H6 .
An exact proof term for the current goal is H7 .
Apply H4 to the current goal.
Apply iffI to the current goal.
Assume H8 .
An exact proof term for the current goal is H6 H8 .
Assume H8 .
An exact proof term for the current goal is H7 H8 .
Apply orIR to the current goal.
An
exact proof term for the current goal is
PNoLt_mon_ q p alpha Ha beta H3 H5 .
∎
Proof: Let alpha be given.
Assume Ha .
Let p, q and r be given.
Assume Hpq Hqr .
Apply PNoLt_E_ alpha p q Hpq to the current goal.
Let beta be given.
Apply PNoLt_E_ alpha q r Hqr to the current goal.
Let gamma be given.
Assume Hgamma1 : gamma ∈ alpha .
Assume Hgamma3 : ¬ q gamma .
Assume Hgamma4 : r gamma .
We prove the intermediate
claim Lgamma :
ordinal gamma .
An
exact proof term for the current goal is
ordinal_Hered alpha Ha gamma Hgamma1 .
Assume H1 .
Apply H1 to the current goal.
We use
beta to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hbeta1 .
Apply and3I to the current goal.
An
exact proof term for the current goal is
PNoEq_antimon_ q r gamma Lgamma beta H1 Hgamma2 .
An exact proof term for the current goal is Hbeta3 .
Apply Hgamma2 beta H1 to the current goal.
Assume H2 _ .
An exact proof term for the current goal is H2 Hbeta4 .
We use
beta to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hbeta1 .
Apply and3I to the current goal.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hgamma2 .
An exact proof term for the current goal is Hbeta3 .
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hgamma4 .
We use gamma to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hgamma1 .
Apply and3I to the current goal.
We will
prove PNoEq_ gamma p r .
We will
prove PNoEq_ gamma p q .
An
exact proof term for the current goal is
PNoEq_antimon_ p q beta Lbeta gamma H1 Hbeta2 .
An exact proof term for the current goal is Hgamma2 .
We will prove ¬ p gamma .
Assume H2 : p gamma .
Apply Hbeta2 gamma H1 to the current goal.
Assume H3 _ .
Apply Hgamma3 to the current goal.
We will prove q gamma .
An exact proof term for the current goal is H3 H2 .
We will prove r gamma .
An exact proof term for the current goal is Hgamma4 .
∎
Definition. We define
PNoLt to be
λalpha p beta q ⇒ PNoLt_ (alpha ∩ beta ) p q ∨ alpha ∈ beta ∧ PNoEq_ alpha p q ∧ q alpha ∨ beta ∈ alpha ∧ PNoEq_ beta p q ∧ ¬ p beta of type
set → (set → prop ) → set → (set → prop ) → prop .
Theorem. (
PNoLtI1 ) The following is provable:
Proof: Let alpha, beta, p and q be given.
Assume H1 .
Apply or3I1 to the current goal.
An exact proof term for the current goal is H1 .
∎
Theorem. (
PNoLtI2 ) The following is provable:
∀alpha beta, ∀p q : set → prop , alpha ∈ beta → PNoEq_ alpha p q → q alpha → PNoLt alpha p beta q
Proof: Let alpha, beta, p and q be given.
Assume H1 H2 H3 .
Apply or3I2 to the current goal.
Apply and3I to the current goal.
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is H2 .
An exact proof term for the current goal is H3 .
∎
Theorem. (
PNoLtI3 ) The following is provable:
Proof: Let alpha, beta, p and q be given.
Assume H1 H2 H3 .
Apply or3I3 to the current goal.
Apply and3I to the current goal.
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is H2 .
An exact proof term for the current goal is H3 .
∎
Theorem. (
PNoLtE ) The following is provable:
Proof: Let alpha, beta, p and q be given.
Assume H1 .
Let R be given.
Assume HC1 HC2 HC3 .
Apply H1 to the current goal.
Assume H1 .
Apply H1 to the current goal.
An exact proof term for the current goal is HC1 .
Assume H1 .
Apply H1 to the current goal.
Assume H1 .
Apply H1 to the current goal.
An exact proof term for the current goal is HC2 .
Assume H1 .
Apply H1 to the current goal.
Assume H1 .
Apply H1 to the current goal.
An exact proof term for the current goal is HC3 .
∎
Theorem. (
PNoLt_irref ) The following is provable:
∀alpha, ∀p : set → prop , ¬ PNoLt alpha p alpha p
Proof: Let alpha and p be given.
Assume H1 .
Apply PNoLtE alpha alpha p p H1 to the current goal.
An
exact proof term for the current goal is
PNoLt_irref_ (alpha ∩ alpha ) p H1 .
Assume H1 : alpha ∈ alpha .
An
exact proof term for the current goal is
In_irref alpha H1 .
Assume H1 : alpha ∈ alpha .
An
exact proof term for the current goal is
In_irref alpha H1 .
∎
Proof: Let alpha, beta, p and q be given.
Assume Ha Hb .
Apply Ha to the current goal.
Assume Ha1 _ .
Apply Hb to the current goal.
Assume Hb1 _ .
We prove the intermediate
claim Lab :
ordinal (alpha ∩ beta ) .
Assume H1 .
Apply H1 to the current goal.
Apply or3I1 to the current goal.
An exact proof term for the current goal is H1 .
Assume H2 .
Apply H2 to the current goal.
We prove the intermediate
claim L1 :
alpha ∩ beta = alpha .
We prove the intermediate
claim L2 :
PNoEq_ alpha p q .
rewrite the current goal using L1 (from right to left).
An exact proof term for the current goal is H1 .
Apply xm (q alpha ) to the current goal.
Assume H3 : q alpha .
Apply or3I1 to the current goal.
An exact proof term for the current goal is H2 .
We will
prove PNoEq_ alpha p q .
An exact proof term for the current goal is L2 .
An exact proof term for the current goal is H3 .
Assume H3 : ¬ q alpha .
Apply or3I3 to the current goal.
An exact proof term for the current goal is H2 .
We will
prove PNoEq_ alpha q p .
An exact proof term for the current goal is L2 .
An exact proof term for the current goal is H3 .
We prove the intermediate
claim L1 :
alpha ∩ beta = alpha .
rewrite the current goal using H2 (from right to left).
We prove the intermediate
claim L2 :
PNoEq_ alpha p q .
rewrite the current goal using L1 (from right to left).
An exact proof term for the current goal is H1 .
Apply or3I2 to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is H2 .
We will
prove PNoEq_ alpha p q .
An exact proof term for the current goal is L2 .
We prove the intermediate
claim L1 :
alpha ∩ beta = beta .
We prove the intermediate
claim L2 :
PNoEq_ beta p q .
rewrite the current goal using L1 (from right to left).
An exact proof term for the current goal is H1 .
Apply xm (p beta ) to the current goal.
Apply or3I3 to the current goal.
An exact proof term for the current goal is H2 .
An exact proof term for the current goal is L2 .
An exact proof term for the current goal is H3 .
Apply or3I1 to the current goal.
An exact proof term for the current goal is H2 .
An exact proof term for the current goal is L2 .
An exact proof term for the current goal is H3 .
Apply or3I3 to the current goal.
An exact proof term for the current goal is H1 .
∎
Proof: Let alpha and beta be given.
Assume Ha Hb .
Let p, q and r be given.
Assume Hpq Hqr .
Apply PNoLtE alpha beta p q Hpq to the current goal.
Apply Hpq1 to the current goal.
Let delta be given.
Assume Hpq2 .
Apply Hpq2 to the current goal.
Assume Hd1 Hd2 .
Assume Hpq3 .
Apply Hpq3 to the current goal.
Assume Hpq3 .
Apply Hpq3 to the current goal.
Assume Hpq4 : ¬ p delta .
Assume Hpq5 : q delta .
We will
prove ∃delta ∈ alpha ∩ beta , PNoEq_ delta p r ∧ ¬ p delta ∧ r delta .
We use delta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hd .
Apply and3I to the current goal.
We will
prove PNoEq_ delta p r .
We will
prove PNoEq_ delta p q .
An exact proof term for the current goal is Hpq3 .
We will
prove PNoEq_ delta q r .
An exact proof term for the current goal is Hqr .
We will prove ¬ p delta .
An exact proof term for the current goal is Hpq4 .
We will prove r delta .
An
exact proof term for the current goal is
iffEL (q delta ) (r delta ) (Hqr delta Hd2 ) Hpq5 .
Assume Hpq3 : q alpha .
We will
prove alpha ∈ beta .
An exact proof term for the current goal is Hpq1 .
We will
prove PNoEq_ alpha p r .
An exact proof term for the current goal is Hpq2 .
We will
prove PNoEq_ alpha q r .
An exact proof term for the current goal is Hqr .
We will prove r alpha .
An
exact proof term for the current goal is
iffEL (q alpha ) (r alpha ) (Hqr alpha Hpq1 ) Hpq3 .
We will
prove beta ∈ alpha .
An exact proof term for the current goal is Hpq1 .
An exact proof term for the current goal is Hpq2 .
An exact proof term for the current goal is Hqr .
An exact proof term for the current goal is Hpq3 .
∎
Proof: Let alpha and beta be given.
Assume Ha Hb .
Let p, q and r be given.
Assume Hpq Hqr .
Apply PNoLtE alpha beta q r Hqr to the current goal.
Apply Hqr1 to the current goal.
Let delta be given.
Assume Hqr2 .
Apply Hqr2 to the current goal.
Assume Hd1 Hd2 .
Assume Hqr3 .
Apply Hqr3 to the current goal.
Assume Hqr3 .
Apply Hqr3 to the current goal.
Assume Hqr4 : ¬ q delta .
Assume Hqr5 : r delta .
We will
prove ∃delta ∈ alpha ∩ beta , PNoEq_ delta p r ∧ ¬ p delta ∧ r delta .
We use delta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hd .
Apply and3I to the current goal.
We will
prove PNoEq_ delta p r .
We will
prove PNoEq_ delta p q .
We will
prove PNoEq_ alpha p q .
An exact proof term for the current goal is Hpq .
We will
prove PNoEq_ delta q r .
An exact proof term for the current goal is Hqr3 .
We will prove ¬ p delta .
Assume H1 : p delta .
Apply Hqr4 to the current goal.
We will prove q delta .
An
exact proof term for the current goal is
iffEL (p delta ) (q delta ) (Hpq delta Hd1 ) H1 .
We will prove r delta .
An exact proof term for the current goal is Hqr5 .
Assume Hqr3 : r alpha .
We will
prove alpha ∈ beta .
An exact proof term for the current goal is Hqr1 .
We will
prove PNoEq_ alpha p r .
An exact proof term for the current goal is Hpq .
An exact proof term for the current goal is Hqr2 .
We will prove r alpha .
An exact proof term for the current goal is Hqr3 .
We will
prove beta ∈ alpha .
An exact proof term for the current goal is Hqr1 .
An exact proof term for the current goal is Hpq .
An exact proof term for the current goal is Hqr2 .
Apply Hqr3 to the current goal.
An
exact proof term for the current goal is
iffEL (p beta ) (q beta ) (Hpq beta Hqr1 ) H1 .
∎
Theorem. (
PNoLt_tra ) The following is provable:
Proof: Let alpha, beta and gamma be given.
Assume Ha Hb Hc .
Apply Ha to the current goal.
Assume Ha1 _ .
Apply Hc to the current goal.
Assume Hc1 _ .
Let p, q and r be given.
Assume Hpq Hqr .
Apply PNoLtE alpha beta p q Hpq to the current goal.
Apply Hpq1 to the current goal.
Let delta be given.
Assume Hpq2 .
Apply Hpq2 to the current goal.
Assume Hd1 Hd2 .
Assume Hpq3 .
Apply Hpq3 to the current goal.
Assume Hpq3 .
Apply Hpq3 to the current goal.
Assume Hpq4 : ¬ p delta .
Assume Hpq5 : q delta .
We prove the intermediate
claim Ld :
ordinal delta .
Apply PNoLtE beta gamma q r Hqr to the current goal.
Apply Hqr1 to the current goal.
Let eps be given.
Assume Hqr2 .
Apply Hqr2 to the current goal.
Assume He1 He2 .
Assume Hqr3 .
Apply Hqr3 to the current goal.
Assume Hqr3 .
Apply Hqr3 to the current goal.
Assume Hqr4 : ¬ q eps .
Assume Hqr5 : r eps .
We prove the intermediate
claim Le :
ordinal eps .
We will
prove PNoLt alpha p gamma r .
We will
prove ∃delta ∈ alpha ∩ gamma , PNoEq_ delta p r ∧ ¬ p delta ∧ r delta .
Assume H1 .
Apply H1 to the current goal.
Assume H1 : delta ∈ eps .
We use delta to witness the existential quantifier.
Apply andI to the current goal.
We will prove delta ∈ alpha ∩ gamma .
An exact proof term for the current goal is Hd1 .
We will prove delta ∈ gamma .
An exact proof term for the current goal is Hc1 eps He2 delta H1 .
Apply and3I to the current goal.
We will
prove PNoEq_ delta p r .
We will
prove PNoEq_ delta p q .
An exact proof term for the current goal is Hpq3 .
We will
prove PNoEq_ delta q r .
An exact proof term for the current goal is Hqr3 .
We will prove ¬ p delta .
An exact proof term for the current goal is Hpq4 .
We will prove r delta .
An
exact proof term for the current goal is
iffEL (q delta ) (r delta ) (Hqr3 delta H1 ) Hpq5 .
Assume H1 : delta = eps .
We use delta to witness the existential quantifier.
Apply andI to the current goal.
We will prove delta ∈ alpha ∩ gamma .
An exact proof term for the current goal is Hd1 .
We will prove delta ∈ gamma .
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is He2 .
Apply and3I to the current goal.
We will
prove PNoEq_ delta p r .
We will
prove PNoEq_ delta p q .
An exact proof term for the current goal is Hpq3 .
We will
prove PNoEq_ delta q r .
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hqr3 .
We will prove ¬ p delta .
An exact proof term for the current goal is Hpq4 .
We will prove r delta .
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hqr5 .
Assume H1 : eps ∈ delta .
We use eps to witness the existential quantifier.
Apply andI to the current goal.
We will prove eps ∈ alpha ∩ gamma .
We will prove eps ∈ alpha .
An exact proof term for the current goal is Ha1 delta Hd1 eps H1 .
An exact proof term for the current goal is He2 .
Apply and3I to the current goal.
We will
prove PNoEq_ delta p q .
An exact proof term for the current goal is Hpq3 .
An exact proof term for the current goal is Hqr3 .
We will prove ¬ p eps .
Assume H2 : p eps .
Apply Hqr4 to the current goal.
An
exact proof term for the current goal is
iffEL (p eps ) (q eps ) (Hpq3 eps H1 ) H2 .
We will prove r eps .
An exact proof term for the current goal is Hqr5 .
We will
prove ∃delta ∈ alpha ∩ gamma , PNoEq_ delta p r ∧ ¬ p delta ∧ r delta .
We use delta to witness the existential quantifier.
Apply andI to the current goal.
We will prove delta ∈ alpha ∩ gamma .
An exact proof term for the current goal is Hd1 .
We will prove delta ∈ gamma .
An
exact proof term for the current goal is
Hc1 beta Hqr1 delta Hd2 .
Apply and3I to the current goal.
We will
prove PNoEq_ delta p r .
We will
prove PNoEq_ delta p q .
An exact proof term for the current goal is Hpq3 .
We will
prove PNoEq_ delta q r .
An exact proof term for the current goal is Hqr2 .
We will prove ¬ p delta .
An exact proof term for the current goal is Hpq4 .
We will prove r delta .
An
exact proof term for the current goal is
iffEL (q delta ) (r delta ) (Hqr2 delta Hd2 ) Hpq5 .
Assume Hqr3 : ¬ q gamma .
Assume H1 .
Apply H1 to the current goal.
Assume H1 : delta ∈ gamma .
We will
prove PNoLt alpha p gamma r .
We will
prove ∃delta ∈ alpha ∩ gamma , PNoEq_ delta p r ∧ ¬ p delta ∧ r delta .
We use delta to witness the existential quantifier.
Apply andI to the current goal.
We will prove delta ∈ alpha ∩ gamma .
An exact proof term for the current goal is Hd1 .
We will prove delta ∈ gamma .
An exact proof term for the current goal is H1 .
Apply and3I to the current goal.
We will
prove PNoEq_ delta p r .
We will
prove PNoEq_ delta p q .
An exact proof term for the current goal is Hpq3 .
We will
prove PNoEq_ delta q r .
We will
prove PNoEq_ gamma q r .
An exact proof term for the current goal is Hqr2 .
We will prove ¬ p delta .
An exact proof term for the current goal is Hpq4 .
We will prove r delta .
An
exact proof term for the current goal is
iffEL (q delta ) (r delta ) (Hqr2 delta H1 ) Hpq5 .
Assume H1 : delta = gamma .
We will prove gamma ∈ alpha .
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hd1 .
We will
prove PNoEq_ gamma p r .
We will
prove PNoEq_ gamma p q .
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hpq3 .
We will
prove PNoEq_ gamma q r .
An exact proof term for the current goal is Hqr2 .
We will prove ¬ p gamma .
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hpq4 .
Assume H1 : gamma ∈ delta .
We will prove gamma ∈ alpha .
An exact proof term for the current goal is Ha1 delta Hd1 gamma H1 .
We will
prove PNoEq_ gamma p r .
We will
prove PNoEq_ gamma p q .
An exact proof term for the current goal is Hpq3 .
We will
prove PNoEq_ gamma q r .
An exact proof term for the current goal is Hqr2 .
We will prove ¬ p gamma .
Assume H2 : p gamma .
Apply Hqr3 to the current goal.
We will prove q gamma .
An
exact proof term for the current goal is
iffEL (p gamma ) (q gamma ) (Hpq3 gamma H1 ) H2 .
Assume Hpq3 : q alpha .
Apply PNoLtE beta gamma q r Hqr to the current goal.
Apply Hqr1 to the current goal.
Let eps be given.
Assume Hqr2 .
Apply Hqr2 to the current goal.
Assume He1 He2 .
Assume Hqr3 .
Apply Hqr3 to the current goal.
Assume Hqr3 .
Apply Hqr3 to the current goal.
Assume Hqr4 : ¬ q eps .
Assume Hqr5 : r eps .
We prove the intermediate
claim Le :
ordinal eps .
Assume H1 .
Apply H1 to the current goal.
Assume H1 : alpha ∈ eps .
We will
prove PNoLt alpha p gamma r .
We will prove alpha ∈ gamma .
An exact proof term for the current goal is Hc1 eps He2 alpha H1 .
We will
prove PNoEq_ alpha p r .
We will
prove PNoEq_ alpha p q .
An exact proof term for the current goal is Hpq2 .
We will
prove PNoEq_ alpha q r .
An exact proof term for the current goal is Hqr3 .
We will prove r alpha .
An
exact proof term for the current goal is
iffEL (q alpha ) (r alpha ) (Hqr3 alpha H1 ) Hpq3 .
Assume H1 : alpha = eps .
We will
prove PNoLt alpha p gamma r .
We will prove alpha ∈ gamma .
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is He2 .
We will
prove PNoEq_ alpha p r .
We will
prove PNoEq_ alpha p q .
An exact proof term for the current goal is Hpq2 .
We will
prove PNoEq_ alpha q r .
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hqr3 .
We will prove r alpha .
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Hqr5 .
Assume H1 : eps ∈ alpha .
We will
prove PNoLt alpha p gamma r .
We will
prove ∃delta ∈ alpha ∩ gamma , PNoEq_ delta p r ∧ ¬ p delta ∧ r delta .
We use eps to witness the existential quantifier.
Apply andI to the current goal.
We will prove eps ∈ alpha ∩ gamma .
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is He2 .
Apply and3I to the current goal.
We will
prove PNoEq_ alpha p q .
An exact proof term for the current goal is Hpq2 .
An exact proof term for the current goal is Hqr3 .
We will prove ¬ p eps .
Assume H2 : p eps .
Apply Hqr4 to the current goal.
We will prove q eps .
An
exact proof term for the current goal is
iffEL (p eps ) (q eps ) (Hpq2 eps H1 ) H2 .
We will prove r eps .
An exact proof term for the current goal is Hqr5 .
We will prove alpha ∈ gamma .
An
exact proof term for the current goal is
Hc1 beta Hqr1 alpha Hpq1 .
We will
prove PNoEq_ alpha p r .
An exact proof term for the current goal is Hpq2 .
An exact proof term for the current goal is Hqr2 .
We will prove r alpha .
An
exact proof term for the current goal is
iffEL (q alpha ) (r alpha ) (Hqr2 alpha Hpq1 ) Hpq3 .
Assume Hqr3 : ¬ q gamma .
We will
prove PNoLt alpha p gamma r .
Assume H1 .
Apply H1 to the current goal.
Assume H1 : alpha ∈ gamma .
We will prove alpha ∈ gamma .
An exact proof term for the current goal is H1 .
We will
prove PNoEq_ alpha p r .
An exact proof term for the current goal is Hpq2 .
An exact proof term for the current goal is Hqr2 .
We will prove r alpha .
An
exact proof term for the current goal is
iffEL (q alpha ) (r alpha ) (Hqr2 alpha H1 ) Hpq3 .
Assume H1 : alpha = gamma .
Apply Hqr3 to the current goal.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is Hpq3 .
Assume H1 : gamma ∈ alpha .
We will prove gamma ∈ alpha .
An exact proof term for the current goal is H1 .
We will
prove PNoEq_ gamma p r .
An exact proof term for the current goal is Hpq2 .
An exact proof term for the current goal is Hqr2 .
We will prove ¬ p gamma .
Assume H2 : p gamma .
Apply Hqr3 to the current goal.
We will prove q gamma .
An
exact proof term for the current goal is
iffEL (p gamma ) (q gamma ) (Hpq2 gamma H1 ) H2 .
Apply PNoLtE beta gamma q r Hqr to the current goal.
Apply Hqr1 to the current goal.
Let eps be given.
Assume Hqr2 .
Apply Hqr2 to the current goal.
Assume He1 He2 .
Assume Hqr3 .
Apply Hqr3 to the current goal.
Assume Hqr3 .
Apply Hqr3 to the current goal.
Assume Hqr4 : ¬ q eps .
Assume Hqr5 : r eps .
We will
prove PNoLt alpha p gamma r .
We will
prove ∃delta ∈ alpha ∩ gamma , PNoEq_ delta p r ∧ ¬ p delta ∧ r delta .
We use eps to witness the existential quantifier.
Apply andI to the current goal.
We will prove eps ∈ alpha ∩ gamma .
We will prove eps ∈ alpha .
An
exact proof term for the current goal is
Ha1 beta Hpq1 eps He1 .
An exact proof term for the current goal is He2 .
Apply and3I to the current goal.
An exact proof term for the current goal is Hpq2 .
An exact proof term for the current goal is Hqr3 .
We will prove ¬ p eps .
Assume H1 : p eps .
Apply Hqr4 to the current goal.
We will prove q eps .
An
exact proof term for the current goal is
iffEL (p eps ) (q eps ) (Hpq2 eps He1 ) H1 .
We will prove r eps .
An exact proof term for the current goal is Hqr5 .
We will
prove ∃delta ∈ alpha ∩ gamma , PNoEq_ delta p r ∧ ¬ p delta ∧ r delta .
We use
beta to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hpq1 .
An exact proof term for the current goal is Hqr1 .
Apply and3I to the current goal.
An exact proof term for the current goal is Hpq2 .
An exact proof term for the current goal is Hqr2 .
An exact proof term for the current goal is Hpq3 .
An exact proof term for the current goal is Hqr3 .
Assume Hqr3 : ¬ q gamma .
We will prove gamma ∈ alpha .
An
exact proof term for the current goal is
Ha1 beta Hpq1 gamma Hqr1 .
We will
prove PNoEq_ gamma p r .
We will
prove PNoEq_ gamma p q .
An exact proof term for the current goal is Hpq2 .
An exact proof term for the current goal is Hqr2 .
We will prove ¬ p gamma .
Assume H1 : p gamma .
Apply Hqr3 to the current goal.
We will prove q gamma .
An
exact proof term for the current goal is
iffEL (p gamma ) (q gamma ) (Hpq2 gamma Hqr1 ) H1 .
∎
Definition. We define
PNoLe to be
λalpha p beta q ⇒ PNoLt alpha p beta q ∨ alpha = beta ∧ PNoEq_ alpha p q of type
set → (set → prop ) → set → (set → prop ) → prop .
Theorem. (
PNoLeI1 ) The following is provable:
Proof: Let alpha, beta, p and q be given.
Assume H1 .
Apply orIL to the current goal.
An exact proof term for the current goal is H1 .
∎
Theorem. (
PNoLeI2 ) The following is provable:
∀alpha, ∀p q : set → prop , PNoEq_ alpha p q → PNoLe alpha p alpha q
Proof: Let alpha, p and q be given.
Assume H1 .
We will
prove PNoLt alpha p alpha q ∨ alpha = alpha ∧ PNoEq_ alpha p q .
Apply orIR to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is H1 .
∎
Theorem. (
PNoLe_ref ) The following is provable:
∀alpha, ∀p : set → prop , PNoLe alpha p alpha p
Proof: Let alpha and p be given.
∎
Proof: Let alpha and beta be given.
Assume Ha Hb .
Let p and q be given.
Apply H1 to the current goal.
Apply H2 to the current goal.
Apply PNoLt_tra alpha beta alpha Ha Hb Ha p q p to the current goal.
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is H2 .
Assume H2 .
Apply H2 to the current goal.
Apply PNoLtE alpha beta p q H1 to the current goal.
Apply Hpq1 to the current goal.
Let delta be given.
Assume Hpq2 .
Apply Hpq2 to the current goal.
Assume Hd1 Hd2 .
Assume Hpq3 .
Apply Hpq3 to the current goal.
Assume Hpq3 .
Apply Hpq3 to the current goal.
Assume Hpq4 : ¬ p delta .
Assume Hpq5 : q delta .
Apply Hpq4 to the current goal.
An
exact proof term for the current goal is
iffEL (q delta ) (p delta ) (H2b delta Hd2 ) Hpq5 .
Assume Hpq3 : q alpha .
Apply In_irref alpha to the current goal.
rewrite the current goal using H2a (from right to left) at position 2.
An exact proof term for the current goal is Hpq1 .
Apply In_irref alpha to the current goal.
rewrite the current goal using H2a (from right to left) at position 1.
An exact proof term for the current goal is Hpq1 .
Assume H1 .
An exact proof term for the current goal is H1 .
∎
Proof: Let alpha, beta and gamma be given.
Assume Ha Hb Hc .
Let p, q and r be given.
Apply H2 to the current goal.
An
exact proof term for the current goal is
PNoLt_tra alpha beta gamma Ha Hb Hc p q r H1 H2 .
Assume H2 .
Apply H2 to the current goal.
We will
prove PNoLt alpha p gamma r .
rewrite the current goal using H2a (from right to left).
An
exact proof term for the current goal is
PNoLtEq_tra alpha beta Ha Hb p q r H1 H2b .
∎
Proof: Let alpha, beta and gamma be given.
Assume Ha Hb Hc .
Let p, q and r be given.
Apply H1 to the current goal.
An
exact proof term for the current goal is
PNoLt_tra alpha beta gamma Ha Hb Hc p q r H1 H2 .
Assume H1 .
Apply H1 to the current goal.
We will
prove PNoLt alpha p gamma r .
rewrite the current goal using H1a (from left to right).
rewrite the current goal using H1a (from right to left).
An exact proof term for the current goal is H1b .
An exact proof term for the current goal is H2 .
∎
Proof: Let alpha and beta be given.
Assume Ha Hb .
Let p, q and r be given.
Assume Hpq .
Apply Hqr to the current goal.
Assume Hqr1 .
Apply orIL to the current goal.
An
exact proof term for the current goal is
PNoEqLt_tra alpha beta Ha Hb p q r Hpq Hqr1 .
Assume Hqr .
Apply Hqr to the current goal.
Apply orIR to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hqr1 .
An
exact proof term for the current goal is
PNoEq_tra_ alpha p q r Hpq Hqr2 .
∎
Theorem. (
PNoLe_tra ) The following is provable:
Proof: Let alpha, beta and gamma be given.
Assume Ha Hb Hc .
Let p, q and r be given.
Apply H1 to the current goal.
We will
prove PNoLt alpha p gamma r ∨ alpha = gamma ∧ PNoEq_ alpha p r .
Apply orIL to the current goal.
An
exact proof term for the current goal is
PNoLtLe_tra alpha beta gamma Ha Hb Hc p q r H1 H2 .
Assume H1 .
Apply H1 to the current goal.
We will
prove PNoLe alpha p gamma r .
rewrite the current goal using H1a (from left to right).
We prove the intermediate
claim L1 :
PNoEq_ beta p q .
rewrite the current goal using H1a (from right to left).
An exact proof term for the current goal is H1b .
An
exact proof term for the current goal is
PNoEqLe_tra beta gamma Hb Hc p q r L1 H2 .
∎
Definition. We define
PNo_downc to be
λL alpha p ⇒ ∃beta, ordinal beta ∧ ∃q : set → prop , L beta q ∧ PNoLe alpha p beta q of type
(set → (set → prop ) → prop ) → set → (set → prop ) → prop .
Definition. We define
PNo_upc to be
λR alpha p ⇒ ∃beta, ordinal beta ∧ ∃q : set → prop , R beta q ∧ PNoLe beta q alpha p of type
(set → (set → prop ) → prop ) → set → (set → prop ) → prop .
Proof: Let L, alpha, beta, p and q be given.
Assume Ha Hb .
Apply H1 to the current goal.
Let gamma be given.
Assume H3 .
Apply H3 to the current goal.
Assume H3 .
Apply H3 to the current goal.
Let r be given.
Assume H3 .
Apply H3 to the current goal.
Assume H3 : L gamma r .
We will
prove ∃delta, ordinal delta ∧ ∃r : set → prop , L delta r ∧ PNoLe beta q delta r .
We use gamma to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hc .
We use r to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H3 .
An
exact proof term for the current goal is
PNoLe_tra beta alpha gamma Hb Ha Hc q p r H2 H4 .
∎
Theorem. (
PNo_downc_ref ) The following is provable:
∀L : set → (set → prop ) → prop , ∀alpha, ordinal alpha → ∀p : set → prop , L alpha p → PNo_downc L alpha p
Proof: Let L and alpha be given.
Assume Ha .
Let p be given.
Assume H1 : L 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 .
We use p to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H1 .
∎
Theorem. (
PNo_upc_ref ) The following is provable:
∀R : set → (set → prop ) → prop , ∀alpha, ordinal alpha → ∀p : set → prop , R alpha p → PNo_upc R alpha p
Proof: Let R and alpha be given.
Assume Ha .
Let p be given.
Assume H1 : R 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 .
We use p to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H1 .
∎
Theorem. (
PNoLe_upc ) The following is provable:
Proof: Let R, alpha, beta, p and q be given.
Assume Ha Hb .
Apply H1 to the current goal.
Let gamma be given.
Assume H3 .
Apply H3 to the current goal.
Assume H3 .
Apply H3 to the current goal.
Let r be given.
Assume H3 .
Apply H3 to the current goal.
Assume H3 : R gamma r .
We will
prove ∃delta, ordinal delta ∧ ∃r : set → prop , R delta r ∧ PNoLe delta r beta q .
We use gamma to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hc .
We use r to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H3 .
An
exact proof term for the current goal is
PNoLe_tra gamma alpha beta Hc Ha Hb r p q H4 H2 .
∎
Definition. We define
PNoLt_pwise to be
λL R ⇒ ∀gamma, ordinal gamma → ∀p : set → prop , L gamma p → ∀delta, ordinal delta → ∀q : set → prop , R delta q → PNoLt gamma p delta q of type
(set → (set → prop ) → prop ) → (set → (set → prop ) → prop ) → prop .
Proof: Let L and R be given.
Assume HLR .
Let gamma be given.
Assume Hc .
Let p be given.
Assume Hp .
Let delta be given.
Assume Hd .
Let q be given.
Assume Hq .
Apply Hp to the current goal.
Let alpha be given.
Assume H1 .
Apply H1 to the current goal.
Assume H3 .
Apply H3 to the current goal.
Let p2 be given.
Assume H3 .
Apply H3 to the current goal.
Assume H4 : L alpha p2 .
Apply Hq to the current goal.
Let beta be given.
Assume H6 .
Apply H6 to the current goal.
Assume H8 .
Apply H8 to the current goal.
Let q2 be given.
Assume H9 .
Apply H9 to the current goal.
We prove the intermediate
claim L1 :
PNoLt gamma p delta q .
Apply PNoLeLt_tra gamma alpha delta Hc H2 Hd p p2 q H5 to the current goal.
We will
prove PNoLt alpha p2 delta q .
Apply PNoLtLe_tra alpha beta delta H2 H7 Hd p2 q2 q (HLR alpha H2 p2 H4 beta H7 q2 H10 ) to the current goal.
An exact proof term for the current goal is H11 .
Assume H12 .
Apply H12 to the current goal.
We will
prove PNoLt gamma p gamma p .
Apply PNoLt_tra gamma delta gamma Hc Hd Hc p q p L1 to the current goal.
An exact proof term for the current goal is H12 .
We will
prove PNoLt delta q delta q .
Apply PNoLeLt_tra delta gamma delta Hd Hc Hd q p q to the current goal.
We will
prove PNoLe delta q gamma p .
We will
prove PNoLt delta q gamma p ∨ delta = gamma ∧ PNoEq_ delta q p .
Apply orIR to the current goal.
An exact proof term for the current goal is H12 .
We will
prove PNoLt gamma p delta q .
An exact proof term for the current goal is L1 .
An exact proof term for the current goal is H12 .
∎
Proof: Let L and alpha be given.
Assume Ha .
Let p and q be given.
Let beta be given.
Let r be given.
An
exact proof term for the current goal is
H1 beta Hb r H2 .
We will
prove PNoEq_ alpha p q .
An exact proof term for the current goal is Hpq .
∎
Proof: Let L and alpha be given.
Assume Ha .
Let p and beta be given.
Assume Hb .
Apply Ha to the current goal.
Assume Ha1 _ .
Apply Lb to the current goal.
Assume H2 _ .
An exact proof term for the current goal is H2 .
Let gamma be given.
Assume Hc .
Let q be given.
Assume H4 .
We prove the intermediate claim Lca : gamma ∈ alpha .
An
exact proof term for the current goal is
Ha1 beta Hb gamma Hc .
We prove the intermediate
claim L1 :
PNoLt gamma q alpha p .
Apply H1 to the current goal.
We will prove gamma ∈ alpha .
An exact proof term for the current goal is Lca .
An exact proof term for the current goal is H4 .
Apply PNoLtE gamma alpha q p L1 to the current goal.
We prove the intermediate claim L2 : gamma ∩ alpha = gamma .
An exact proof term for the current goal is Ha1 gamma Lca .
We prove the intermediate
claim L3 :
gamma ∩ beta = gamma .
An exact proof term for the current goal is Lbt gamma Hc .
rewrite the current goal using L3 (from left to right).
rewrite the current goal using L2 (from right to left).
An exact proof term for the current goal is H5 .
Assume H5 : gamma ∈ alpha .
Assume H7 : p gamma .
We will
prove gamma ∈ beta .
An exact proof term for the current goal is Hc .
We will
prove PNoEq_ gamma q p .
An exact proof term for the current goal is H6 .
We will prove p gamma .
An exact proof term for the current goal is H7 .
Assume H5 : alpha ∈ gamma .
An
exact proof term for the current goal is
In_no2cycle alpha gamma H5 Lca .
∎
Proof: Let R and alpha be given.
Assume Ha .
Let p and q be given.
Let beta be given.
Let r be given.
We will
prove PNoEq_ alpha q p .
An exact proof term for the current goal is Hpq .
An
exact proof term for the current goal is
H1 beta Hb r H2 .
∎
Proof: Let R and alpha be given.
Assume Ha .
Let p and beta be given.
Assume Hb .
Apply Ha to the current goal.
Assume Ha1 _ .
Apply Lb to the current goal.
Assume H2 _ .
An exact proof term for the current goal is H2 .
Let gamma be given.
Assume Hc .
Let q be given.
Assume H4 .
We prove the intermediate claim Lca : gamma ∈ alpha .
An
exact proof term for the current goal is
Ha1 beta Hb gamma Hc .
We prove the intermediate
claim L1 :
PNoLt alpha p gamma q .
Apply H1 to the current goal.
We will prove gamma ∈ alpha .
An exact proof term for the current goal is Lca .
An exact proof term for the current goal is H4 .
Apply PNoLtE alpha gamma p q L1 to the current goal.
We prove the intermediate claim L2 : alpha ∩ gamma = gamma .
An exact proof term for the current goal is Ha1 gamma Lca .
We prove the intermediate
claim L3 :
beta ∩ gamma = gamma .
An exact proof term for the current goal is Lbt gamma Hc .
rewrite the current goal using L3 (from left to right).
rewrite the current goal using L2 (from right to left).
An exact proof term for the current goal is H5 .
Assume H5 : alpha ∈ gamma .
An
exact proof term for the current goal is
In_no2cycle alpha gamma H5 Lca .
Assume H5 : gamma ∈ alpha .
Assume H7 : ¬ p gamma .
We will
prove gamma ∈ beta .
An exact proof term for the current goal is Hc .
We will
prove PNoEq_ gamma p q .
An exact proof term for the current goal is H6 .
We will prove ¬ p gamma .
An exact proof term for the current goal is H7 .
∎
Proof: Let L, R and alpha be given.
Assume Ha .
Let p and q be given.
Assume Hpq H1 .
Apply H1 to the current goal.
Assume H2 H3 .
Apply andI to the current goal.
∎
Proof: Let L, R and alpha be given.
Assume Ha .
Let p and beta be given.
Assume Hb H1 .
Apply H1 to the current goal.
Assume H2 H3 .
Apply andI to the current goal.
∎
Theorem. (
PNo_extend0_eq ) The following is provable:
∀alpha, ∀p : set → prop , PNoEq_ alpha p (λdelta ⇒ p delta ∧ delta ≠ alpha )
Proof: Let alpha and p be given.
Set p0 to be the term λdelta ⇒ p delta ∧ delta ≠ alpha of type set → prop .
Let beta be given.
Apply iffI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is H1 .
We will
prove beta ≠ alpha .
Apply In_irref alpha to the current goal.
rewrite the current goal using H2 (from right to left) at position 1.
An exact proof term for the current goal is Hb .
Apply H1 to the current goal.
Assume H2 _ .
An exact proof term for the current goal is H2 .
∎
Theorem. (
PNo_extend1_eq ) The following is provable:
∀alpha, ∀p : set → prop , PNoEq_ alpha p (λdelta ⇒ p delta ∨ delta = alpha )
Proof: Let alpha and p be given.
Set p1 to be the term λdelta ⇒ p delta ∨ delta = alpha of type set → prop .
Let beta be given.
Apply iffI to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is H1 .
Apply H1 to the current goal.
An exact proof term for the current goal is H2 .
Apply In_irref alpha to the current goal.
rewrite the current goal using H2 (from right to left) at position 1.
An exact proof term for the current goal is Hb .
∎
Proof: Let L and R be given.
Assume HLR .
Let alpha be given.
Assume Ha .
Apply Ha to the current goal.
Assume Ha1 _ .
Apply dneg to the current goal.
Let gamma be given.
Assume Hc : gamma ∈ alpha .
Apply IH gamma Hc to the current goal.
Assume H1 .
An exact proof term for the current goal is H1 .
Apply H1 to the current goal.
Let tau be given.
Assume H2 .
Apply H2 to the current goal.
Assume Ht : tau ∈ gamma .
Assume H2 .
Apply H2 to the current goal.
Let p be given.
Apply HNC2 to the current goal.
We use tau to witness the existential quantifier.
Apply andI to the current goal.
We will prove tau ∈ alpha .
An exact proof term for the current goal is Ha1 gamma Hc tau Ht .
We use p to witness the existential quantifier.
An exact proof term for the current goal is H3 .
Let gamma be given.
Assume Hc1 : gamma ∈ alpha .
Apply LIH gamma Hc1 to the current goal.
Let p be given.
Assume Hp .
Apply Hp to the current goal.
Apply Hp1 to the current goal.
Assume Hp1a Hp1b .
We prove the intermediate
claim Lplpe :
PNoEq_ gamma pl p .
Let delta be given.
Assume Hd : delta ∈ gamma .
We prove the intermediate
claim Lsda :
ordsucc delta ∈ alpha .
An
exact proof term for the current goal is
Ha1 gamma Hc1 (ordsucc delta ) Hsd .
Apply IH2 (ordsucc delta ) Hsd Lsda to the current goal.
We will prove pl delta ↔ p delta .
Apply Hpl2 p to the current goal.
We will
prove delta ∈ ordsucc delta .
We will prove pl delta ↔ p delta .
Apply iffI to the current goal.
Assume H2 : pl delta .
We will prove p delta .
Apply H2 p to the current goal.
rewrite the current goal using Hsd (from right to left).
An exact proof term for the current goal is Hp1 .
Assume H2 : p delta .
Let q be given.
rewrite the current goal using Hsd (from right to left).
We will prove q delta .
An
exact proof term for the current goal is
iffEL (p delta ) (q delta ) (Hp2 q Hq delta Hd ) H2 .
Apply andI to the current goal.
Apply andI to the current goal.
Let beta be given.
Let q be given.
An
exact proof term for the current goal is
Hp1a beta Hb q Hq .
We will
prove PNoEq_ gamma p pl .
An exact proof term for the current goal is Lplpe .
Let beta be given.
Let q be given.
We will
prove PNoEq_ gamma pl p .
An exact proof term for the current goal is Lplpe .
An
exact proof term for the current goal is
Hp1b beta Hb q Hq .
Let q be given.
We will
prove PNoEq_ gamma pl q .
Apply PNoEq_tra_ gamma pl p q to the current goal.
We will
prove PNoEq_ gamma pl p .
An exact proof term for the current goal is Lplpe .
We will
prove PNoEq_ gamma p q .
An exact proof term for the current goal is Hp2 q Hq .
Let gamma be given.
Assume Hc : gamma ∈ alpha .
We prove the intermediate
claim Lc :
ordinal gamma .
An
exact proof term for the current goal is
ordinal_Hered alpha Ha gamma Hc .
An exact proof term for the current goal is Lpl1 gamma Lc Hc .
Apply HNC1 to the current goal.
We use pl to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Let beta be given.
Let q be given.
Assume H2 .
Apply H2 to the current goal.
An exact proof term for the current goal is H2 .
Assume H2 .
Apply H2 to the current goal.
Apply In_irref alpha to the current goal.
rewrite the current goal using H2 (from right to left) at position 1.
An exact proof term for the current goal is Hb .
Apply PNoLtE alpha beta pl q H2 to the current goal.
Apply H3 to the current goal.
Let gamma be given.
Assume H4 .
Apply H4 to the current goal.
Assume Hc1 Hc2 .
Assume H5 .
Apply H5 to the current goal.
Assume H5 .
Apply H5 to the current goal.
Assume H6 : ¬ pl gamma .
Assume H7 : q gamma .
We prove the intermediate
claim Lc :
ordinal gamma .
Apply H6 to the current goal.
We will prove pl gamma .
Let p be given.
We will prove p gamma .
Apply Hp to the current goal.
Assume Hp1 Hp2 .
We prove the intermediate
claim Lqp :
PNoLt gamma q (ordsucc gamma ) p .
Apply Hp1 gamma (ordsuccI2 gamma ) q to the current goal.
An exact proof term for the current goal is Hq .
We will
prove gamma ∈ beta .
An exact proof term for the current goal is Hc2 .
We will
prove PNoEq_ gamma q q .
We will prove q gamma .
An exact proof term for the current goal is H7 .
Apply H6 to the current goal.
Let delta be given.
Assume H7 .
Apply H7 to the current goal.
Assume Hd1 Hd2 .
Assume H7 .
Apply H7 to the current goal.
Assume H7 .
Apply H7 to the current goal.
Assume H8 : ¬ q delta .
Assume H9 : p delta .
We prove the intermediate
claim Ld :
ordinal delta .
An
exact proof term for the current goal is
ordinal_Hered gamma Lc delta Hd1 .
We prove the intermediate claim Lda : delta ∈ alpha .
An exact proof term for the current goal is Ha1 gamma Hc1 delta Hd1 .
We prove the intermediate
claim Lsda :
ordsucc delta ∈ alpha .
An exact proof term for the current goal is H1 delta Lda .
We prove the intermediate claim Lpld : pl delta .
Apply Lpl2 (ordsucc delta ) Lsda to the current goal.
Assume _ .
We prove the intermediate
claim Lpld1 :
PNoEq_ (ordsucc delta ) pl p .
Apply Hpl3 p to the current goal.
An exact proof term for the current goal is Lc .
We will prove delta ∈ gamma .
An exact proof term for the current goal is Hd1 .
An exact proof term for the current goal is Hp .
An
exact proof term for the current goal is
iffER (pl delta ) (p delta ) (Lpld1 delta (ordsuccI2 delta ) ) H9 .
We prove the intermediate claim Lnpld : ¬ pl delta .
Assume H10 : pl delta .
Apply H8 to the current goal.
An
exact proof term for the current goal is
iffEL (pl delta ) (q delta ) (H5 delta Hd1 ) H10 .
An exact proof term for the current goal is Lnpld Lpld .
Assume H8 : p gamma .
An exact proof term for the current goal is H8 .
Apply H5 to the current goal.
Let p be given.
Apply Hp to the current goal.
Assume Hp1 Hp2 .
Apply H6 to the current goal.
Let delta be given.
Assume H7 .
Apply H7 to the current goal.
Assume Hd1 Hd2 .
Assume H7 .
Apply H7 to the current goal.
Assume H7 .
Apply H7 to the current goal.
Assume H8 : ¬ q delta .
Assume H9 : p delta .
We prove the intermediate
claim Ld :
ordinal delta .
We prove the intermediate claim Lda : delta ∈ alpha .
An
exact proof term for the current goal is
Ha1 beta Hb delta Hd1 .
We prove the intermediate
claim Lsda :
ordsucc delta ∈ alpha .
An exact proof term for the current goal is H1 delta Lda .
We prove the intermediate claim Lpld : pl delta .
Apply Lpl2 (ordsucc delta ) Lsda to the current goal.
Assume _ .
We prove the intermediate
claim Lpld1 :
PNoEq_ (ordsucc delta ) pl p .
Apply Hpl3 p to the current goal.
An exact proof term for the current goal is Lb .
We will
prove delta ∈ beta .
An exact proof term for the current goal is Hd1 .
An exact proof term for the current goal is Hp .
An
exact proof term for the current goal is
iffER (pl delta ) (p delta ) (Lpld1 delta (ordsuccI2 delta ) ) H9 .
We prove the intermediate claim Lnpld : ¬ pl delta .
Assume H10 : pl delta .
Apply H8 to the current goal.
An
exact proof term for the current goal is
iffEL (pl delta ) (q delta ) (H4 delta Hd1 ) H10 .
An exact proof term for the current goal is Lnpld Lpld .
An exact proof term for the current goal is H8 .
Let beta be given.
Let q be given.
We prove the intermediate
claim Lsba :
ordsucc beta ∈ alpha .
An
exact proof term for the current goal is
H1 beta Hb .
Assume H2 .
Apply H2 to the current goal.
An exact proof term for the current goal is H2 .
Assume H2 .
Apply H2 to the current goal.
Apply In_irref alpha to the current goal.
rewrite the current goal using H2 (from left to right) at position 1.
An exact proof term for the current goal is Hb .
Apply PNoLtE beta alpha q pl H2 to the current goal.
Apply H3 to the current goal.
Let gamma be given.
Assume H4 .
Apply H4 to the current goal.
Assume Hc2 Hc1 .
Assume H5 .
Apply H5 to the current goal.
Assume H5 .
Apply H5 to the current goal.
Assume H6 : ¬ q gamma .
Assume H7 : pl gamma .
We prove the intermediate
claim Lc :
ordinal gamma .
We prove the intermediate
claim Lsca :
ordsucc gamma ∈ alpha .
An exact proof term for the current goal is H1 gamma Hc1 .
Apply Lpl2 (ordsucc gamma ) Lsca to the current goal.
Assume _ .
Apply Hpl2 to the current goal.
Assume _ .
We prove the intermediate
claim Lplq :
PNoLt (ordsucc gamma ) pl gamma q .
Apply Hpl2b gamma (ordsuccI2 gamma ) q to the current goal.
An exact proof term for the current goal is Hq .
We will
prove gamma ∈ beta .
An exact proof term for the current goal is Hc2 .
We will
prove PNoEq_ gamma q q .
We will prove ¬ q gamma .
An exact proof term for the current goal is H6 .
We prove the intermediate
claim Lqpl :
PNoLt gamma q (ordsucc gamma ) pl .
We will
prove gamma ∈ ordsucc gamma .
We will
prove PNoEq_ gamma q pl .
An exact proof term for the current goal is H5 .
We will prove pl gamma .
An exact proof term for the current goal is H7 .
An
exact proof term for the current goal is
PNoLt_tra gamma (ordsucc gamma ) gamma Lc Lsc Lc q pl q Lqpl Lplq .
Assume _ .
Apply Hpl2 to the current goal.
Assume _ .
An exact proof term for the current goal is Hq .
An exact proof term for the current goal is H4 .
An exact proof term for the current goal is H5 .
Let q be given.
Let gamma be given.
Assume Hc : gamma ∈ alpha .
We will prove pl gamma ↔ q gamma .
We prove the intermediate
claim Lsca :
ordsucc gamma ∈ alpha .
An exact proof term for the current goal is H1 gamma Hc .
Apply Lpl2 (ordsucc gamma ) Lsca to the current goal.
Assume _ .
Apply Hpl3 to the current goal.
We will
prove gamma ∈ ordsucc gamma .
Apply H1 to the current goal.
Let beta be given.
Assume H1 .
Apply H1 to the current goal.
rewrite the current goal using Hab (from right to left).
An exact proof term for the current goal is Ha .
An exact proof term for the current goal is Lbsb1 .
Apply LIH beta Hb to the current goal.
Let p be given.
Apply Hp to the current goal.
Apply Hp0 to the current goal.
Set p0 to be the term
λdelta ⇒ p delta ∧ delta ≠ beta of type
set → prop .
Set p1 to be the term
λdelta ⇒ p delta ∨ delta = beta of type
set → prop .
We prove the intermediate
claim Lp0e :
PNoEq_ beta p0 p .
Let gamma be given.
We will prove p0 gamma ↔ p gamma .
Apply iffI to the current goal.
We will prove p gamma .
Apply H2 to the current goal.
Assume H2 _ .
An exact proof term for the current goal is H2 .
Assume H2 : p gamma .
We will
prove p gamma ∧ gamma ≠ beta .
Apply andI to the current goal.
An exact proof term for the current goal is H2 .
rewrite the current goal using H3 (from right to left) at position 1.
An exact proof term for the current goal is Hc .
We prove the intermediate
claim Lp0b :
¬ p0 beta .
Apply H2 to the current goal.
Assume _ H2 .
Apply H2 to the current goal.
Use reflexivity.
An exact proof term for the current goal is Lp0e .
An exact proof term for the current goal is Lp0b .
We prove the intermediate
claim Lp1e :
PNoEq_ beta p p1 .
Let gamma be given.
We will prove p gamma ↔ p1 gamma .
Apply iffI to the current goal.
Assume H2 : p gamma .
We will
prove p gamma ∨ gamma = beta .
Apply orIL to the current goal.
An exact proof term for the current goal is H2 .
We will prove p gamma .
Apply H2 to the current goal.
Assume H3 : p gamma .
An exact proof term for the current goal is H3 .
rewrite the current goal using H3 (from right to left) at position 1.
An exact proof term for the current goal is Hc .
We prove the intermediate
claim Lp1b :
p1 beta .
Apply orIR to the current goal.
Use reflexivity.
An exact proof term for the current goal is Lp1e .
An exact proof term for the current goal is Lp1b .
rewrite the current goal using Hab (from left to right).
Assume H2 .
Apply HNC2 to the current goal.
We use
beta to
witness the existential quantifier.
Apply andI to the current goal.
We will
prove beta ∈ alpha .
An exact proof term for the current goal is Hb .
We use p to witness the existential quantifier.
An exact proof term for the current goal is H2 .
rewrite the current goal using
eq_or_nand (from left to right).
Assume H2 .
Apply H2 to the current goal.
Apply H2 to the current goal.
Let q0 be given.
Apply H3 to the current goal.
Let q1 be given.
An
exact proof term for the current goal is
LLR beta Lb q0 H4 beta Lb q1 H6 .
Apply orIR to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is H7 .
An exact proof term for the current goal is H5 .
Apply Lcases to the current goal.
Apply andI to the current goal.
Let gamma be given.
Let q be given.
We prove the intermediate
claim Lc :
ordinal gamma .
We prove the intermediate
claim L1 :
PNoLt gamma q beta p .
An exact proof term for the current goal is Hp1 gamma H4 q H3 .
Apply PNoLtE gamma beta q p L1 to the current goal.
Apply H5 to the current goal.
Let delta be given.
Assume H6 .
Apply H6 to the current goal.
Assume H6 .
Apply H6 to the current goal.
Assume H6 .
Apply H6 to the current goal.
Assume H7 : ¬ q delta .
Assume H8 : p delta .
Assume Hd1 : delta ∈ gamma .
We use delta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hd1 .
An exact proof term for the current goal is Hd2 .
Apply and3I to the current goal.
We will
prove PNoEq_ delta q p0 .
Apply PNoEq_tra_ delta q p p0 to the current goal.
An exact proof term for the current goal is H6 .
An exact proof term for the current goal is Lp0e .
We will prove ¬ q delta .
An exact proof term for the current goal is H7 .
We will prove p0 delta .
We will
prove p delta ∧ delta ≠ beta .
Apply andI to the current goal.
An exact proof term for the current goal is H8 .
rewrite the current goal using H9 (from right to left) at position 1.
An exact proof term for the current goal is Hd2 .
Assume H7 : p gamma .
An exact proof term for the current goal is H5 .
We will
prove PNoEq_ gamma q p0 .
Apply PNoEq_tra_ gamma q p p0 to the current goal.
We will
prove PNoEq_ gamma q p .
An exact proof term for the current goal is H6 .
We will
prove PNoEq_ gamma p p0 .
An exact proof term for the current goal is Lp0e .
We will prove p0 gamma .
We will
prove p gamma ∧ gamma ≠ beta .
Apply andI to the current goal.
An exact proof term for the current goal is H7 .
Apply In_irref gamma to the current goal.
rewrite the current goal using H8 (from left to right) at position 2.
An exact proof term for the current goal is H5 .
rewrite the current goal using H4 (from left to right).
Assume H5 .
Apply H5 to the current goal.
Assume H5 .
An exact proof term for the current goal is H5 .
Assume H5 .
Apply H5 to the current goal.
rewrite the current goal using H5 (from left to right) at position 2.
rewrite the current goal using Lbsb2 (from left to right).
Apply H6 to the current goal.
Let delta be given.
Assume H7 .
Apply H7 to the current goal.
Assume H7 .
Apply H7 to the current goal.
Assume H7 .
Apply H7 to the current goal.
Assume H8 : ¬ p0 delta .
Assume H9 : q delta .
We prove the intermediate
claim Ld :
ordinal delta .
We prove the intermediate
claim L2 :
PNoLt beta p delta q .
We will
prove delta ∈ beta .
An exact proof term for the current goal is Hd .
We will
prove PNoEq_ delta p q .
Apply PNoEq_tra_ delta p p0 q to the current goal.
We will
prove PNoEq_ delta p p0 .
An exact proof term for the current goal is Lp0e .
We will
prove PNoEq_ delta p0 q .
An exact proof term for the current goal is H7 .
We will prove ¬ p delta .
Assume H10 : p delta .
Apply H8 to the current goal.
We will
prove p delta ∧ delta ≠ beta .
Apply andI to the current goal.
An exact proof term for the current goal is H10 .
rewrite the current goal using H11 (from right to left) at position 1.
An exact proof term for the current goal is Hd .
We prove the intermediate
claim L3 :
PNoLt delta q beta p .
Apply Hp1 delta Hd q to the current goal.
Apply PNoLe_downc L gamma delta q q Lc Ld H3 to the current goal.
We will
prove PNoLe delta q gamma q .
We will
prove PNoLt delta q gamma q .
We will prove delta ∈ gamma .
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is Hd .
We will
prove PNoEq_ delta q q .
We will prove q delta .
An exact proof term for the current goal is H9 .
We will
prove PNoLt delta q delta q .
An
exact proof term for the current goal is
PNoLt_tra delta beta delta Ld Lb Ld q p q L3 L2 .
Apply H2 q to the current goal.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is H3 .
An exact proof term for the current goal is Lp0e .
An exact proof term for the current goal is H7 .
Let gamma be given.
Let q be given.
We prove the intermediate
claim Lc :
ordinal gamma .
Apply Hp2 gamma H4 q to the current goal.
An exact proof term for the current goal is H3 .
rewrite the current goal using H4 (from left to right).
Assume H5 .
Apply H5 to the current goal.
rewrite the current goal using Lbsb1 (from left to right).
Apply H6 to the current goal.
Let delta be given.
Assume H7 .
Apply H7 to the current goal.
Assume H9 .
Apply H9 to the current goal.
Assume H9 .
Apply H9 to the current goal.
Assume H10 : ¬ q delta .
Assume H11 : p0 delta .
We prove the intermediate
claim Ld :
ordinal delta .
We prove the intermediate
claim L4 :
PNoLt beta p delta q .
Apply Hp2 delta H8 q to the current goal.
Apply PNoLe_upc R gamma delta q q Lc Ld H3 to the current goal.
We will
prove PNoLe gamma q delta q .
We will
prove PNoLt gamma q delta q .
We will prove delta ∈ gamma .
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is H8 .
We will
prove PNoEq_ delta q q .
We will prove ¬ q delta .
An exact proof term for the current goal is H10 .
We prove the intermediate
claim L5 :
PNoLt delta q beta p .
We will
prove delta ∈ beta .
An exact proof term for the current goal is H8 .
We will
prove PNoEq_ delta q p .
Apply PNoEq_tra_ delta q p0 p to the current goal.
An exact proof term for the current goal is H9 .
We will
prove PNoEq_ delta p0 p .
An exact proof term for the current goal is Lp0e .
We will prove p delta .
Apply H11 to the current goal.
Assume H12 _ .
An exact proof term for the current goal is H12 .
An
exact proof term for the current goal is
PNoLt_tra beta delta beta Lb Ld Lb p q p L4 L5 .
Apply H8 to the current goal.
Assume _ H9 .
Apply H9 to the current goal.
Use reflexivity.
Assume H5 .
Apply H5 to the current goal.
rewrite the current goal using H5 (from left to right) at position 2.
An exact proof term for the current goal is H5 .
Apply HNC1 to the current goal.
We use p0 to witness the existential quantifier.
rewrite the current goal using Hab (from left to right).
Apply andI to the current goal.
An exact proof term for the current goal is Lp0imv .
Let q be given.
We prove the intermediate
claim Lpqe :
PNoEq_ beta p q .
An exact proof term for the current goal is Hp3 q Lqb .
Apply xm (q beta ) to the current goal.
Apply Lnotboth to the current goal.
rewrite the current goal using Hab (from left to right).
Apply andI to the current goal.
An exact proof term for the current goal is Lp0imv .
Let gamma be given.
We prove the intermediate claim Lpqce : p gamma ↔ q gamma .
An exact proof term for the current goal is Lpqe gamma H3 .
Apply Lpqce to the current goal.
Assume Hpqc Hqpc .
We will prove q gamma ↔ p1 gamma .
Apply iffI to the current goal.
Assume H4 : q gamma .
We will
prove p gamma ∨ gamma = beta .
Apply orIL to the current goal.
An exact proof term for the current goal is Hqpc H4 .
Apply H4 to the current goal.
An exact proof term for the current goal is Hpqc .
rewrite the current goal using H5 (from right to left) at position 1.
An exact proof term for the current goal is H3 .
We will prove q gamma ↔ p1 gamma .
Apply iffI to the current goal.
Assume _ .
We will
prove p gamma ∨ gamma = beta .
Apply orIR to the current goal.
An exact proof term for the current goal is H3 .
Assume _ .
We will prove q gamma .
rewrite the current goal using H3 (from left to right).
An exact proof term for the current goal is Hq1 .
An exact proof term for the current goal is Hq .
Let gamma be given.
We prove the intermediate claim Lpqce : p gamma ↔ q gamma .
An exact proof term for the current goal is Lpqe gamma H3 .
Apply Lpqce to the current goal.
Assume Hpqc Hqpc .
We will prove p0 gamma ↔ q gamma .
Apply iffI to the current goal.
Apply H4 to the current goal.
Assume H5 : p gamma .
Assume _ .
An exact proof term for the current goal is Hpqc H5 .
Assume H4 : q gamma .
We will
prove p gamma ∧ gamma ≠ beta .
Apply andI to the current goal.
We will prove p gamma .
An exact proof term for the current goal is Hqpc H4 .
We will
prove gamma ≠ beta .
rewrite the current goal using H5 (from right to left) at position 1.
An exact proof term for the current goal is H3 .
We will prove p0 gamma ↔ q gamma .
Apply iffI to the current goal.
Apply H4 to the current goal.
Assume _ H5 .
An exact proof term for the current goal is H5 H3 .
Assume H4 : q gamma .
Apply Hq0 to the current goal.
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is H4 .
Apply andI to the current goal.
Let gamma be given.
Let q be given.
We prove the intermediate
claim Lc :
ordinal gamma .
Apply Hp1 gamma H4 q to the current goal.
An exact proof term for the current goal is H3 .
An exact proof term for the current goal is Lpp1 .
rewrite the current goal using H4 (from left to right).
Assume H5 .
Apply H5 to the current goal.
An exact proof term for the current goal is H5 .
Assume H5 .
Apply H5 to the current goal.
rewrite the current goal using H5 (from left to right) at position 2.
rewrite the current goal using Lbsb2 (from left to right).
Apply H6 to the current goal.
Let delta be given.
Assume H7 .
Apply H7 to the current goal.
Assume H9 .
Apply H9 to the current goal.
Assume H9 .
Apply H9 to the current goal.
Assume H10 : ¬ p1 delta .
Assume H11 : q delta .
We prove the intermediate
claim Ld :
ordinal delta .
We prove the intermediate
claim L4 :
PNoLt delta q beta p .
Apply Hp1 delta H8 q to the current goal.
Apply PNoLe_downc L gamma delta q q Lc Ld H3 to the current goal.
We will
prove PNoLe delta q gamma q .
We will
prove PNoLt delta q gamma q .
We will prove delta ∈ gamma .
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is H8 .
We will
prove PNoEq_ delta q q .
We will prove q delta .
An exact proof term for the current goal is H11 .
We prove the intermediate
claim L5 :
PNoLt beta p delta q .
We will
prove delta ∈ beta .
An exact proof term for the current goal is H8 .
We will
prove PNoEq_ delta p q .
Apply PNoEq_tra_ delta p p1 q to the current goal.
We will
prove PNoEq_ delta p p1 .
An exact proof term for the current goal is Lp1e .
An exact proof term for the current goal is H9 .
We will prove ¬ p delta .
Assume H12 : p delta .
Apply H10 to the current goal.
We will
prove p delta ∨ delta = beta .
Apply orIL to the current goal.
An exact proof term for the current goal is H12 .
An
exact proof term for the current goal is
PNoLt_tra beta delta beta Lb Ld Lb p q p L5 L4 .
Apply H8 to the current goal.
Apply orIR to the current goal.
Use reflexivity.
Let gamma be given.
Let q be given.
We prove the intermediate
claim Lc :
ordinal gamma .
We prove the intermediate
claim L1 :
PNoLt beta p gamma q .
An exact proof term for the current goal is Hp2 gamma H4 q H3 .
Apply PNoLtE beta gamma p q L1 to the current goal.
Apply H5 to the current goal.
Let delta be given.
Assume H6 .
Apply H6 to the current goal.
Assume H6 .
Apply H6 to the current goal.
Assume H6 .
Apply H6 to the current goal.
Assume H7 : ¬ p delta .
Assume H8 : q delta .
Assume Hd1 : delta ∈ gamma .
We use delta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hd2 .
An exact proof term for the current goal is Hd1 .
Apply and3I to the current goal.
We will
prove PNoEq_ delta p1 q .
Apply PNoEq_tra_ delta p1 p q to the current goal.
An exact proof term for the current goal is Lp1e .
An exact proof term for the current goal is H6 .
We will prove ¬ p1 delta .
Apply H9 to the current goal.
An exact proof term for the current goal is H7 .
rewrite the current goal using H10 (from right to left) at position 1.
An exact proof term for the current goal is Hd2 .
We will prove q delta .
An exact proof term for the current goal is H8 .
Assume H7 : ¬ p gamma .
An exact proof term for the current goal is H5 .
We will
prove PNoEq_ gamma p1 q .
Apply PNoEq_tra_ gamma p1 p q to the current goal.
We will
prove PNoEq_ gamma p1 p .
An exact proof term for the current goal is Lp1e .
We will
prove PNoEq_ gamma p q .
An exact proof term for the current goal is H6 .
We will prove ¬ p1 gamma .
Apply H8 to the current goal.
An exact proof term for the current goal is H7 .
rewrite the current goal using H9 (from right to left) at position 1.
An exact proof term for the current goal is H5 .
rewrite the current goal using H4 (from left to right).
Assume H5 .
Apply H5 to the current goal.
rewrite the current goal using Lbsb1 (from left to right).
Apply H6 to the current goal.
Let delta be given.
Assume H7 .
Apply H7 to the current goal.
Assume H7 .
Apply H7 to the current goal.
Assume H7 .
Apply H7 to the current goal.
Assume H8 : ¬ q delta .
Assume H9 : p1 delta .
We prove the intermediate
claim Ld :
ordinal delta .
We prove the intermediate
claim L2 :
PNoLt delta q beta p .
We will
prove delta ∈ beta .
An exact proof term for the current goal is Hd .
We will
prove PNoEq_ delta q p .
Apply PNoEq_tra_ delta q p1 p to the current goal.
We will
prove PNoEq_ delta q p1 .
An exact proof term for the current goal is H7 .
We will
prove PNoEq_ delta p1 p .
An exact proof term for the current goal is Lp1e .
We will prove p delta .
Apply H9 to the current goal.
Assume H10 : p delta .
An exact proof term for the current goal is H10 .
rewrite the current goal using H10 (from right to left) at position 1.
An exact proof term for the current goal is Hd .
We prove the intermediate
claim L3 :
PNoLt beta p delta q .
Apply Hp2 delta Hd q to the current goal.
Apply PNoLe_upc R gamma delta q q Lc Ld H3 to the current goal.
We will
prove PNoLe gamma q delta q .
We will
prove PNoLt gamma q delta q .
We will prove delta ∈ gamma .
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is Hd .
We will
prove PNoEq_ delta q q .
We will prove ¬ q delta .
An exact proof term for the current goal is H8 .
We will
prove PNoLt delta q delta q .
An
exact proof term for the current goal is
PNoLt_tra delta beta delta Ld Lb Ld q p q L2 L3 .
Apply H2 q to the current goal.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is H3 .
An exact proof term for the current goal is Lp1e .
An exact proof term for the current goal is H7 .
Assume H5 .
Apply H5 to the current goal.
rewrite the current goal using H5 (from left to right) at position 2.
Assume H5 .
An exact proof term for the current goal is H5 .
Apply HNC1 to the current goal.
We use p1 to witness the existential quantifier.
rewrite the current goal using Hab (from left to right).
Apply andI to the current goal.
An exact proof term for the current goal is Lp1imv .
Let q be given.
We prove the intermediate
claim Lpqe :
PNoEq_ beta p q .
An exact proof term for the current goal is Hp3 q Lqb .
Apply xm (q beta ) to the current goal.
Let gamma be given.
We prove the intermediate claim Lpqce : p gamma ↔ q gamma .
An exact proof term for the current goal is Lpqe gamma H3 .
Apply Lpqce to the current goal.
Assume Hpqc Hqpc .
We will prove p1 gamma ↔ q gamma .
Apply iffI to the current goal.
Apply H4 to the current goal.
Assume H5 : p gamma .
An exact proof term for the current goal is Hpqc H5 .
rewrite the current goal using H5 (from right to left) at position 1.
An exact proof term for the current goal is H3 .
Assume H4 : q gamma .
We will
prove p gamma ∨ gamma = beta .
Apply orIL to the current goal.
We will prove p gamma .
An exact proof term for the current goal is Hqpc H4 .
We will prove p1 gamma ↔ q gamma .
Apply iffI to the current goal.
Assume _ .
We will prove q gamma .
rewrite the current goal using H3 (from left to right).
An exact proof term for the current goal is Hq1 .
Assume H4 : q gamma .
We will
prove p gamma ∨ gamma = beta .
Apply orIR to the current goal.
An exact proof term for the current goal is H3 .
Apply Lnotboth to the current goal.
rewrite the current goal using Hab (from left to right).
Apply andI to the current goal.
Let gamma be given.
We prove the intermediate claim Lpqce : p gamma ↔ q gamma .
An exact proof term for the current goal is Lpqe gamma H3 .
Apply Lpqce to the current goal.
Assume Hpqc Hqpc .
We will prove q gamma ↔ p0 gamma .
Apply iffI to the current goal.
Assume H4 : q gamma .
We will
prove p gamma ∧ gamma ≠ beta .
Apply andI to the current goal.
We will prove p gamma .
An exact proof term for the current goal is Hqpc H4 .
We will
prove gamma ≠ beta .
rewrite the current goal using H5 (from right to left) at position 1.
An exact proof term for the current goal is H3 .
Apply H4 to the current goal.
Assume H5 _ .
An exact proof term for the current goal is Hpqc H5 .
We will prove q gamma ↔ p0 gamma .
Apply iffI to the current goal.
Assume H4 : q gamma .
Apply Hq0 to the current goal.
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is H4 .
Assume H4 : p0 gamma .
Apply H4 to the current goal.
Assume _ H5 .
Apply H5 to the current goal.
An exact proof term for the current goal is H3 .
An exact proof term for the current goal is Hq .
An exact proof term for the current goal is Lp1imv .
∎
Definition. We define
PNo_lenbdd to be
λalpha L ⇒ ∀beta, ∀p : set → prop , L beta p → beta ∈ alpha of type
set → (set → (set → prop ) → prop ) → prop .
Proof: Let L and R be given.
Let alpha be given.
Assume Ha .
Apply Ha to the current goal.
Assume Ha1 _ .
Assume HaL HaR .
Let p be given.
Apply Hp1 to the current goal.
Assume Hp1a Hp1b .
Set p0 to be the term λdelta ⇒ p delta ∧ delta ≠ alpha of type set → prop .
We prove the intermediate
claim Lpp0e :
PNoEq_ alpha p p0 .
Apply andI to the current goal.
Let gamma be given.
Let q be given.
We prove the intermediate
claim Lc :
ordinal gamma .
Apply Hq to the current goal.
Let delta be given.
Assume Hq1 .
Apply Hq1 to the current goal.
Assume Hq1 .
Apply Hq1 to the current goal.
Let r be given.
Assume Hq1 .
Apply Hq1 to the current goal.
Assume Hr : L delta r .
We prove the intermediate claim Lda : delta ∈ alpha .
An exact proof term for the current goal is HaL delta r Hr .
We prove the intermediate
claim Ldsa :
delta ∈ ordsucc alpha .
An exact proof term for the current goal is Lda .
We prove the intermediate
claim Ldr :
PNo_downc L delta r .
An
exact proof term for the current goal is
PNo_downc_ref L delta Hd r Hr .
We prove the intermediate
claim Lrp :
PNoLt delta r alpha p .
An exact proof term for the current goal is Hp1a delta Lda r Ldr .
Assume H1 .
Apply H1 to the current goal.
Assume H1 .
An exact proof term for the current goal is H1 .
Assume H1 .
Apply H1 to the current goal.
Apply In_irref delta to the current goal.
rewrite the current goal using H2 (from left to right) at position 2.
An exact proof term for the current goal is Ldsa .
Apply PNoLt_tra delta alpha delta Hd Ha Hd r p r Lrp to the current goal.
We will
prove PNoLt alpha p delta r .
Apply H2 to the current goal.
Let eps be given.
Assume H3 .
Apply H3 to the current goal.
Assume He1 He2 .
We prove the intermediate claim Lea : eps ∈ alpha .
An exact proof term for the current goal is Ha1 delta Lda eps He2 .
Assume H3 .
Apply H3 to the current goal.
Assume H3 .
Apply H3 to the current goal.
Assume H4 : ¬ p0 eps .
Assume H5 : r eps .
We will
prove PNoLt_ (alpha ∩ delta ) p r .
We use eps to witness the existential quantifier.
Apply andI to the current goal.
We will prove eps ∈ alpha ∩ delta .
An exact proof term for the current goal is Lea .
An exact proof term for the current goal is He2 .
Apply and3I to the current goal.
An exact proof term for the current goal is Lpp0e .
An exact proof term for the current goal is H3 .
We will prove ¬ p eps .
Assume H5 : p eps .
Apply H4 to the current goal.
We will prove p eps ∧ eps ≠ alpha .
Apply andI to the current goal.
An exact proof term for the current goal is H5 .
We will prove eps ≠ alpha .
Assume H6 : eps = alpha .
Apply In_irref alpha to the current goal.
rewrite the current goal using H6 (from right to left) at position 1.
An exact proof term for the current goal is Lea .
We will prove r eps .
An exact proof term for the current goal is H5 .
Assume H4 : ¬ p0 delta .
Apply PNoLtI3 alpha delta p r Lda to the current goal.
We will
prove PNoEq_ delta p r .
Apply PNoEq_tra_ delta p p0 r to the current goal.
An exact proof term for the current goal is Lpp0e .
An exact proof term for the current goal is H3 .
We will prove ¬ p delta .
Assume H5 : p delta .
Apply H4 to the current goal.
We will prove p delta ∧ delta ≠ alpha .
Apply andI to the current goal.
An exact proof term for the current goal is H5 .
We will prove delta ≠ alpha .
Assume H6 : delta = alpha .
Apply In_irref alpha to the current goal.
rewrite the current goal using H6 (from right to left) at position 1.
An exact proof term for the current goal is Lda .
Let gamma be given.
Let q be given.
We prove the intermediate
claim Lc :
ordinal gamma .
Apply PNoLt_tra (ordsucc alpha ) alpha gamma Lsa Ha Lc p0 p q to the current goal.
We will
prove alpha ∈ ordsucc alpha .
We will
prove PNoEq_ alpha p0 p .
An exact proof term for the current goal is Lpp0e .
We will prove ¬ p0 alpha .
Assume H2 : p0 alpha .
Apply H2 to the current goal.
Assume H3 : p alpha .
Assume H4 : alpha ≠ alpha .
Apply H4 to the current goal.
Use reflexivity.
We will
prove PNoLt alpha p gamma q .
Apply Hq to the current goal.
Let delta be given.
Assume Hq1 .
Apply Hq1 to the current goal.
Assume Hq1 .
Apply Hq1 to the current goal.
Let r be given.
Assume Hq1 .
Apply Hq1 to the current goal.
Assume Hr : R delta r .
We prove the intermediate
claim Ldr :
PNo_upc R delta r .
An
exact proof term for the current goal is
PNo_upc_ref R delta Hd r Hr .
Apply (λH : PNoLt alpha p delta r ⇒ PNoLtLe_tra alpha delta gamma Ha Hd Lc p r q H Hrq ) to the current goal.
We will
prove PNoLt alpha p delta r .
An exact proof term for the current goal is Hp1b delta (HaR delta r Hr ) r Ldr .
∎
Proof: Let L and R be given.
Let alpha be given.
Assume Ha .
Apply Ha to the current goal.
Assume Ha1 _ .
Assume HaL HaR .
Let p be given.
Apply Hp1 to the current goal.
Assume Hp1a Hp1b .
Set p1 to be the term λdelta ⇒ p delta ∨ delta = alpha of type set → prop .
We prove the intermediate
claim Lpp1e :
PNoEq_ alpha p p1 .
Apply andI to the current goal.
Let gamma be given.
Let q be given.
We prove the intermediate
claim Lc :
ordinal gamma .
Apply PNoLt_tra gamma alpha (ordsucc alpha ) Lc Ha Lsa q p p1 to the current goal.
We will
prove PNoLt gamma q alpha p .
Apply Hq to the current goal.
Let delta be given.
Assume Hq1 .
Apply Hq1 to the current goal.
Assume Hq1 .
Apply Hq1 to the current goal.
Let r be given.
Assume Hq1 .
Apply Hq1 to the current goal.
Assume Hr : L delta r .
We prove the intermediate
claim Ldr :
PNo_downc L delta r .
We use delta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hd .
We use r to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hr .
Apply PNoLeLt_tra gamma delta alpha Lc Hd Ha q r p Hqr to the current goal.
We will
prove PNoLt delta r alpha p .
An exact proof term for the current goal is Hp1a delta (HaL delta r Hr ) r Ldr .
We will
prove alpha ∈ ordsucc alpha .
We will
prove PNoEq_ alpha p p1 .
An exact proof term for the current goal is Lpp1e .
We will prove p1 alpha .
We will prove p alpha ∨ alpha = alpha .
Apply orIR to the current goal.
Use reflexivity.
Let gamma be given.
Let q be given.
We prove the intermediate
claim Lc :
ordinal gamma .
Apply Hq to the current goal.
Let delta be given.
Assume Hq1 .
Apply Hq1 to the current goal.
Assume Hq1 .
Apply Hq1 to the current goal.
Let r be given.
Assume Hq1 .
Apply Hq1 to the current goal.
Assume Hr : R delta r .
We prove the intermediate claim Lda : delta ∈ alpha .
An exact proof term for the current goal is HaR delta r Hr .
We prove the intermediate
claim Ldsa :
delta ∈ ordsucc alpha .
An exact proof term for the current goal is Lda .
We prove the intermediate
claim Ldr :
PNo_upc R delta r .
We use delta to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hd .
We use r to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hr .
We prove the intermediate
claim Lpr :
PNoLt alpha p delta r .
An exact proof term for the current goal is Hp1b delta Lda r Ldr .
Assume H1 .
Apply H1 to the current goal.
We will
prove PNoLt alpha p alpha p .
Apply PNoLt_tra alpha delta alpha Ha Hd Ha p r p Lpr to the current goal.
We will
prove PNoLt delta r alpha p .
Apply H2 to the current goal.
Let eps be given.
Assume H3 .
Apply H3 to the current goal.
Assume He1 He2 .
We prove the intermediate claim Lea : eps ∈ alpha .
An exact proof term for the current goal is Ha1 delta Lda eps He1 .
Assume H3 .
Apply H3 to the current goal.
Assume H3 .
Apply H3 to the current goal.
Assume H4 : ¬ r eps .
Assume H5 : p1 eps .
We will
prove PNoLt_ (delta ∩ alpha ) r p .
We use eps to witness the existential quantifier.
Apply andI to the current goal.
We will prove eps ∈ delta ∩ alpha .
An exact proof term for the current goal is He1 .
An exact proof term for the current goal is Lea .
Apply and3I to the current goal.
An exact proof term for the current goal is H3 .
An exact proof term for the current goal is Lpp1e .
We will prove ¬ r eps .
An exact proof term for the current goal is H4 .
We will prove p eps .
Apply H5 to the current goal.
An exact proof term for the current goal is (λH ⇒ H ) .
Assume H6 : eps = alpha .
Apply In_irref alpha to the current goal.
rewrite the current goal using H6 (from right to left) at position 1.
An exact proof term for the current goal is Lea .
Assume H4 : p1 delta .
Apply PNoLtI2 delta alpha r p Lda to the current goal.
We will
prove PNoEq_ delta r p .
Apply PNoEq_tra_ delta r p1 p to the current goal.
An exact proof term for the current goal is H3 .
An exact proof term for the current goal is Lpp1e .
We will prove p delta .
Apply H4 to the current goal.
An exact proof term for the current goal is (λH ⇒ H ) .
Assume H5 : delta = alpha .
Apply In_irref alpha to the current goal.
rewrite the current goal using H5 (from right to left) at position 1.
An exact proof term for the current goal is Lda .
Assume H1 .
Apply H1 to the current goal.
Apply In_irref delta to the current goal.
rewrite the current goal using H2 (from left to right) at position 2.
An exact proof term for the current goal is Ldsa .
Assume H1 .
An exact proof term for the current goal is H1 .
∎
Proof: Let L and R be given.
Let alpha be given.
Assume Ha .
Assume HaL HaR .
Let p be given.
Assume Hp1 .
∎
Proof: Let L and R be given.
Assume HLR .
Let alpha be given.
Assume Ha .
Apply Ha to the current goal.
Assume Ha1 _ .
Assume HaL HaR .
Assume H2 .
Apply H2 to the current goal.
Let p be given.
Apply Hp to the current goal.
Apply Hp1 to the current goal.
Assume Hp1a Hp1b .
We use alpha to witness the existential quantifier.
Apply andI to the current goal.
We will
prove alpha ∈ ordsucc alpha .
We use p to witness the existential quantifier.
Assume H1 .
Apply H1 to the current goal.
Let beta be given.
Assume H1 .
Apply H1 to the current goal.
Assume H1 .
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 .
∎
Proof: Let L and alpha be given.
Assume Ha .
Let p and q be given.
Let beta be given.
Let r be given.
An
exact proof term for the current goal is
H1 beta Hb r H2 .
We will
prove PNoEq_ alpha p q .
An exact proof term for the current goal is Hpq .
∎
Proof: Let R and alpha be given.
Assume Ha .
Let p and q be given.
Let beta be given.
Let r be given.
We will
prove PNoEq_ alpha q p .
An exact proof term for the current goal is Hpq .
An
exact proof term for the current goal is
H1 beta Hb r H2 .
∎
Proof: Let L, R and alpha be given.
Assume Ha .
Let p and q be given.
Assume Hpq H1 .
Apply H1 to the current goal.
Assume H2 H3 .
Apply andI to the current goal.
∎
Proof: Let L and alpha be given.
Let beta be given.
Let p be given.
Let gamma be given.
Let q be given.
Apply Ha to the current goal.
Assume Ha1 _ .
Apply Lb to the current goal.
Assume H _ .
An exact proof term for the current goal is H .
We prove the intermediate
claim Lc :
ordinal gamma .
We prove the intermediate
claim Lcb :
gamma ⊆ beta .
An exact proof term for the current goal is Lb1 gamma Hc .
Apply Hq to the current goal.
Let delta be given.
Assume H2 .
Apply H2 to the current goal.
Assume H2 .
Apply H2 to the current goal.
Let r be given.
Assume H2 .
Apply H2 to the current goal.
Assume H2 : L delta r .
We prove the intermediate
claim L1 :
PNoLt delta r alpha p .
An exact proof term for the current goal is H1 delta Hd r H2 .
We prove the intermediate
claim L2 :
PNoLt gamma q alpha p .
An
exact proof term for the current goal is
PNoLeLt_tra gamma delta alpha Lc Hd Ha q r p H3 L1 .
We prove the intermediate claim Lca : gamma ∈ alpha .
An
exact proof term for the current goal is
Ha1 beta Hb1 gamma Hc .
rewrite the current goal using Hb1 (from right to left).
An exact proof term for the current goal is Hc .
We prove the intermediate claim Lca2 : gamma ⊆ alpha .
An exact proof term for the current goal is Ha1 gamma Lca .
Assume H4 .
Apply H4 to the current goal.
Assume H4 .
An exact proof term for the current goal is H4 .
Assume H4 .
Apply H4 to the current goal.
rewrite the current goal using H4 (from right to left) at position 1.
An exact proof term for the current goal is Hc .
Apply PNoLtE beta gamma p q H4 to the current goal.
Apply H5 to the current goal.
Apply PNoLt_tra alpha gamma alpha Ha Lc Ha p q p to the current goal.
We will
prove PNoLt alpha p gamma q .
We will
prove PNoLt_ (alpha ∩ gamma ) p q .
We will
prove PNoLt_ gamma p q .
An exact proof term for the current goal is H5 .
We will
prove PNoLt gamma q alpha p .
An exact proof term for the current goal is L2 .
Assume H7 : ¬ p gamma .
Apply PNoLt_tra alpha gamma alpha Ha Lc Ha p q p to the current goal.
We will
prove PNoLt alpha p gamma q .
We will prove gamma ∈ alpha .
An exact proof term for the current goal is Lca .
We will
prove PNoEq_ gamma p q .
An exact proof term for the current goal is H6 .
We will prove ¬ p gamma .
An exact proof term for the current goal is H7 .
We will
prove PNoLt gamma q alpha p .
An exact proof term for the current goal is L2 .
∎
Proof: Let R and alpha be given.
Let beta be given.
Let p be given.
Let gamma be given.
Let q be given.
Apply Ha to the current goal.
Assume Ha1 _ .
Apply Lb to the current goal.
Assume H _ .
An exact proof term for the current goal is H .
We prove the intermediate
claim Lc :
ordinal gamma .
We prove the intermediate
claim Lcb :
gamma ⊆ beta .
An exact proof term for the current goal is Lb1 gamma Hc .
Apply Hq to the current goal.
Let delta be given.
Assume H2 .
Apply H2 to the current goal.
Assume H2 .
Apply H2 to the current goal.
Let r be given.
Assume H2 .
Apply H2 to the current goal.
Assume H2 : R delta r .
We prove the intermediate
claim L1 :
PNoLt alpha p delta r .
An exact proof term for the current goal is H1 delta Hd r H2 .
We prove the intermediate
claim L2 :
PNoLt alpha p gamma q .
An
exact proof term for the current goal is
PNoLtLe_tra alpha delta gamma Ha Hd Lc p r q L1 H3 .
We prove the intermediate claim Lca : gamma ∈ alpha .
An
exact proof term for the current goal is
Ha1 beta Hb1 gamma Hc .
rewrite the current goal using Hb1 (from right to left).
An exact proof term for the current goal is Hc .
We prove the intermediate claim Lca2 : gamma ⊆ alpha .
An exact proof term for the current goal is Ha1 gamma Lca .
Assume H4 .
Apply H4 to the current goal.
Apply PNoLtE gamma beta q p H4 to the current goal.
Apply H5 to the current goal.
Apply PNoLt_tra alpha gamma alpha Ha Lc Ha p q p to the current goal.
We will
prove PNoLt alpha p gamma q .
An exact proof term for the current goal is L2 .
We will
prove PNoLt gamma q alpha p .
We will
prove PNoLt_ (gamma ∩ alpha ) q p .
We will
prove PNoLt_ gamma q p .
An exact proof term for the current goal is H5 .
Assume H7 : p gamma .
Apply PNoLt_tra alpha gamma alpha Ha Lc Ha p q p to the current goal.
We will
prove PNoLt alpha p gamma q .
An exact proof term for the current goal is L2 .
We will
prove PNoLt gamma q alpha p .
We will prove gamma ∈ alpha .
An exact proof term for the current goal is Lca .
We will
prove PNoEq_ gamma q p .
An exact proof term for the current goal is H6 .
We will prove p gamma .
An exact proof term for the current goal is H7 .
Assume H4 .
Apply H4 to the current goal.
rewrite the current goal using H4 (from right to left) at position 1.
An exact proof term for the current goal is Hc .
Assume H4 .
An exact proof term for the current goal is H4 .
∎
Proof: Let L, R and alpha be given.
Let beta be given.
Let p be given.
Apply H1 to the current goal.
Apply andI to the current goal.
∎
Proof: Let L and R be given.
Let alpha be given.
Let p be given.
Set p0 to be the term λdelta ⇒ p delta ∧ delta ≠ alpha of type set → prop .
Set p1 to be the term λdelta ⇒ p delta ∨ delta = alpha of type set → prop .
Apply Hp to the current goal.
Apply Hp0 to the current goal.
Apply Hp1 to the current goal.
We prove the intermediate claim Lnp0a : ¬ p0 alpha .
Assume H10 .
Apply H10 to the current goal.
Assume H11 : p alpha .
Assume H12 : alpha ≠ alpha .
Apply H12 to the current goal.
Use reflexivity.
We prove the intermediate claim Lp1a : p1 alpha .
We will prove p alpha ∨ alpha = alpha .
Apply orIR to the current goal.
Use reflexivity.
We prove the intermediate
claim Lap0p :
PNoLt (ordsucc alpha ) p0 alpha p .
We will
prove PNoEq_ alpha p0 p .
We will prove ¬ p0 alpha .
An exact proof term for the current goal is Lnp0a .
We prove the intermediate
claim Lapp1 :
PNoLt alpha p (ordsucc alpha ) p1 .
We will
prove PNoEq_ alpha p p1 .
We will prove p1 alpha .
An exact proof term for the current goal is Lp1a .
Apply andI to the current goal.
Let beta be given.
Let q be given.
An exact proof term for the current goal is Hq .
Apply Hp0a beta H10 q to the current goal.
An exact proof term for the current goal is L4 .
An exact proof term for the current goal is Lap0p .
We prove the intermediate
claim L6 :
∀gamma ∈ ordsucc alpha , gamma ∈ beta → PNoEq_ gamma p q → q gamma → p0 gamma .
Let gamma be given.
Assume H11 : q gamma .
Apply dneg to the current goal.
Assume HNC : ¬ p0 gamma .
We prove the intermediate
claim Lc :
ordinal gamma .
We prove the intermediate
claim L6a :
PNoLt gamma q beta q .
An exact proof term for the current goal is Hc2 .
We will
prove PNoEq_ gamma q q .
We will prove q gamma .
An exact proof term for the current goal is H11 .
We prove the intermediate
claim L6b :
PNo_downc L gamma q .
We will
prove ∃delta, ordinal delta ∧ ∃r : set → prop , L delta r ∧ PNoLe gamma q delta r .
We use
beta to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb .
We use q to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hq .
An exact proof term for the current goal is L6a .
We prove the intermediate
claim L6c :
PNoLt gamma q (ordsucc alpha ) p0 .
An exact proof term for the current goal is Hp0a gamma Hc1 q L6b .
We prove the intermediate
claim L6d :
PNoLt (ordsucc alpha ) p0 gamma q .
An exact proof term for the current goal is Hc1 .
We will
prove PNoEq_ gamma p0 q .
Apply PNoEq_tra_ gamma p0 p q to the current goal.
We will
prove PNoEq_ gamma p p0 .
Apply ordsuccE alpha gamma Hc1 to the current goal.
Assume H12 : gamma ∈ alpha .
We will
prove PNoEq_ alpha p p0 .
Assume H12 : gamma = alpha .
rewrite the current goal using H12 (from left to right).
We will
prove PNoEq_ alpha p p0 .
An exact proof term for the current goal is H10 .
We will prove ¬ p0 gamma .
An exact proof term for the current goal is HNC .
An
exact proof term for the current goal is
PNoLt_tra gamma (ordsucc alpha ) gamma Lc Lsa Lc q p0 q L6c L6d .
Assume H10 .
Apply H10 to the current goal.
Apply PNoLtE alpha beta p q H10 to the current goal.
Apply H11 to the current goal.
Let gamma be given.
Assume H12 .
Apply H12 to the current goal.
Assume H12 .
Apply H12 to the current goal.
Assume H12 .
Apply H12 to the current goal.
Assume H13 : ¬ p gamma .
Assume H14 : q gamma .
Assume Hc1 : gamma ∈ alpha .
Apply L6 gamma (ordsuccI1 alpha gamma Hc1 ) Hc2 H12 H14 to the current goal.
Assume H15 : p gamma .
Assume _ .
Apply H13 to the current goal.
An exact proof term for the current goal is H15 .
Assume H13 : q alpha .
Apply Lnp0a to the current goal.
We will prove p0 alpha .
An
exact proof term for the current goal is
L6 alpha (ordsuccI2 alpha ) H11 H12 H13 .
Assume _ _ .
Apply L5 to the current goal.
An exact proof term for the current goal is H11 .
Assume H10 .
Apply H10 to the current goal.
Apply L5 to the current goal.
rewrite the current goal using H10a (from right to left).
An exact proof term for the current goal is H10 .
Let beta be given.
Let q be given.
An exact proof term for the current goal is Hq .
An exact proof term for the current goal is Lapp1 .
Apply Hp1b beta H10 q to the current goal.
An exact proof term for the current goal is L4 .
We prove the intermediate
claim L6 :
∀gamma ∈ ordsucc alpha , gamma ∈ beta → PNoEq_ gamma q p → p1 gamma → q gamma .
Let gamma be given.
Assume H11 : p1 gamma .
Apply dneg to the current goal.
Assume HNC : ¬ q gamma .
We prove the intermediate
claim Lc :
ordinal gamma .
We prove the intermediate
claim L6a :
PNoLt beta q gamma q .
An exact proof term for the current goal is Hc2 .
We will
prove PNoEq_ gamma q q .
We will prove ¬ q gamma .
An exact proof term for the current goal is HNC .
We prove the intermediate
claim L6b :
PNo_upc R gamma q .
We will
prove ∃delta, ordinal delta ∧ ∃r : set → prop , R delta r ∧ PNoLe delta r gamma q .
We use
beta to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb .
We use q to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hq .
An exact proof term for the current goal is L6a .
We prove the intermediate
claim L6c :
PNoLt (ordsucc alpha ) p1 gamma q .
An exact proof term for the current goal is Hp1b gamma Hc1 q L6b .
We prove the intermediate
claim L6d :
PNoLt gamma q (ordsucc alpha ) p1 .
An exact proof term for the current goal is Hc1 .
We will
prove PNoEq_ gamma q p1 .
Apply PNoEq_tra_ gamma q p p1 to the current goal.
An exact proof term for the current goal is H10 .
We will
prove PNoEq_ gamma p p1 .
Apply ordsuccE alpha gamma Hc1 to the current goal.
Assume H12 : gamma ∈ alpha .
We will
prove PNoEq_ alpha p p1 .
Assume H12 : gamma = alpha .
rewrite the current goal using H12 (from left to right).
We will
prove PNoEq_ alpha p p1 .
We will prove p1 gamma .
An exact proof term for the current goal is H11 .
An
exact proof term for the current goal is
PNoLt_tra gamma (ordsucc alpha ) gamma Lc Lsa Lc q p1 q L6d L6c .
Assume H10 .
Apply H10 to the current goal.
Assume H10 .
An exact proof term for the current goal is H10 .
Assume H10 .
Apply H10 to the current goal.
Apply L5 to the current goal.
rewrite the current goal using H10a (from right to left).
Apply PNoLtE beta alpha q p H10 to the current goal.
Apply H11 to the current goal.
Let gamma be given.
Assume H12 .
Apply H12 to the current goal.
Assume H12 .
Apply H12 to the current goal.
Assume H12 .
Apply H12 to the current goal.
Assume H13 : ¬ q gamma .
Assume H14 : p gamma .
Assume Hc1 : gamma ∈ alpha .
Apply H13 to the current goal.
Apply L6 gamma (ordsuccI1 alpha gamma Hc1 ) Hc2 H12 to the current goal.
We will prove p1 gamma .
We will prove p gamma ∨ gamma = alpha .
Apply orIL to the current goal.
An exact proof term for the current goal is H14 .
Assume _ _ .
Apply L5 to the current goal.
An exact proof term for the current goal is H11 .
Assume H13 : ¬ q alpha .
Apply H13 to the current goal.
An
exact proof term for the current goal is
L6 alpha (ordsuccI2 alpha ) H11 H12 Lp1a .
∎
Proof: Let L and R be given.
Assume HLR .
Let alpha be given.
Assume Ha .
Assume HaL HaR .
Let beta be given.
Assume H1 .
Apply H1 to the current goal.
Assume H1 .
Apply H1 to the current goal.
Let p be given.
We use
beta to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb .
We use p to witness the existential quantifier.
∎
Definition. We define
PNo_least_rep2 to be
λL R beta p ⇒ PNo_least_rep L R beta p ∧ ∀x, x ∉ beta → ¬ p x of type
(set → (set → prop ) → prop ) → (set → (set → prop ) → prop ) → set → (set → prop ) → prop .
Proof: Let L and R be given.
Assume HLR .
Let alpha be given.
Assume Ha .
Let p and q be given.
Assume Hp .
Assume Hq .
Apply Ha to the current goal.
Assume Ha1 _ .
Apply Hp to the current goal.
Assume Hp1 .
Apply Hp1 to the current goal.
Assume _ .
Apply Hp1 to the current goal.
Apply Hq to the current goal.
Let beta be given.
We prove the intermediate
claim Lbpq :
PNoEq_ beta p q .
Let gamma be given.
An
exact proof term for the current goal is
IH gamma Hc (Ha1 beta Hb2 gamma Hc ) .
Apply iffI to the current goal.
Apply dneg to the current goal.
We prove the intermediate
claim Lqp :
PNoLt beta q alpha p .
We will
prove beta ∈ alpha .
An exact proof term for the current goal is Hb2 .
An exact proof term for the current goal is Lbpq .
An exact proof term for the current goal is H1 .
We prove the intermediate
claim Lqq :
PNoLt alpha q beta q .
We will
prove beta ∈ alpha .
An exact proof term for the current goal is Hb2 .
An exact proof term for the current goal is H2 .
Apply Hp2 beta Hb2 q to the current goal.
Apply andI to the current goal.
Let gamma be given.
Let r be given.
Assume Hr : L gamma r .
Apply PNoLt_tra gamma alpha beta Hc Ha Hb1 r q q to the current goal.
We will
prove PNoLt gamma r alpha q .
An exact proof term for the current goal is Hq1 gamma Hc r Hr .
An exact proof term for the current goal is Lqq .
Let gamma be given.
Let r be given.
Assume Hr : R gamma r .
Apply PNoLt_tra beta alpha gamma Hb1 Ha Hc q p r to the current goal.
An exact proof term for the current goal is Lqp .
We will
prove PNoLt alpha p gamma r .
An exact proof term for the current goal is Hp1b gamma Hc r Hr .
Apply dneg to the current goal.
We prove the intermediate
claim Lpq :
PNoLt alpha p beta q .
We will
prove beta ∈ alpha .
An exact proof term for the current goal is Hb2 .
An exact proof term for the current goal is Lbpq .
An exact proof term for the current goal is H2 .
We prove the intermediate
claim Lqq :
PNoLt beta q alpha q .
We will
prove beta ∈ alpha .
An exact proof term for the current goal is Hb2 .
An exact proof term for the current goal is H1 .
Apply Hp2 beta Hb2 q to the current goal.
Apply andI to the current goal.
Let gamma be given.
Let r be given.
Assume Hr : L gamma r .
Apply PNoLt_tra gamma alpha beta Hc Ha Hb1 r p q to the current goal.
We will
prove PNoLt gamma r alpha p .
An exact proof term for the current goal is Hp1a gamma Hc r Hr .
An exact proof term for the current goal is Lpq .
Let gamma be given.
Let r be given.
Assume Hr : R gamma r .
Apply PNoLt_tra beta alpha gamma Hb1 Ha Hc q q r to the current goal.
An exact proof term for the current goal is Lqq .
We will
prove PNoLt alpha q gamma r .
An exact proof term for the current goal is Hq2 gamma Hc r Hr .
Let beta be given.
∎
Proof: Let L and R be given.
Assume HLR .
Let alpha be given.
Assume Ha HaL HaR .
Let beta be given.
Assume H1 .
Apply H1 to the current goal.
Assume H1 .
Apply H1 to the current goal.
Let p be given.
We use
beta to
witness the existential quantifier.
Apply andI to the current goal.
We use p to witness the existential quantifier.
An exact proof term for the current goal is Hp .
Apply L1 to the current goal.
Let beta be given.
Assume H1 .
Apply H1 to the current goal.
Assume H1 .
Apply H1 to the current goal.
Apply H2 to the current goal.
Let p be given.
We use
beta to
witness the existential quantifier.
Apply andI to the current goal.
We use
(λx ⇒ x ∈ beta ∧ p x ) to
witness the existential quantifier.
Apply andI to the current goal.
Apply and3I to the current goal.
An exact proof term for the current goal is H1 .
Let x be given.
We will
prove p x ↔ x ∈ beta ∧ p x .
Apply iffI to the current goal.
Assume H4 .
Apply andI to the current goal.
An exact proof term for the current goal is Hx .
An exact proof term for the current goal is H4 .
Assume H4 .
Apply H4 to the current goal.
Assume _ H5 .
An exact proof term for the current goal is H5 .
An exact proof term for the current goal is Hp .
Let gamma be given.
Let q be given.
Apply H3 gamma Hc to the current goal.
We use q to witness the existential quantifier.
An exact proof term for the current goal is H4 .
We will
prove ∀x, x ∉ beta → ¬ (x ∈ beta ∧ p x ) .
Let x be given.
Assume Hx .
Assume H4 .
Apply H4 to the current goal.
Assume H5 _ .
An exact proof term for the current goal is Hx H5 .
Let q and r be given.
Apply Hq to the current goal.
Assume Hq1 Hq2 .
Apply Hr to the current goal.
Assume Hr1 Hr2 .
We will prove q = r .
Let x be given.
Apply xm (x ∈ beta ) to the current goal.
We will prove q x ↔ r x .
Apply Hr1 to the current goal.
Assume Hr1a .
Apply Hr1a to the current goal.
Assume _ .
Assume _ .
Apply iffI to the current goal.
Assume H5 : q x .
Apply Hq2 x H4 to the current goal.
An exact proof term for the current goal is H5 .
Assume H5 : r x .
Apply Hr2 x H4 to the current goal.
An exact proof term for the current goal is H5 .
∎
Proof: Let L and R be given.
Assume HLR .
Let alpha be given.
Assume Ha HaL HaR .
∎
Proof: Let L and R be given.
Assume HLR .
Let alpha be given.
Assume Ha HaL HaR .
Assume H _ .
An exact proof term for the current goal is H .
∎
Theorem. (
PNo_bd_In ) The following is provable:
Proof: Let L and R be given.
Assume HLR .
Let alpha be given.
Assume Ha HaL HaR .
Apply PNo_bd_pred L R HLR alpha Ha HaL HaR to the current goal.
Assume H1 .
Apply H1 to the current goal.
Let beta be given.
Assume H4 .
Apply H4 to the current goal.
Assume H4 .
Apply H4 to the current goal.
Let p be given.
An exact proof term for the current goal is H4 .
We prove the intermediate
claim Lb :
beta ∈ PNo_bd L R .
Apply H4 to the current goal.
An exact proof term for the current goal is Hb .
Apply H3 beta Lb p to the current goal.
An exact proof term for the current goal is Hp .
∎