Primitive . 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
Primitive . 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 .
Primitive . The name
Empty is a term of type
set .
Axiom. (
EmptyAx ) We take the following as an axiom:
Primitive . The name
⋃ is a term of type
set → set .
Axiom. (
UnionEq ) We take the following as an axiom:
Primitive . 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
Primitive . 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 .
Primitive . 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:
Axiom. (
andER ) We take the following as an axiom:
Axiom. (
orIL ) We take the following as an axiom:
Axiom. (
orIR ) We take the following as an axiom:
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:
Axiom. (
or3I2 ) We take the following as an axiom:
Axiom. (
or3I3 ) We take the following as an axiom:
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. (
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:
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:
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:
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:
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:
Axiom. (
dneg ) We take the following as an axiom:
Axiom. (
eq_or_nand ) We take the following as an axiom:
Primitive . 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 ) 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
Primitive . 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_0 ) We take the following as an axiom:
Axiom. (
If_i_1 ) We take the following as an axiom:
Axiom. (
If_i_or ) We take the following as an axiom:
Primitive . 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:
Axiom. (
UPairI2 ) We take the following as an axiom:
Primitive . 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:
Axiom. (
SingE ) We take the following as an axiom:
∀x y : set , y ∈ { x } → y = x
Primitive . 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 ) We take the following as an axiom:
∀X Y : set , X ∪ Y = Y ∪ X
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.
Primitive . 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 )
Primitive . 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
Primitive . 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
Primitive . 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
Primitive . 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. (
In_irref ) We take the following as an axiom:
Axiom. (
In_no2cycle ) We take the following as an axiom:
Primitive . 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:
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:
Axiom. (
In_0_2 ) We take the following as an axiom:
Axiom. (
In_1_2 ) We take the following as an axiom:
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_p_trans ) We take the following as an axiom:
Axiom. (
nat_trans ) We take the following as an axiom:
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:
Axiom. (
neq_1_0 ) We take the following as an axiom:
Axiom. (
neq_0_2 ) We take the following as an axiom:
Axiom. (
neq_2_0 ) We take the following as an axiom:
Axiom. (
neq_1_2 ) We take the following as an axiom:
Axiom. (
ZF_closed_E ) We take the following as an axiom:
Primitive . 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:
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
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
Primitive . The name
inv is a term of type
set → (set → set ) → set → set .
Axiom. (
surj_rinv ) We take the following as an axiom:
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
End of Section SchroederBernstein
Beginning of Section PigeonHole
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:
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
Primitive . 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
Primitive . 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
Primitive . 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
Primitive . 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
Primitive . 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
Primitive . 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 )
Primitive . 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 )
Primitive . 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:
Axiom. (
add_nat_SR ) We take the following as an axiom:
Axiom. (
add_nat_p ) We take the following as an axiom:
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:
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
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:
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:
Axiom. (
Unj_eq ) We take the following as an axiom:
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:
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_0_0 ) We take the following as an axiom:
Beginning of Section pair_setsum
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:
Axiom. (
proj0E ) We take the following as an axiom:
Axiom. (
proj1I ) We take the following as an axiom:
Axiom. (
proj1E ) We take the following as an axiom:
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. (
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 ).
Notation . We now use n-tuple notation (
a0 ,...,
an-1 ) for n ≥ 2 for λ i ∈
n .
if i = 0
then a0 else ... if i =
n-2 then an-2 else an-1 .
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. (
lamI2 ) We take the following as an axiom:
Beginning of Section Tuples
Variable x0 x1 : set
End of Section Tuples
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 .
Primitive . The name
DescrR_i_io_1 is a term of type
(set → (set → prop ) → prop ) → set .
Primitive . The name
DescrR_i_io_2 is a term of type
(set → (set → prop ) → prop ) → set → prop .
Definition. We define
PNoEq_ to be
λalpha p q ⇒ ∀ beta ∈ alpha , p beta ↔ q beta of type
set → (set → prop ) → (set → prop ) → prop .
Axiom. (
PNoEq_ref_ ) We take the following as an axiom:
∀alpha, ∀p : set → prop , PNoEq_ alpha p p
Axiom. (
PNoEq_sym_ ) We take the following as an axiom:
∀alpha, ∀p q : set → prop , PNoEq_ alpha p q → PNoEq_ alpha q p
Axiom. (
PNoEq_tra_ ) We take the following as an axiom:
Axiom. (
PNoLt_E_ ) We take the following as an axiom:
Axiom. (
PNoLt_irref_ ) We take the following as an axiom:
∀alpha, ∀p : set → prop , ¬ PNoLt_ alpha p p
Axiom. (
PNoLt_mon_ ) We take the following as an axiom:
Axiom. (
PNoLt_tra_ ) We take the following as an axiom:
Primitive . The name
PNoLt is a term of type
set → (set → prop ) → set → (set → prop ) → prop .
Axiom. (
PNoLtI1 ) We take the following as an axiom:
Axiom. (
PNoLtI2 ) We take the following as an axiom:
Axiom. (
PNoLtI3 ) We take the following as an axiom:
Axiom. (
PNoLtE ) We take the following as an axiom:
Axiom. (
PNoLt_irref ) We take the following as an axiom:
∀alpha, ∀p : set → prop , ¬ PNoLt alpha p alpha p
Axiom. (
PNoLtEq_tra ) We take the following as an axiom:
Axiom. (
PNoEqLt_tra ) We take the following as an axiom:
Axiom. (
PNoLt_tra ) We take the following as an axiom:
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 .
Axiom. (
PNoLeI1 ) We take the following as an axiom:
Axiom. (
PNoLeI2 ) We take the following as an axiom:
∀alpha, ∀p q : set → prop , PNoEq_ alpha p q → PNoLe alpha p alpha q
Axiom. (
PNoLe_ref ) We take the following as an axiom:
∀alpha, ∀p : set → prop , PNoLe alpha p alpha p
Axiom. (
PNoLtLe_tra ) We take the following as an axiom:
Axiom. (
PNoLeLt_tra ) We take the following as an axiom:
Axiom. (
PNoEqLe_tra ) We take the following as an axiom:
Axiom. (
PNoLe_tra ) We take the following as an axiom:
Axiom. (
PNoLe_downc ) We take the following as an axiom:
Axiom. (
PNo_downc_ref ) We take the following as an axiom:
∀L : set → (set → prop ) → prop , ∀alpha, ordinal alpha → ∀p : set → prop , L alpha p → PNo_downc L alpha p
Axiom. (
PNo_upc_ref ) We take the following as an axiom:
∀R : set → (set → prop ) → prop , ∀alpha, ordinal alpha → ∀p : set → prop , R alpha p → PNo_upc R alpha p
Axiom. (
PNoLe_upc ) We take the following as an axiom:
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 .
Axiom. (
PNo_extend0_eq ) We take the following as an axiom:
∀alpha, ∀p : set → prop , PNoEq_ alpha p (λdelta ⇒ p delta ∧ delta ≠ alpha )
Axiom. (
PNo_extend1_eq ) We take the following as an axiom:
∀alpha, ∀p : set → prop , PNoEq_ alpha p (λdelta ⇒ p delta ∨ delta = alpha )
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 .
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 .
Primitive . The name
PNo_bd is a term of type
(set → (set → prop ) → prop ) → (set → (set → prop ) → prop ) → set .
Primitive . The name
PNo_pred is a term of type
(set → (set → prop ) → prop ) → (set → (set → prop ) → prop ) → set → prop .
Axiom. (
PNo_bd_pred ) We take the following as an axiom:
Axiom. (
PNo_bd_In ) We take the following as an axiom:
Beginning of Section TaggedSets
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
tag .
Proof:
We prove the intermediate
claim L1 :
0 ∈ { 1 } .
An
exact proof term for the current goal is
SingE 1 0 L1 .
∎
Proof: Assume H1 .
Apply H1 to the current goal.
Assume H2 _ .
∎
Proof: Let y be given.
We prove the intermediate
claim L1 :
{ 1 } ∈ y ' .
An
exact proof term for the current goal is
SingI { 1 } .
∎
Proof: Let alpha and y be given.
Assume H1 H2 .
An
exact proof term for the current goal is
ordinal_Hered alpha H1 (y ' ) H2 .
∎
Proof: Let alpha and beta be given.
Assume Ha He .
Let gamma be given.
We prove the intermediate
claim L1 :
gamma ∈ beta ' .
rewrite the current goal using He (from right to left).
We will
prove gamma ∈ alpha ∪ { { 1 } } .
An exact proof term for the current goal is Hc .
An exact proof term for the current goal is H1 .
rewrite the current goal using
SingE { 1 } gamma H1 (from right to left).
An
exact proof term for the current goal is
ordinal_Hered alpha Ha gamma Hc .
∎
Proof: Let alpha and beta be given.
Assume Ha Hb He .
∎
Proof: Let alpha and beta be given.
Assume Ha Hb .
Let gamma be given.
We prove the intermediate
claim L2 :
beta = gamma .
rewrite the current goal using L2 (from left to right).
An exact proof term for the current goal is H2 .
∎
Proof: Let alpha and Y be given.
Let y be given.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is H1 .
∎
Definition. We define
SNoElts_ to be
λalpha ⇒ alpha ∪ { beta ' | beta ∈ alpha } of type
set → set .
Proof: Let alpha and beta be given.
Let x be given.
Apply binunionE alpha { gamma ' | gamma ∈ alpha } x H2 to the current goal.
Apply H1 to the current goal.
An exact proof term for the current goal is H3 .
Apply ReplE_impred alpha (λgamma ⇒ gamma ' ) x H3 to the current goal.
Let gamma be given.
rewrite the current goal using H5 (from left to right).
An
exact proof term for the current goal is
ReplI beta (λgamma ⇒ gamma ' ) gamma (H1 gamma H4 ) .
∎
Proof: Let alpha be given.
Let p be given.
Let beta be given.
Apply iffI to the current goal.
An
exact proof term for the current goal is
SepE2 alpha p beta H2 .
Let gamma be given.
We will
prove gamma ' ∈ alpha .
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is Hb .
Apply SepI to the current goal.
An exact proof term for the current goal is Hb .
An exact proof term for the current goal is H1 .
∎
Theorem. (
SNo_PSNo ) The following is provable:
Proof: Let alpha be given.
Assume Ha .
Let p be given.
Apply andI to the current goal.
Let u be given.
Apply SepE alpha p u H1 to the current goal.
Assume H3 : p u .
An exact proof term for the current goal is H2 .
Let beta be given.
rewrite the current goal using H4 (from left to right).
An
exact proof term for the current goal is
ReplI alpha (λbeta ⇒ beta ' ) beta H2 .
Let beta be given.
Apply xm (p beta ) to the current goal.
Apply SepE alpha p (beta ' ) H4 to the current goal.
Let gamma be given.
We prove the intermediate
claim Lgamma :
ordinal gamma .
An
exact proof term for the current goal is
ordinal_Hered alpha Ha gamma H5 .
We prove the intermediate
claim L1 :
beta = gamma .
An
exact proof term for the current goal is
tagged_eqE_eq beta gamma Lbeta Lgamma H7 .
Apply H6 to the current goal.
We will prove p gamma .
rewrite the current goal using L1 (from right to left).
An exact proof term for the current goal is H2 .
An
exact proof term for the current goal is
SepI alpha p beta H1 H2 .
Apply SepE alpha p beta H4 to the current goal.
An exact proof term for the current goal is H2 H6 .
Let gamma be given.
rewrite the current goal using H7 (from right to left).
An exact proof term for the current goal is Lbeta .
∎
Proof: Let alpha and x be given.
Assume Ha Hx .
Apply Hx to the current goal.
Let u be given.
Apply SepI to the current goal.
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is Hu .
Let beta be given.
rewrite the current goal using H3 (from left to right).
We prove the intermediate
claim L2 :
beta ∉ x .
An exact proof term for the current goal is H6 H4 .
Apply H4 to the current goal.
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is Hu .
Let u be given.
Apply SepE alpha (λbeta ⇒ beta ∈ x ) u H1 to the current goal.
An exact proof term for the current goal is H3 .
Let beta be given.
rewrite the current goal using H4 (from left to right).
An exact proof term for the current goal is H5 .
An exact proof term for the current goal is H3 H5 .
∎
Definition. We define
SNo to be
λx ⇒ ∃ alpha, ordinal alpha ∧ SNo_ alpha x of type
set → prop .
Theorem. (
SNo_SNo ) The following is provable:
Proof: Let alpha be given.
Assume Ha .
Let z be given.
We use alpha to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha .
An exact proof term for the current goal is Hz .
∎
Proof: Let x, alpha and beta be given.
Assume Ha Hb Hax Hbx .
Let gamma be given.
We will
prove gamma ∈ beta .
Apply Hax to the current goal.
Assume Hax1 Hax2 .
Apply Hbx to the current goal.
Assume Hbx1 Hbx2 .
We prove the intermediate
claim Lc :
ordinal gamma .
An
exact proof term for the current goal is
ordinal_Hered alpha Ha gamma Hc .
An
exact proof term for the current goal is
Hbx1 (gamma ' ) H1 .
Apply L2 to the current goal.
An exact proof term for the current goal is Hbx1 gamma H1 .
We prove the intermediate
claim L2 :
gamma ∈ beta ∨ gamma ∈ { delta ' | delta ∈ beta } .
Apply L2 to the current goal.
An exact proof term for the current goal is H2 .
∎
Proof: Let x, alpha and beta be given.
Assume Ha Hb Hax Hbx .
∎
Proof: Let x be given.
Assume Hx .
Assume H1 _ .
An exact proof term for the current goal is H1 .
∎
Theorem. (
SNoLev_ ) The following is provable:
Proof: Let x be given.
Assume Hx .
Assume _ H1 .
An exact proof term for the current goal is H1 .
∎
Proof: Let x be given.
Assume Hx .
An exact proof term for the current goal is Hx1 .
An exact proof term for the current goal is Hx2 .
∎
Proof: Let alpha be given.
Let p be given.
We prove the intermediate
claim L1 :
SNo_ alpha (PSNo alpha p ) .
An
exact proof term for the current goal is
SNo_PSNo alpha Ha p .
We prove the intermediate
claim L2 :
SNo (PSNo alpha p ) .
We use alpha to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha .
An exact proof term for the current goal is L1 .
∎
Theorem. (
SNo_Subq ) The following is provable:
Proof: Let x and y be given.
Assume Hx Hy H1 H2 .
Apply SNoLev_ x Hx to the current goal.
Apply SNoLev_ y Hy to the current goal.
Let u be given.
An exact proof term for the current goal is Hx2a u Hu .
Apply H2 u H3 to the current goal.
Assume H4 _ .
An exact proof term for the current goal is H4 Hu .
Let beta be given.
An
exact proof term for the current goal is
H1 beta H4 .
rewrite the current goal using H5 (from left to right).
An exact proof term for the current goal is H6 .
Apply H9 to the current goal.
Apply H2 beta H4 to the current goal.
Assume _ H10 .
An exact proof term for the current goal is H10 H7 .
Apply H8 to the current goal.
rewrite the current goal using H5 (from right to left).
An exact proof term for the current goal is Hu .
∎
Definition. We define
SNoEq_ to be
λalpha x y ⇒ PNoEq_ alpha (λbeta ⇒ beta ∈ x ) (λbeta ⇒ beta ∈ y ) of type
set → set → set → prop .
Theorem. (
SNoEq_I ) The following is provable:
Proof: Let alpha, x and y be given.
Assume Hxy .
An exact proof term for the current goal is Hxy .
∎
Theorem. (
SNo_eq ) The following is provable:
Proof: Let x and y be given.
Assume Hx Hy H1 H2 .
Apply SNo_Subq x y Hx Hy to the current goal.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is H2 .
Apply SNo_Subq y x Hy Hx to the current goal.
rewrite the current goal using H1 (from left to right).
Let alpha be given.
We will
prove alpha ∈ y ↔ alpha ∈ x .
We will
prove alpha ∈ x ↔ alpha ∈ y .
Apply H2 alpha to the current goal.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is H3 .
∎
End of Section TaggedSets
Notation . We use
< as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLt .
Notation . We use
≤ as an infix operator with priority 490 and no associativity corresponding to applying term
SNoLe .
Theorem. (
SNoLtLe ) The following is provable:
Proof: Let x and y be given.
Assume H1 .
An exact proof term for the current goal is H1 .
∎
Theorem. (
SNoLeE ) The following is provable:
Proof: Let x and y be given.
Assume Hx Hy .
Apply H1 to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is H2 .
Assume H2 .
Apply H2 to the current goal.
Apply orIR to the current goal.
An
exact proof term for the current goal is
SNo_eq x y Hx Hy H2 H3 .
∎
Proof: Let alpha, x and y be given.
∎
Proof: Let alpha, x, y and z be given.
∎
Theorem. (
SNoLtE ) The following is provable:
Proof: Let x and y be given.
Let p be given.
Assume Hp1 Hp2 Hp3 .
An exact proof term for the current goal is Hx .
An exact proof term for the current goal is Hy .
Let alpha be given.
We prove the intermediate
claim La :
ordinal alpha .
Set z to be the term
PSNo alpha (λbeta ⇒ beta ∈ x ) .
We prove the intermediate
claim L1 :
SNo_ alpha z .
An exact proof term for the current goal is La .
We prove the intermediate
claim L2 :
SNo z .
We use alpha to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is La .
An exact proof term for the current goal is L1 .
We prove the intermediate
claim L3 :
SNoLev z = alpha .
An
exact proof term for the current goal is
SNoLev_uniq z (SNoLev z ) alpha Hz1 La Hz2 L1 .
We prove the intermediate
claim L4 :
SNoEq_ alpha z x .
An exact proof term for the current goal is La .
We prove the intermediate
claim L5 :
SNoEq_ alpha z y .
Apply SNoEq_tra_ alpha z x y L4 to the current goal.
We will
prove SNoEq_ alpha x y .
An exact proof term for the current goal is H2 .
Apply Hp1 z L2 to the current goal.
rewrite the current goal using L3 (from left to right).
An exact proof term for the current goal is Ha .
rewrite the current goal using L3 (from left to right).
An exact proof term for the current goal is L4 .
rewrite the current goal using L3 (from left to right).
An exact proof term for the current goal is L5 .
rewrite the current goal using L3 (from left to right).
An exact proof term for the current goal is Ha1 .
An exact proof term for the current goal is L4 .
An exact proof term for the current goal is H3 .
rewrite the current goal using L3 (from left to right).
An exact proof term for the current goal is Ha2 .
An exact proof term for the current goal is L5 .
An exact proof term for the current goal is H4 .
rewrite the current goal using L3 (from left to right).
An exact proof term for the current goal is H3 .
rewrite the current goal using L3 (from left to right).
An exact proof term for the current goal is H4 .
Apply Hp2 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 .
Apply Hp3 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. (
SNoLtI2 ) The following is provable:
Proof: Let x and y be given.
Assume H1 H2 H3 .
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. (
SNoLtI3 ) The following is provable:
Proof: Let x and y be given.
Assume H1 H2 H3 .
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 .
∎
Proof: Let x and y be given.
Assume Hx Hy .
Assume H1 .
Apply H1 to the current goal.
Assume H1 .
Apply or3I1 to the current goal.
An exact proof term for the current goal is H1 .
Assume H1 .
Apply H1 to the current goal.
Apply or3I2 to the current goal.
An
exact proof term for the current goal is
SNo_eq x y Hx Hy H2 H3 .
Assume H1 .
Apply or3I3 to the current goal.
An exact proof term for the current goal is H1 .
∎
Proof: Let x and y be given.
Assume Hx Hy .
Let p be given.
Assume Hp1 Hp2 Hp3 .
Assume H .
Apply H to the current goal.
An exact proof term for the current goal is Hp1 .
An exact proof term for the current goal is Hp2 .
An exact proof term for the current goal is Hp3 .
∎
Theorem. (
SNoLt_tra ) The following is provable:
Proof: Let x, y and z be given.
Assume Hx Hy Hz Hxy Hyz .
∎
Theorem. (
SNoLe_ref ) The following is provable:
Proof: Let x and y be given.
Assume Hx Hy Hxy Hyx .
An
exact proof term for the current goal is
SNo_eq x y Hx Hy H1 H2 .
∎
Proof: Let x, y and z be given.
Assume Hx Hy Hz Hxy Hyz .
∎
Proof: Let x, y and z be given.
Assume Hx Hy Hz Hxy Hyz .
∎
Theorem. (
SNoLe_tra ) The following is provable:
Proof: Let x, y and z be given.
Assume Hx Hy Hz Hxy Hyz .
∎
Proof: Let x and y be given.
Assume Hx Hy .
Assume H1 .
Apply H1 to the current goal.
Apply orIL to the current goal.
An exact proof term for the current goal is H1 .
Apply orIR to the current goal.
rewrite the current goal using H1 (from left to right).
Apply orIR to the current goal.
An exact proof term for the current goal is H1 .
∎
Proof: Let alpha, beta, p and q be given.
Assume Ha Hb .
rewrite the current goal using
SNoLev_PSNo alpha Ha p (from left to right).
We will
prove PNoEq_ alpha p (λgamma ⇒ gamma ∈ PSNo alpha p ) .
An exact proof term for the current goal is Ha .
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is Hb .
∎
Proof: Let alpha, beta, p and q be given.
Assume Ha Hb .
rewrite the current goal using
SNoLev_PSNo alpha Ha p (from left to right).
We will
prove PNoEq_ alpha (λgamma ⇒ gamma ∈ PSNo alpha p ) p .
An exact proof term for the current goal is Ha .
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is Hb .
∎
Proof: Let L and R be given.
Apply HC to the current goal.
Assume HC .
Apply HC to the current goal.
Set L' to be the term
λalpha p ⇒ ordinal alpha ∧ PSNo alpha p ∈ L of type
set → (set → prop ) → prop .
Set R' to be the term
λalpha p ⇒ ordinal alpha ∧ PSNo alpha p ∈ R of type
set → (set → prop ) → prop .
Set tau to be the term
PNo_bd L' R' .
We prove the intermediate
claim LLR :
PNoLt_pwise L' R' .
Let gamma be given.
Let p be given.
Assume H1 : L' gamma p .
Apply H1 to the current goal.
Assume _ H1 .
Let delta be given.
Let q be given.
Assume H2 : R' delta q .
Apply H2 to the current goal.
Assume _ H2 .
We will
prove PNoLt gamma p delta q .
An
exact proof term for the current goal is
HLR (PSNo gamma p ) H1 (PSNo delta q ) H2 .
We prove the intermediate
claim La :
ordinal alpha .
Let x be given.
An exact proof term for the current goal is HL x Hx .
Let y be given.
An exact proof term for the current goal is HR y Hy .
We prove the intermediate
claim Lab :
ordinal (alpha ∪ beta ) .
Assume H1 .
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is Lb .
Assume H1 .
rewrite the current goal using
binunion_com (from left to right).
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is La .
Let gamma be given.
Let p be given.
Assume H1 .
Apply H1 to the current goal.
We will
prove gamma ∈ alpha ∪ beta .
We will
prove PSNo gamma p ∈ L .
An exact proof term for the current goal is H2 .
rewrite the current goal using
SNoLev_PSNo gamma H1 p (from left to right).
Let gamma be given.
Let p be given.
Assume H1 .
Apply H1 to the current goal.
We will
prove gamma ∈ alpha ∪ beta .
We will
prove PSNo gamma p ∈ R .
An exact proof term for the current goal is H2 .
rewrite the current goal using
SNoLev_PSNo gamma H1 p (from left to right).
Assume H1 .
Apply H1 to the current goal.
Apply H2 to the current goal.
We prove the intermediate
claim LNoC :
SNo (SNoCut L R ) .
We use tau to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is H1 .
We prove the intermediate
claim LLleveqtau :
SNoLev (SNoCut L R ) = tau .
We prove the intermediate
claim LLbdtau :
tau ∈ ordsucc (alpha ∪ beta ) .
An
exact proof term for the current goal is
PNo_bd_In L' R' LLR (alpha ∪ beta ) Lab LLab LRab .
rewrite the current goal using LLleveqtau (from left to right).
An exact proof term for the current goal is LLbdtau .
We prove the intermediate
claim LLecw :
PNoEq_ tau (λgamma ⇒ gamma ∈ SNoCut L R ) w .
We will
prove PNoEq_ tau (λgamma ⇒ gamma ∈ PSNo tau w ) w .
An
exact proof term for the current goal is
PNoEq_PSNo tau H1 w .
An exact proof term for the current goal is LNoC .
We prove the intermediate
claim LL :
∀ x ∈ L , x < SNoCut L R .
Let x be given.
We will
prove x < PSNo tau w .
We prove the intermediate
claim L1 :
SNo x .
An exact proof term for the current goal is HL x Hx .
We prove the intermediate
claim L2 :
x = PSNo (SNoLev x ) (λgamma ⇒ gamma ∈ x ) .
An exact proof term for the current goal is L1 .
We prove the intermediate
claim L3 :
L' (SNoLev x ) (λgamma ⇒ gamma ∈ x ) .
Apply andI to the current goal.
An exact proof term for the current goal is LLx .
rewrite the current goal using L2 (from right to left).
An exact proof term for the current goal is Hx .
We will
prove x < PSNo tau w .
rewrite the current goal using L2 (from left to right).
An
exact proof term for the current goal is
H4 (SNoLev x ) LLx (λgamma ⇒ gamma ∈ x ) L3 .
We prove the intermediate
claim LR :
∀ y ∈ R , SNoCut L R < y .
Let y be given.
We will
prove PSNo tau w < y .
We prove the intermediate
claim L1 :
SNo y .
An exact proof term for the current goal is HR y Hy .
We prove the intermediate
claim L2 :
y = PSNo (SNoLev y ) (λgamma ⇒ gamma ∈ y ) .
An exact proof term for the current goal is L1 .
We prove the intermediate
claim L3 :
R' (SNoLev y ) (λgamma ⇒ gamma ∈ y ) .
Apply andI to the current goal.
An exact proof term for the current goal is LLy .
rewrite the current goal using L2 (from right to left).
An exact proof term for the current goal is Hy .
We will
prove PSNo tau w < y .
rewrite the current goal using L2 (from left to right).
An
exact proof term for the current goal is
H5 (SNoLev y ) LLy (λgamma ⇒ gamma ∈ y ) L3 .
Apply and5I to the current goal.
An exact proof term for the current goal is LNoC .
An exact proof term for the current goal is LLbd .
An exact proof term for the current goal is LL .
An exact proof term for the current goal is LR .
Let z be given.
An exact proof term for the current goal is Hz .
Apply andI to the current goal.
Let gamma be given.
Let q be given.
Assume Hq : L' gamma q .
We will
prove PNoLt gamma q (SNoLev z ) (λgamma ⇒ gamma ∈ z ) .
Apply Hq to the current goal.
rewrite the current goal using
SNo_PSNo_eta z Hz (from right to left).
We will
prove PSNo gamma q < z .
An
exact proof term for the current goal is
H10 (PSNo gamma q ) Hq2 .
Let gamma be given.
Let q be given.
Assume Hq : R' gamma q .
We will
prove PNoLt (SNoLev z ) (λgamma ⇒ gamma ∈ z ) gamma q .
Apply Hq to the current goal.
rewrite the current goal using
SNo_PSNo_eta z Hz (from right to left).
We will
prove z < PSNo gamma q .
An
exact proof term for the current goal is
H11 (PSNo gamma q ) Hq2 .
We prove the intermediate
claim LLznt :
SNoLev z ∉ tau .
An
exact proof term for the current goal is
H3 (SNoLev z ) H12 (λgamma ⇒ gamma ∈ z ) Lzimv .
We prove the intermediate
claim LLzlet :
tau ⊆ SNoLev z .
An exact proof term for the current goal is LLznt H12 .
Assume H12 .
An exact proof term for the current goal is H12 .
rewrite the current goal using LLleveqtau (from left to right).
Apply andI to the current goal.
An exact proof term for the current goal is LLzlet .
We will
prove PNoEq_ tau (λgamma ⇒ gamma ∈ SNoCut L R ) (λgamma ⇒ gamma ∈ z ) .
Assume H12 .
Apply H12 to the current goal.
Apply H12 to the current goal.
Let delta be given.
Assume H13 .
Apply H13 to the current goal.
Assume H13 .
Apply H13 to the current goal.
Assume H13 .
Apply H13 to the current goal.
We prove the intermediate
claim Ld :
ordinal delta .
An
exact proof term for the current goal is
ordinal_Hered tau H1 delta Hd .
Set z0 to be the term
λeps ⇒ eps ∈ z ∧ eps ≠ delta of type
set → prop .
Set z1 to be the term
λeps ⇒ eps ∈ z ∨ eps = delta of type
set → prop .
We prove the intermediate
claim Lnz0d :
¬ z0 delta .
Assume H10 .
Apply H10 to the current goal.
Apply H12 to the current goal.
Use reflexivity.
We prove the intermediate claim Lz1d : z1 delta .
We will
prove delta ∈ z ∨ delta = delta .
Apply orIR to the current goal.
Use reflexivity.
Apply H3 delta Hd (λgamma ⇒ gamma ∈ z ) to the current goal.
Apply andI to the current goal.
Let eps be given.
Apply ordsuccE delta eps He to the current goal.
Apply iff_trans (w eps ) (eps ∈ z ) (z0 eps ) to the current goal.
An exact proof term for the current goal is H13 eps He1 .
An
exact proof term for the current goal is
PNo_extend0_eq delta (λgamma ⇒ gamma ∈ z ) eps He1 .
We will
prove w eps ↔ z0 eps .
rewrite the current goal using He1 (from left to right).
We will
prove w delta ↔ z0 delta .
Apply iffI to the current goal.
Assume H16 : w delta .
An exact proof term for the current goal is H14 H16 .
Assume H16 : z0 delta .
An exact proof term for the current goal is Lnz0d H16 .
An exact proof term for the current goal is Hd .
An exact proof term for the current goal is H2 .
Let eps be given.
Apply ordsuccE delta eps He to the current goal.
An
exact proof term for the current goal is
PNo_extend1_eq delta (λgamma ⇒ gamma ∈ z ) eps He1 .
We will
prove eps ∈ z ↔ z1 eps .
rewrite the current goal using He1 (from left to right).
We will
prove delta ∈ z ↔ z1 delta .
Apply iffI to the current goal.
Assume _ .
An exact proof term for the current goal is Lz1d .
Assume _ .
An exact proof term for the current goal is H15 .
Apply LLzlet to the current goal.
We will
prove delta ∈ tau .
An exact proof term for the current goal is Hd .
An exact proof term for the current goal is Lzimv .
Apply PNoEq_tra_ tau (λgamma ⇒ gamma ∈ SNoCut L R ) w (λgamma ⇒ gamma ∈ z ) to the current goal.
An exact proof term for the current goal is LLecw .
We will
prove PNoEq_ tau w (λgamma ⇒ gamma ∈ z ) .
An exact proof term for the current goal is H12 .
Apply H12 to the current goal.
Let delta be given.
Assume H13 .
Apply H13 to the current goal.
Assume H13 .
Apply H13 to the current goal.
Assume H13 .
Apply H13 to the current goal.
Assume H15 : w delta .
We prove the intermediate
claim Ld :
ordinal delta .
An
exact proof term for the current goal is
ordinal_Hered tau H1 delta Hd .
Set z0 to be the term
λeps ⇒ eps ∈ z ∧ eps ≠ delta of type
set → prop .
Set z1 to be the term
λeps ⇒ eps ∈ z ∨ eps = delta of type
set → prop .
We prove the intermediate
claim Lnz0d :
¬ z0 delta .
Assume H10 .
Apply H10 to the current goal.
Apply H12 to the current goal.
Use reflexivity.
We prove the intermediate claim Lz1d : z1 delta .
We will
prove delta ∈ z ∨ delta = delta .
Apply orIR to the current goal.
Use reflexivity.
Apply H3 delta Hd (λgamma ⇒ gamma ∈ z ) to the current goal.
Apply andI to the current goal.
Let eps be given.
Apply ordsuccE delta eps He to the current goal.
An
exact proof term for the current goal is
PNo_extend0_eq delta (λgamma ⇒ gamma ∈ z ) eps He1 .
We will
prove eps ∈ z ↔ z0 eps .
rewrite the current goal using He1 (from left to right).
We will
prove delta ∈ z ↔ z0 delta .
Apply iffI to the current goal.
An exact proof term for the current goal is H14 H16 .
Assume H16 : z0 delta .
An exact proof term for the current goal is Lnz0d H16 .
Apply LLzlet to the current goal.
We will
prove delta ∈ tau .
An exact proof term for the current goal is Hd .
An exact proof term for the current goal is Lzimv .
Let eps be given.
Apply ordsuccE delta eps He to the current goal.
Apply iff_trans (w eps ) (eps ∈ z ) (z1 eps ) to the current goal.
An exact proof term for the current goal is H13 eps He1 .
An
exact proof term for the current goal is
PNo_extend1_eq delta (λgamma ⇒ gamma ∈ z ) eps He1 .
We will
prove w eps ↔ z1 eps .
rewrite the current goal using He1 (from left to right).
We will
prove w delta ↔ z1 delta .
Apply iffI to the current goal.
Assume _ .
An exact proof term for the current goal is Lz1d .
Assume _ .
An exact proof term for the current goal is H15 .
An exact proof term for the current goal is Hd .
An exact proof term for the current goal is H2 .
∎
Proof: Let L and R be given.
Assume HLR .
Let p be given.
Assume Hp .
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
Assume H .
Apply H to the current goal.
An exact proof term for the current goal is Hp .
∎
Proof: Let L be given.
Assume H1 .
Apply and3I to the current goal.
An exact proof term for the current goal is H1 .
Let y be given.
Assume Hy .
An
exact proof term for the current goal is
EmptyE y Hy .
Let x be given.
Assume Hx .
Let y be given.
Assume Hy .
An
exact proof term for the current goal is
EmptyE y Hy .
∎
Proof: Let R be given.
Assume H1 .
Apply and3I to the current goal.
Let x be given.
Assume Hx .
An
exact proof term for the current goal is
EmptyE x Hx .
An exact proof term for the current goal is H1 .
Let x be given.
Assume Hx .
An
exact proof term for the current goal is
EmptyE x Hx .
∎
Proof:
Let x be given.
Assume Hx .
An
exact proof term for the current goal is
EmptyE x Hx .
∎
Theorem. (
SNoS_E ) The following is provable:
Proof: Let alpha be given.
Let x be given.
∎
Beginning of Section TaggedSets2
Notation . We use
' as a postfix operator with priority 100 corresponding to applying term
tag .
Theorem. (
SNoS_I ) The following is provable:
Proof: Let alpha be given.
Let x be given.
Let beta be given.
Apply H1 to the current goal.
We will
prove x ∈ SNoS_ alpha .
Apply SepI to the current goal.
Apply PowerI to the current goal.
Apply Ha to the current goal.
Assume Ha1 _ .
An
exact proof term for the current goal is
Ha1 beta Hb .
We will
prove ∃ gamma ∈ alpha , SNo_ gamma x .
We use
beta to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb .
An exact proof term for the current goal is H1 .
∎
Theorem. (
SNoS_I2 ) The following is provable:
Proof: Let x and y be given.
Assume Hx Hy Hxy .
∎
Theorem. (
SNoS_Subq ) The following is provable:
Proof: Let alpha and beta be given.
Assume Ha Hb Hab .
Let x be given.
Apply SNoS_E alpha Ha x Hx to the current goal.
Let gamma be given.
Assume Hc .
Apply Hc to the current goal.
An
exact proof term for the current goal is
SNoS_I beta Hb x gamma (Hab gamma Hc1 ) Hc2 .
∎
Proof: Let alpha be given.
Assume Ha .
Let x be given.
Assume Hx .
An exact proof term for the current goal is Hx1 .
An exact proof term for the current goal is Ha .
An exact proof term for the current goal is Hx2 .
An exact proof term for the current goal is Hx .
∎
Theorem. (
SNoS_E2 ) The following is provable:
Proof: Let alpha be given.
Assume Ha .
Let x be given.
Assume Hx .
Let p be given.
Assume Hp .
Apply SNoS_E alpha Ha x Hx to the current goal.
Let beta be given.
Assume H1 .
Apply H1 to the current goal.
We prove the intermediate
claim Lx :
SNo x .
An
exact proof term for the current goal is
SNo_SNo beta Lb x H1 .
We prove the intermediate
claim Lxa :
SNoLev x ∈ alpha .
rewrite the current goal using Lxb (from left to right).
An exact proof term for the current goal is Hb .
An exact proof term for the current goal is Hp Lxa Hx1 Lx Hx2 .
∎
Proof: Let w be given.
Let x be given.
rewrite the current goal using Hxw (from left to right) at position 2.
An exact proof term for the current goal is Hx1 .
∎
Proof: Let z be given.
Set L to be the term
SNoL z .
Set R to be the term
SNoR z .
We prove the intermediate
claim L1 :
∀ x ∈ L , SNo x .
Let x be given.
An
exact proof term for the current goal is
SepE1 (SNoS_ (SNoLev z ) ) (λx ⇒ x < z ) x Hx .
Let beta be given.
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 H1 .
We prove the intermediate
claim L2 :
∀ y ∈ R , SNo y .
Let y be given.
An
exact proof term for the current goal is
SepE1 (SNoS_ (SNoLev z ) ) (λy ⇒ z < y ) y Hy .
Let beta be given.
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 H1 .
We prove the intermediate
claim L3 :
∀ x ∈ L , ∀ y ∈ R , x < y .
Let x be given.
Assume Hx .
Let y be given.
Assume Hy .
Apply SNoLt_tra x z y (L1 x Hx ) Hz (L2 y Hy ) to the current goal.
An
exact proof term for the current goal is
SepE2 (SNoS_ (SNoLev z ) ) (λx ⇒ x < z ) x Hx .
An
exact proof term for the current goal is
SepE2 (SNoS_ (SNoLev z ) ) (λy ⇒ z < y ) y Hy .
Apply and3I to the current goal.
An exact proof term for the current goal is L1 .
An exact proof term for the current goal is L2 .
An exact proof term for the current goal is L3 .
∎
Theorem. (
SNoL_E ) The following is provable:
Proof: Let x be given.
Let w be given.
Let p be given.
Assume Hp .
An exact proof term for the current goal is Hp Hw5 Hw3 Hw2 .
∎
Theorem. (
SNoR_E ) The following is provable:
Proof: Let x be given.
Let z be given.
Let p be given.
Assume Hp .
An exact proof term for the current goal is Hp Hz5 Hz3 Hz2 .
∎
Theorem. (
SNoL_SNoS ) The following is provable:
Proof: Let x be given.
Assume Hx .
Let w be given.
Apply SNoL_E x Hx w Hw to the current goal.
An
exact proof term for the current goal is
SNoS_I2 w x Hw1 Hx Hw2 .
∎
Theorem. (
SNoR_SNoS ) The following is provable:
Proof: Let x be given.
Assume Hx .
Let z be given.
Apply SNoR_E x Hx z Hz to the current goal.
An
exact proof term for the current goal is
SNoS_I2 z x Hz1 Hx Hz2 .
∎
Theorem. (
SNoL_I ) The following is provable:
Proof: Let z be given.
Assume Hz .
Let x be given.
Assume Hx Hxz1 Hxz2 .
We will
prove x ∈ SNoL z .
Apply SepI to the current goal.
An
exact proof term for the current goal is
SNoS_I2 x z Hx Hz Hxz1 .
An exact proof term for the current goal is Hxz2 .
∎
Theorem. (
SNoR_I ) The following is provable:
Proof: Let z be given.
Assume Hz .
Let y be given.
Assume Hy Hyz Hzy .
We will
prove y ∈ SNoR z .
Apply SepI to the current goal.
An
exact proof term for the current goal is
SNoS_I2 y z Hy Hz Hyz .
An exact proof term for the current goal is Hzy .
∎
Theorem. (
SNo_eta ) The following is provable:
Proof: Let z be given.
Set L to be the term
SNoL z .
Set R to be the term
SNoR z .
We prove the intermediate
claim LC :
SNoCutP L R .
Assume H1 .
Apply H1 to the current goal.
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 H1 .
We prove the intermediate
claim L5 :
∀ x ∈ L , x < z .
Let x be given.
An
exact proof term for the current goal is
SepE2 (SNoS_ (SNoLev z ) ) (λx ⇒ x < z ) x Hx .
We prove the intermediate
claim L6 :
∀ y ∈ R , z < y .
Let y be given.
An
exact proof term for the current goal is
SepE2 (SNoS_ (SNoLev z ) ) (λy ⇒ z < y ) y Hy .
Apply H5 z Hz L5 L6 to the current goal.
Assume H8 .
Apply H8 to the current goal.
Assume H9 .
Apply H9 to the current goal.
Apply H4 to the current goal.
Apply SepI to the current goal.
An
exact proof term for the current goal is
SNoLev_ (SNoCut L R ) H1 .
An exact proof term for the current goal is H9 .
rewrite the current goal using H9 (from left to right) at position 1.
An exact proof term for the current goal is H8 .
Apply H3 to the current goal.
Apply SepI to the current goal.
An
exact proof term for the current goal is
SNoLev_ (SNoCut L R ) H1 .
An exact proof term for the current goal is H9 .
An exact proof term for the current goal is H8 .
Apply H6 to the current goal.
An exact proof term for the current goal is H8 .
Use symmetry.
Apply SNo_eq to the current goal.
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is Hz .
An exact proof term for the current goal is L7 .
An exact proof term for the current goal is H7 .
∎
Proof: Let L and R be given.
Assume H2 _ .
Apply H2 to the current goal.
Assume H2 _ .
Apply H2 to the current goal.
Assume H2 _ .
Apply H2 to the current goal.
Assume H2 _ .
An exact proof term for the current goal is H2 .
∎
Proof: Let L and R be given.
Assume H2 _ .
Apply H2 to the current goal.
Assume H2 _ .
Apply H2 to the current goal.
Assume _ H2 .
An exact proof term for the current goal is H2 .
∎
Proof: Let L and R be given.
Assume H2 _ .
Apply H2 to the current goal.
Assume _ H2 .
An exact proof term for the current goal is H2 .
∎
Proof: Let L and R be given.
Assume _ H2 .
An exact proof term for the current goal is H2 .
∎
Theorem. (
SNoCut_Le ) The following is provable:
Proof: Let L1, R1, L2 and R2 be given.
Assume HLR1 HLR2 .
Apply HLR1 to the current goal.
Assume HLR1a .
Apply HLR1a to the current goal.
Apply HLR2 to the current goal.
Assume HLR2a .
Apply HLR2a to the current goal.
Assume H3 .
Apply H3 to the current goal.
Assume H3 .
Apply H3 to the current goal.
Assume H3 .
Apply H3 to the current goal.
Assume H8 .
Apply H8 to the current goal.
Assume H8 .
Apply H8 to the current goal.
Assume H8 .
Apply H8 to the current goal.
Let z be given.
We prove the intermediate
claim LzL1 :
∀ x ∈ L1 , x < z .
Let x be given.
Apply SNoLt_tra x (SNoCut L2 R2 ) z (HLR1a x Hx ) H8 Hz1 to the current goal.
An exact proof term for the current goal is H1 x Hx .
An exact proof term for the current goal is Hz5 .
We prove the intermediate
claim LzR1 :
∀ y ∈ R1 , z < y .
Let y be given.
Apply SNoLt_tra z (SNoCut L1 R1 ) y Hz1 H3 (HLR1b y Hy ) to the current goal.
An exact proof term for the current goal is Hz6 .
An exact proof term for the current goal is H6 y Hy .
Apply H7 z Hz1 LzL1 LzR1 to the current goal.
Assume _ .
Apply H14 to the current goal.
Set z to be the term
SNoCut L2 R2 .
We prove the intermediate
claim LzR1 :
∀ y ∈ R1 , z < y .
Let y be given.
An exact proof term for the current goal is H13 .
An exact proof term for the current goal is H6 y Hy .
Apply H7 z H8 H1 LzR1 to the current goal.
Assume _ .
Apply H17 to the current goal.
An exact proof term for the current goal is H14 .
Set z to be the term
SNoCut L1 R1 .
We prove the intermediate
claim LzL2 :
∀ x ∈ L2 , x < z .
Let x be given.
An exact proof term for the current goal is H10 x Hx .
An exact proof term for the current goal is H13 .
Apply H12 z H3 LzL2 H2 to the current goal.
Assume _ .
Apply H17 to the current goal.
An exact proof term for the current goal is H14 .
An exact proof term for the current goal is H13 .
∎
Proof: Let L1, R1, L2 and R2 be given.
Assume HLR1 HLR2 .
We prove the intermediate
claim LNLR1 :
SNo (SNoCut L1 R1 ) .
We prove the intermediate
claim LNLR2 :
SNo (SNoCut L2 R2 ) .
An
exact proof term for the current goal is
SNoCut_Le L1 R1 L2 R2 HLR1 HLR2 H1 H4 .
An
exact proof term for the current goal is
SNoCut_Le L2 R2 L1 R1 HLR2 HLR1 H3 H2 .
∎
Proof: Let x and y be given.
Assume Hx Hy Hxy .
Let p be given.
Assume Hp1 Hp2 Hp3 .
Apply SNoLtE x y Hx Hy Hxy to the current goal.
Let z be given.
Assume Hz1 Hz2 _ _ Hz3 Hz4 _ _ .
Assume Hz2a Hz2b .
Apply Hp1 z to the current goal.
We will
prove z ∈ SNoL y .
An
exact proof term for the current goal is
SNoL_I y Hy z Hz1 Hz2b Hz4 .
We will
prove z ∈ SNoR x .
An
exact proof term for the current goal is
SNoR_I x Hx z Hz1 Hz2a Hz3 .
Assume H1 _ _ .
Apply Hp2 to the current goal.
An
exact proof term for the current goal is
SNoL_I y Hy x Hx H1 Hxy .
Assume H1 _ _ .
Apply Hp3 to the current goal.
An
exact proof term for the current goal is
SNoR_I x Hx y Hy H1 Hxy .
∎
Proof: Let x and y be given.
Assume Hx Hy .
Let p be given.
Assume Hp1 Hp2 Hp3 Hp4 Hp5 Hp6 Hp7 .
An exact proof term for the current goal is Hp2 .
An exact proof term for the current goal is Hp3 .
An exact proof term for the current goal is Hp4 .
An exact proof term for the current goal is Hp1 H1 .
Let z be given.
Assume H2 H3 .
An exact proof term for the current goal is Hp5 z H3 H2 .
An exact proof term for the current goal is Hp7 .
An exact proof term for the current goal is Hp6 .
∎
Proof: Let L and R be given.
Assume HLR .
Set y to be the term
SNoCut L R .
Let w be given.
Apply dneg to the current goal.
Apply HLR to the current goal.
Assume H .
Apply H to the current goal.
Assume HL HR HLR' .
Apply SNoL_E y H1 w Hw to the current goal.
Assume Hw1 Hw2 Hw3 .
Apply H5 w Hw1 to the current goal.
Let w' be given.
Apply SNoLtLe_or w' w (HL w' Hw' ) Hw1 to the current goal.
Assume H6 .
An exact proof term for the current goal is H6 .
Apply HC to the current goal.
We use w' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw' .
An exact proof term for the current goal is H6 .
Let z be given.
Apply SNoLt_tra w y z Hw1 H1 (HR z Hz ) Hw3 to the current goal.
An exact proof term for the current goal is H4 z Hz .
An exact proof term for the current goal is Hw2 .
∎
Proof: Let L and R be given.
Assume HLR .
Set y to be the term
SNoCut L R .
Let z be given.
Apply dneg to the current goal.
Apply HLR to the current goal.
Assume H .
Apply H to the current goal.
Assume HL HR HLR' .
Apply SNoR_E y H1 z Hz to the current goal.
Assume Hz1 Hz2 Hz3 .
Apply H5 z Hz1 to the current goal.
Let w be given.
Apply SNoLt_tra w y z (HL w Hw ) H1 Hz1 to the current goal.
An exact proof term for the current goal is H3 w Hw .
An exact proof term for the current goal is Hz3 .
Let z' be given.
Apply SNoLtLe_or z z' Hz1 (HR z' Hz' ) to the current goal.
Assume H6 .
An exact proof term for the current goal is H6 .
Apply HC to the current goal.
We use z' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz' .
An exact proof term for the current goal is H6 .
An exact proof term for the current goal is Hz2 .
∎
Proof: Let alpha be given.
Apply andI to the current goal.
Let beta be given.
An exact proof term for the current goal is Hb .
Let beta be given.
We will
prove beta ∈ alpha .
An exact proof term for the current goal is Hb .
∎
Proof: Let alpha be given.
We use alpha to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha .
An
exact proof term for the current goal is
ordinal_SNo_ alpha Ha .
∎
Proof: Let alpha be given.
∎
Proof: Let alpha be given.
Let z be given.
We prove the intermediate
claim La1 :
SNo alpha .
An
exact proof term for the current goal is
ordinal_SNo alpha Ha .
We prove the intermediate
claim La2 :
SNoLev alpha = alpha .
Assume H1 .
Apply H1 to the current goal.
An exact proof term for the current goal is H1 .
Apply In_irref alpha to the current goal.
rewrite the current goal using La2 (from right to left) at position 1.
We will
prove SNoLev alpha ∈ alpha .
rewrite the current goal using H1 (from right to left) at position 1.
An exact proof term for the current goal is Hz2 .
Apply SNoLtE alpha z La1 Hz H1 to the current goal.
Let w be given.
rewrite the current goal using La2 (from left to right).
Apply H7 to the current goal.
rewrite the current goal using La2 (from left to right).
rewrite the current goal using La2 (from left to right).
An exact proof term for the current goal is H4 H2 .
∎
Proof: Let alpha be given.
We prove the intermediate
claim La1 :
SNo alpha .
An
exact proof term for the current goal is
ordinal_SNo alpha Ha .
We prove the intermediate
claim La2 :
SNoLev alpha = alpha .
Let x be given.
Apply SNoL_E alpha La1 x Hx to the current goal.
We will
prove x ∈ SNoS_ alpha .
rewrite the current goal using La2 (from right to left).
Apply SNoS_I2 x alpha Hx1 La1 to the current goal.
An exact proof term for the current goal is Hx2 .
Let x be given.
Apply SNoS_E2 alpha Ha x Hx to the current goal.
We will
prove x ∈ SNoL alpha .
Apply SNoL_I alpha La1 x Hx3 to the current goal.
rewrite the current goal using La2 (from left to right).
An exact proof term for the current goal is Hx1 .
∎
Proof: Let alpha be given.
We prove the intermediate
claim La1 :
SNo alpha .
An
exact proof term for the current goal is
ordinal_SNo alpha Ha .
We prove the intermediate
claim La2 :
SNoLev alpha = alpha .
Let x be given.
Apply SNoR_E alpha La1 x Hx to the current goal.
rewrite the current goal using La2 (from left to right).
Apply SNoLt_tra x alpha x Hx1 La1 Hx1 to the current goal.
An exact proof term for the current goal is Hx3 .
∎
Theorem. (
nat_p_SNo ) The following is provable:
Proof: Let n be given.
Assume Hn .
An exact proof term for the current goal is Hn .
∎
Theorem. (
omega_SNo ) The following is provable:
Proof: Let n be given.
Assume Hn .
An exact proof term for the current goal is Hn .
∎
Proof: Let n be given.
An exact proof term for the current goal is Hn .
An exact proof term for the current goal is Hn .
∎
Proof: Let alpha be given.
Let beta be given.
We prove the intermediate
claim Lb1 :
SNo beta .
rewrite the current goal using Lb2 (from left to right).
An exact proof term for the current goal is Hb .
∎
Proof: Let alpha be given.
Apply Ha to the current goal.
Assume Ha1 _ .
Let z be given.
We prove the intermediate
claim La1 :
SNo alpha .
An
exact proof term for the current goal is
ordinal_SNo alpha Ha .
We prove the intermediate
claim La2 :
SNoLev alpha = alpha .
Apply dneg to the current goal.
Let beta be given.
Apply dneg to the current goal.
Apply H1 to the current goal.
We prove the intermediate
claim Lb1 :
SNo beta .
rewrite the current goal using Lb2 (from left to right).
rewrite the current goal using Hz3 (from left to right).
We will
prove beta ∈ alpha .
An exact proof term for the current goal is Hb2 .
rewrite the current goal using Lb2 (from left to right).
Let gamma be given.
We will
prove gamma ∈ z ↔ gamma ∈ beta .
Apply iffI to the current goal.
Assume _ .
An exact proof term for the current goal is Hc .
Assume _ .
Apply IH gamma Hc to the current goal.
We will
prove gamma ∈ alpha .
An
exact proof term for the current goal is
Ha1 beta Hb2 gamma Hc .
rewrite the current goal using Lb2 (from left to right).
An exact proof term for the current goal is H2 .
We will
prove beta < alpha .
We prove the intermediate
claim L2 :
alpha ⊆ z .
We prove the intermediate
claim L3 :
z = alpha .
Apply SNo_eq z alpha Hz La1 to the current goal.
rewrite the current goal using La2 (from left to right).
An exact proof term for the current goal is Hz3 .
rewrite the current goal using Hz3 (from left to right).
Let beta be given.
Apply iffI to the current goal.
Assume _ .
An exact proof term for the current goal is Hb .
Assume _ .
An
exact proof term for the current goal is
L2 beta Hb .
Apply H1 to the current goal.
rewrite the current goal using L3 (from left to right).
We will
prove alpha ≤ alpha .
∎
Proof: Let alpha and beta be given.
Assume Ha Hb Hab .
An exact proof term for the current goal is H1 .
We prove the intermediate
claim L1a :
alpha = beta .
An exact proof term for the current goal is Hab .
An exact proof term for the current goal is H1 .
rewrite the current goal using L1a (from left to right).
We prove the intermediate
claim La1 :
SNo alpha .
An
exact proof term for the current goal is
ordinal_SNo alpha Ha .
We prove the intermediate
claim La2 :
SNoLev alpha = alpha .
rewrite the current goal using La2 (from left to right).
An exact proof term for the current goal is L1 .
∎
Proof: Let alpha and beta be given.
Assume Ha Hb .
Assume H1 .
Assume H2 .
An exact proof term for the current goal is H2 .
We will
prove alpha < alpha .
We will
prove beta ≤ alpha .
∎
Proof: Let m be given.
Assume Hm .
∎
Theorem. (
SNo_0 ) The following is provable:
Theorem. (
SNo_1 ) The following is provable:
Proof:
An
exact proof term for the current goal is
nat_1 .
∎
Theorem. (
SNo_2 ) The following is provable:
Proof:
An
exact proof term for the current goal is
nat_2 .
∎
Theorem. (
SNoLev_0 ) The following is provable:
Proof:
rewrite the current goal using
binunion_idl 0 (from left to right).
Assume _ _ _ .
Use transitivity with and
0 .
An exact proof term for the current goal is L1 .
Use symmetry.
An
exact proof term for the current goal is
SNoLev_0 .
rewrite the current goal using L1 (from left to right).
Let beta be given.
An
exact proof term for the current goal is
EmptyE beta Hb .
∎
Theorem. (
SNoL_0 ) The following is provable:
Proof:
Let z be given.
We prove the intermediate
claim Lz :
z ∈ SNoS_ 0 .
rewrite the current goal using
SNoLev_0 (from right to left).
An
exact proof term for the current goal is
SNoL_SNoS_ 0 z Hz .
An
exact proof term for the current goal is
EmptyE (SNoLev z ) Hz1 .
∎
Theorem. (
SNoR_0 ) The following is provable:
Proof:
Let z be given.
We prove the intermediate
claim Lz :
z ∈ SNoS_ 0 .
rewrite the current goal using
SNoLev_0 (from right to left).
An
exact proof term for the current goal is
SNoR_SNoS_ 0 z Hz .
An
exact proof term for the current goal is
EmptyE (SNoLev z ) Hz1 .
∎
Theorem. (
SNoL_1 ) The following is provable:
Proof:
Let x be given.
Assume _ .
We prove the intermediate
claim L1 :
0 = x .
rewrite the current goal using
SNoLev_0 (from left to right).
Use reflexivity.
rewrite the current goal using
SNoLev_0 (from left to right).
Let beta be given.
An
exact proof term for the current goal is
EmptyE beta Hb .
rewrite the current goal using L1 (from right to left).
An
exact proof term for the current goal is
In_0_1 .
Let x be given.
rewrite the current goal using
SNoLev_0 (from left to right).
An
exact proof term for the current goal is
In_0_1 .
∎
Theorem. (
SNoR_1 ) The following is provable:
Proof: Let x be given.
We prove the intermediate
claim LLx2 :
SNo (SNoLev x ) .
We prove the intermediate
claim L3 :
x ≤ SNoLev x .
Let z be given.
Apply SNoLt_tra z x z Hz Hx Hz to the current goal.
Apply H2 to the current goal.
An exact proof term for the current goal is Hz7 .
An exact proof term for the current goal is Hz .
An exact proof term for the current goal is Hz4 .
An exact proof term for the current goal is H4 .
An exact proof term for the current goal is H4 .
Use symmetry.
An exact proof term for the current goal is H3 .
∎
Proof: Let x be given.
rewrite the current goal using
SNo_max_SNoLev x Hx H2 (from right to left).
∎
Proof: Let x be given.
Assume Hx Hxpos Hxlow .
Assume _ .
We prove the intermediate
claim L1 :
SNoLev x = 1 .
An exact proof term for the current goal is Hxlow .
Let n be given.
Apply cases_1 n Hn to the current goal.
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is L1 .
rewrite the current goal using L1 (from left to right).
Let n be given.
We will
prove n ∈ x ↔ n ∈ 1 .
Apply cases_1 n Hn (λn ⇒ n ∈ x ↔ n ∈ 1 ) to the current goal.
Apply iffI to the current goal.
Assume _ .
An
exact proof term for the current goal is
In_0_1 .
Assume _ .
An exact proof term for the current goal is H2 .
An exact proof term for the current goal is H1 .
∎
Proof: Let x be given.
Set alpha to be the term
SNoLev x .
We prove the intermediate
claim La :
ordinal alpha .
∎
Proof: Let x be given.
Set alpha to be the term
SNoLev x .
We prove the intermediate
claim La :
ordinal alpha .
∎
Proof: Let x be given.
Assume Hx .
∎
Proof: Let x be given.
Assume Hx .
∎
Proof: Let x be given.
Assume Hx .
∎
Proof: Let x be given.
Assume Hx .
∎
Proof: Let x be given.
Set alpha to be the term
SNoLev x .
Set p to be the term
λdelta ⇒ delta ∈ x ∧ delta ≠ alpha of type
set → prop .
Assume _ .
Apply H4 to the current goal.
Use reflexivity.
Let beta be given.
rewrite the current goal using H5 (from right to left).
∎
Proof: Let x be given.
Set alpha to be the term
SNoLev x .
Set p to be the term
λdelta ⇒ delta ∈ x ∨ delta = alpha of type
set → prop .
Apply SepI to the current goal.
We will
prove alpha ∈ x ∨ alpha = alpha .
Apply orIR to the current goal.
Use reflexivity.
∎
Proof: Let x be given.
Set alpha to be the term
SNoLev x .
We prove the intermediate
claim La :
ordinal alpha .
Set p to be the term
λbeta ⇒ beta ∈ x of type
set → prop .
Set q to be the term
λbeta ⇒ beta ∈ x ∧ beta ≠ alpha of type
set → prop .
We will
prove PNoEq_ alpha q p .
∎
Proof: Let x be given.
Set alpha to be the term
SNoLev x .
We prove the intermediate
claim La :
ordinal alpha .
Set p to be the term
λbeta ⇒ beta ∈ x of type
set → prop .
Set q to be the term
λbeta ⇒ beta ∈ x ∨ beta = alpha of type
set → prop .
We will
prove PNoEq_ alpha q p .
∎
Proof: Let x be given.
Assume Hx Hx0 .
rewrite the current goal using
SNoLev_0 (from left to right).
An exact proof term for the current goal is Hx0 .
rewrite the current goal using Hx0 (from left to right).
Let alpha be given.
An
exact proof term for the current goal is
EmptyE alpha Ha .
∎
Proof: Let n and alpha be given.
Assume Ha .
An
exact proof term for the current goal is
SingE 0 alpha H2 .
Let m be given.
rewrite the current goal using H3 (from right to left).
An exact proof term for the current goal is Ha .
∎
Theorem. (
eps_0_1 ) The following is provable:
Proof:
Let x be given.
rewrite the current goal using
SingE 0 x Hx (from left to right).
An
exact proof term for the current goal is
In_0_1 .
Let m be given.
An
exact proof term for the current goal is
EmptyE m Hm .
Let x be given.
Apply SingI to the current goal.
∎
Theorem. (
SNo__eps_ ) The following is provable:
Proof: Let n be given.
Assume Hn .
We prove the intermediate
claim Ln :
nat_p n .
An
exact proof term for the current goal is
omega_nat_p n Hn .
Apply andI to the current goal.
Let x be given.
rewrite the current goal using
SingE 0 x Hx (from left to right).
Let m be given.
rewrite the current goal using Hxm (from left to right).
Let m be given.
We prove the intermediate
claim Lm :
nat_p m .
Apply nat_inv m Lm to the current goal.
rewrite the current goal using Hm (from left to right).
rewrite the current goal using
SingE 0 (0 ' ) H2 (from right to left) at position 2.
Apply SingI to the current goal.
Let m be given.
An exact proof term for the current goal is H3 .
An
exact proof term for the current goal is
SingI 0 .
Assume H1 .
Apply H1 to the current goal.
Let k be given.
Assume H1 .
Apply H1 to the current goal.
We prove the intermediate
claim Lm :
nat_p m .
rewrite the current goal using Hmk (from left to right).
An
exact proof term for the current goal is
nat_ordsucc k Hk .
rewrite the current goal using Hmk (from right to left).
An exact proof term for the current goal is Hm .
We prove the intermediate
claim Lk :
k ∈ n .
rewrite the current goal using H2 (from right to left).
rewrite the current goal using Hmk (from left to right).
An
exact proof term for the current goal is
ReplI n (λk ⇒ (ordsucc k ) ' ) k Lk .
We will
prove m ∉ eps_ n .
Apply EmptyE 0 to the current goal.
rewrite the current goal using
SingE 0 m H2 (from right to left) at position 2.
rewrite the current goal using Hmk (from left to right).
Let j be given.
rewrite the current goal using Hmj (from right to left).
∎
Theorem. (
SNo_eps_ ) The following is provable:
Proof: Let n be given.
Assume Hn .
We prove the intermediate
claim Ln :
nat_p n .
An
exact proof term for the current goal is
omega_nat_p n Hn .
∎
Theorem. (
SNo_eps_1 ) The following is provable:
Proof: Let n be given.
Assume Hn .
We prove the intermediate
claim Ln :
nat_p n .
An
exact proof term for the current goal is
omega_nat_p n Hn .
∎
Proof: Let n be given.
Assume Hn .
An
exact proof term for the current goal is
SNo__eps_ n Hn .
∎
Proof: Let n be given.
Assume Hn .
Let m be given.
Assume Hm .
We prove the intermediate
claim Lnn :
nat_p n .
An
exact proof term for the current goal is
omega_nat_p n Hn .
We prove the intermediate
claim Lmn :
nat_p m .
An
exact proof term for the current goal is
nat_p_trans n Lnn m Hm .
We prove the intermediate
claim Lm :
m ∈ ω .
An
exact proof term for the current goal is
nat_p_omega m Lmn .
rewrite the current goal using
SNoLev_eps_ m Lm (from left to right).
rewrite the current goal using
SNoLev_eps_ n Hn (from left to right).
rewrite the current goal using
SNoLev_eps_ m Lm (from left to right).
Let k be given.
We prove the intermediate
claim Lk :
ordinal k .
Apply iffI to the current goal.
Apply SingI to the current goal.
Apply SingI to the current goal.
rewrite the current goal using
SNoLev_eps_ m Lm (from left to right).
∎
Proof: Let n be given.
Assume Hn .
rewrite the current goal using
SNoLev_0 (from left to right).
rewrite the current goal using
SNoLev_eps_ n Hn (from left to right).
rewrite the current goal using
SNoLev_0 (from left to right).
Let alpha be given.
An
exact proof term for the current goal is
EmptyE alpha Ha .
rewrite the current goal using
SNoLev_0 (from left to right).
Apply SingI to the current goal.
∎
Proof: Let n be given.
Let x be given.
We prove the intermediate
claim Ln :
n ∈ ω .
An
exact proof term for the current goal is
nat_p_omega n Hn .
We will
prove eps_ n < x .
An exact proof term for the current goal is H2 .
rewrite the current goal using
SNoLev_eps_ n Ln (from right to left) at position 1.
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is Hx1 .
Let z be given.
We prove the intermediate
claim Lz0 :
z = 0 .
Apply SNoLt_tra x z x Hx3 Hz1 Hx3 Hz5 to the current goal.
rewrite the current goal using Lz0 (from left to right).
An exact proof term for the current goal is Hxpos .
We prove the intermediate
claim Lx0 :
x = 0 .
rewrite the current goal using Lx0 (from left to right) at position 1.
An exact proof term for the current goal is Hxpos .
rewrite the current goal using
SNoLev_eps_ n Ln (from left to right).
∎
Proof: Let n be given.
Assume Hn .
Let x be given.
We prove the intermediate
claim Ln :
n ∈ ω .
An
exact proof term for the current goal is
nat_p_omega n Hn .
We will
prove eps_ n ≤ x .
Let z be given.
We prove the intermediate
claim Lz0 :
z = 0 .
Apply SNoLt_tra x z x Hx3 Hz1 Hx3 Hz5 to the current goal.
rewrite the current goal using Lz0 (from left to right).
An exact proof term for the current goal is Hxpos .
We prove the intermediate
claim Lx0 :
x = 0 .
rewrite the current goal using Lx0 (from left to right) at position 1.
An exact proof term for the current goal is Hxpos .
rewrite the current goal using
SNoLev_eps_ n Ln (from left to right).
rewrite the current goal using H4 (from left to right) at position 1.
An exact proof term for the current goal is H3 .
An exact proof term for the current goal is H2 .
∎
Proof: Let n be given.
Assume Hn .
Let x be given.
An exact proof term for the current goal is Hx1a .
We prove the intermediate
claim L2 :
x = 0 .
An
exact proof term for the current goal is
SNoLev_0_eq_0 x Hx1c H1 .
rewrite the current goal using L2 (from left to right) at position 1.
An exact proof term for the current goal is Hx2 .
Assume H1 .
Apply H1 to the current goal.
Let m be given.
Assume H1 .
Apply H1 to the current goal.
We use m to witness the existential quantifier.
Apply andI to the current goal.
rewrite the current goal using Hm2 (from left to right).
We will
prove x = eps_ m .
An exact proof term for the current goal is Hm2 .
An exact proof term for the current goal is Hx3 .
rewrite the current goal using Hm2 (from left to right).
Let k be given.
We prove the intermediate
claim L3 :
ordinal k .
Apply iffI to the current goal.
Apply SingI to the current goal.
Apply SingI to the current goal.
∎
Proof: Let n be given.
Assume Hn .
Set L to be the term
{ 0 } .
We prove the intermediate
claim Ln :
nat_p n .
An
exact proof term for the current goal is
omega_nat_p n Hn .
Apply and3I to the current goal.
Let w be given.
Assume Hw .
rewrite the current goal using
SingE 0 w Hw (from left to right).
An
exact proof term for the current goal is
SNo_0 .
Let z be given.
Assume Hz .
Let m be given.
rewrite the current goal using Hm2 (from left to right).
An
exact proof term for the current goal is
nat_p_trans n Ln m Hm1 .
Let w be given.
Assume Hw .
Let z be given.
Assume Hz .
Let m be given.
rewrite the current goal using
SingE 0 w Hw (from left to right).
rewrite the current goal using Hm2 (from left to right).
An
exact proof term for the current goal is
nat_p_trans n Ln m Hm1 .
∎
Proof: Let n be given.
Assume Hn .
Set L to be the term
{ 0 } .
We prove the intermediate
claim Ln :
nat_p n .
An
exact proof term for the current goal is
omega_nat_p n Hn .
We prove the intermediate
claim L1 :
SNoCutP L R .
An
exact proof term for the current goal is
eps_SNoCutP n Hn .
We prove the intermediate
claim LRS :
∀ z ∈ R , SNo z .
Apply L1 to the current goal.
Assume H _ .
Apply H to the current goal.
Assume _ H .
An exact proof term for the current goal is H .
Let k be given.
Assume Hk .
Let w be given.
rewrite the current goal using
SingE 0 w Hw (from left to right).
rewrite the current goal using
SNoLev_0 (from left to right).
An exact proof term for the current goal is H2 .
Let i be given.
Assume Hi .
rewrite the current goal using
SNoLev_0 (from left to right).
An
exact proof term for the current goal is
In_0_1 .
Let k be given.
Assume Hk .
Let z be given.
Let m be given.
rewrite the current goal using Hm2 (from left to right).
An exact proof term for the current goal is Ln .
An exact proof term for the current goal is Hm1 .
Apply L3b to the current goal.
An exact proof term for the current goal is H3 .
rewrite the current goal using H3 (from left to right).
An exact proof term for the current goal is L3a .
Let i be given.
Apply nat_inv n Ln to the current goal.
An exact proof term for the current goal is Hn0 H2 .
Assume H2 .
Apply H2 to the current goal.
Let n' be given.
Assume H2 .
Apply H2 to the current goal.
We will
prove eps_ n' ∈ R .
Apply ReplI to the current goal.
rewrite the current goal using Hn'2 (from left to right).
rewrite the current goal using Hn'2 (from right to left).
An exact proof term for the current goal is Hi .
Apply xm (n = 0 ) to the current goal.
We prove the intermediate
claim L4a :
R = 0 .
Let z be given.
Assume Hz .
Let m be given.
rewrite the current goal using H2 (from left to right).
An
exact proof term for the current goal is
EmptyE m Hm1 .
rewrite the current goal using L4a (from left to right).
rewrite the current goal using
binunion_idr (from left to right).
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is L2 .
rewrite the current goal using L3 H2 (from right to left).
rewrite the current goal using L2 (from left to right).
rewrite the current goal using L3 H2 (from left to right).
Let i be given.
Assume Hi .
An exact proof term for the current goal is Ln .
rewrite the current goal using L4 (from left to right).
We prove the intermediate
claim L5 :
SNo (eps_ n ) .
An
exact proof term for the current goal is
SNo_eps_ n Hn .
We prove the intermediate
claim L6 :
∀ w ∈ L , w < eps_ n .
Let w be given.
Assume Hw .
rewrite the current goal using
SingE 0 w Hw (from left to right).
An
exact proof term for the current goal is
SNo_eps_pos n Hn .
We prove the intermediate
claim L7 :
∀ z ∈ R , eps_ n < z .
Let z be given.
Assume Hz .
Let m be given.
rewrite the current goal using Hm2 (from left to right).
An
exact proof term for the current goal is
SNo_eps_decr n Hn m Hm1 .
Apply H5 (eps_ n ) L5 L6 L7 to the current goal.
Use symmetry.
rewrite the current goal using
SNoLev_eps_ n Hn (from left to right).
We prove the intermediate
claim L8 :
eps_ n < SNoCut L R .
An
exact proof term for the current goal is
SNoLev_ (SNoCut L R ) H1 .
Apply H3 to the current goal.
Apply SingI to the current goal.
Let z be given.
We prove the intermediate
claim L9 :
∀ w ∈ L , w < z .
Let w be given.
Assume Hw .
rewrite the current goal using
SingE 0 w Hw (from left to right).
An
exact proof term for the current goal is
SNo_eps_pos n Hn .
An exact proof term for the current goal is Hz5 .
We prove the intermediate
claim L10 :
∀ v ∈ R , z < v .
Let v be given.
Assume Hv .
Apply SNoLt_tra z (SNoCut L R ) v Hz1 H1 (LRS v Hv ) Hz6 to the current goal.
Apply H4 to the current goal.
An exact proof term for the current goal is Hv .
Apply H5 z Hz1 L9 L10 to the current goal.
Apply H9 to the current goal.
rewrite the current goal using
SNoLev_eps_ n Hn (from left to right).
rewrite the current goal using
SNoLev_eps_ n Hn (from left to right).
An exact proof term for the current goal is H9 .
An exact proof term for the current goal is H1 .
Apply H3 to the current goal.
Apply SingI to the current goal.
An exact proof term for the current goal is H10 .
Apply L11 to the current goal.
Let m be given.
Assume H12 .
Apply H12 to the current goal.
rewrite the current goal using Hm2 (from right to left) at position 1.
Apply H4 to the current goal.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hm1 .
An exact proof term for the current goal is H8 .
An exact proof term for the current goal is H7 .
∎
End of Section TaggedSets2
Theorem. (
SNo_etaE ) The following is provable:
Proof: Let z be given.
Let p be given.
Assume H1 .
We prove the intermediate
claim L1 :
z = SNoCut L R .
An
exact proof term for the current goal is
SNo_eta z Hz .
Let x be given.
Let beta be given.
Assume Hx3 .
Apply Hx3 to the current goal.
We prove the intermediate
claim Lx1 :
SNo x .
We use
beta to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Lb .
An exact proof term for the current goal is Hx3 .
An exact proof term for the current goal is Hx4 .
An exact proof term for the current goal is Lb .
Apply Hx5 to the current goal.
An exact proof term for the current goal is Hx3 .
rewrite the current goal using Lx2 (from left to right).
An exact proof term for the current goal is Hb .
Apply and3I to the current goal.
An exact proof term for the current goal is Lx1 .
An exact proof term for the current goal is Lx3 .
An exact proof term for the current goal is Hx2 .
Let y be given.
Let beta be given.
Assume Hy3 .
Apply Hy3 to the current goal.
We prove the intermediate
claim Ly1 :
SNo y .
We use
beta to
witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Lb .
An exact proof term for the current goal is Hy3 .
An exact proof term for the current goal is Hy4 .
An exact proof term for the current goal is Lb .
Apply Hy5 to the current goal.
An exact proof term for the current goal is Hy3 .
rewrite the current goal using Ly2 (from left to right).
An exact proof term for the current goal is Hb .
Apply and3I to the current goal.
An exact proof term for the current goal is Ly1 .
An exact proof term for the current goal is Ly3 .
An exact proof term for the current goal is Hy2 .
Apply H1 L R to the current goal.
Apply and3I to the current goal.
Let x be given.
Assume Hx .
Apply LL x Hx to the current goal.
Assume H _ .
Apply H to the current goal.
Assume H _ .
An exact proof term for the current goal is H .
Let y be given.
Assume Hy .
Apply LR y Hy to the current goal.
Assume H _ .
Apply H to the current goal.
Assume H _ .
An exact proof term for the current goal is H .
Let x be given.
Assume Hx .
Let y be given.
Assume Hy .
Apply LL x Hx to the current goal.
Assume H2 .
Apply H2 to the current goal.
Apply LR y Hy to the current goal.
Assume H5 .
Apply H5 to the current goal.
An
exact proof term for the current goal is
SNoLt_tra x z y H2 Hz H5 H4 H7 .
Let x be given.
Assume Hx .
Apply LL x Hx to the current goal.
Assume H _ .
Apply H to the current goal.
Assume _ H .
An exact proof term for the current goal is H .
Let y be given.
Assume Hy .
Apply LR y Hy to the current goal.
Assume H _ .
Apply H to the current goal.
Assume _ H .
An exact proof term for the current goal is H .
An exact proof term for the current goal is L1 .
∎
Theorem. (
SNo_ind ) The following is provable:
Proof: Let P be given.
Assume H1 .
We prove the intermediate
claim L1 :
∀alpha, ordinal alpha → ∀z, SNo z → SNoLev z ∈ alpha → P z .
Let alpha be given.
Let z be given.
We will prove P z .
Apply SNo_etaE z Hz to the current goal.
Let L and R be given.
Apply H2 to the current goal.
Assume H6 .
Apply H6 to the current goal.
rewrite the current goal using H5 (from left to right).
Apply H1 to the current goal.
An exact proof term for the current goal is H2 .
We will
prove ∀x, x ∈ L → P x .
Let x be given.
Apply IH (SNoLev z ) Hz2 x to the current goal.
An exact proof term for the current goal is H6 x Hx .
An exact proof term for the current goal is H3 x Hx .
We will
prove ∀y, y ∈ R → P y .
Let y be given.
Apply IH (SNoLev z ) Hz2 y to the current goal.
An exact proof term for the current goal is H7 y Hy .
An exact proof term for the current goal is H4 y Hy .
Let z be given.
An exact proof term for the current goal is Hz .
∎
Beginning of Section SurrealRecI
Variable F : set → (set → set ) → set
Hypothesis Fr : ∀z, SNo z → ∀g h : set → set , (∀ w ∈ SNoS_ (SNoLev z ) , g w = h w ) → F z g = F z h
Proof: Let z be given.
We prove the intermediate
claim L1 :
∀alpha, ∀g h : set → set → set , (∀ x ∈ alpha , g x = h x ) → G alpha g = G alpha h .
Let alpha, g and h be given.
We will
prove G alpha g = G alpha h .
Apply xm (ordinal alpha ) to the current goal.
Apply func_ext set set to the current goal.
Let z be given.
rewrite the current goal using
If_i_1 (z ∈ SNoS_ (ordsucc alpha ) ) (F z (λw ⇒ g (SNoLev w ) w ) ) default Hz (from left to right).
rewrite the current goal using
If_i_1 (z ∈ SNoS_ (ordsucc alpha ) ) (F z (λw ⇒ h (SNoLev w ) w ) ) default Hz (from left to right).
We will
prove F z (λw ⇒ g (SNoLev w ) w ) = F z (λw ⇒ h (SNoLev w ) w ) .
We will
prove F z (λw ⇒ g (SNoLev w ) w ) = F z (λw ⇒ h (SNoLev w ) w ) .
Apply Fr to the current goal.
An exact proof term for the current goal is Hz3 .
Let w be given.
We prove the intermediate
claim LLw :
SNoLev w ∈ alpha .
Apply H1 to the current goal.
Assume Ha1 _ .
An
exact proof term for the current goal is
Ha1 (SNoLev z ) H2 (SNoLev w ) Hw1 .
rewrite the current goal using H2 (from right to left).
An exact proof term for the current goal is Hw1 .
rewrite the current goal using
Hgh (SNoLev w ) LLw (from left to right).
Use reflexivity.
rewrite the current goal using
If_i_0 (z ∈ SNoS_ (ordsucc alpha ) ) (F z (λw ⇒ h (SNoLev w ) w ) ) default Hz (from left to right).
rewrite the current goal using
In_rec_ii_eq G L1 (from left to right).
An
exact proof term for the current goal is
SNoS_SNoLev z Hz .
∎
End of Section SurrealRecI
Beginning of Section SurrealRecII
Variable F : set → (set → (set → set ) ) → (set → set )
Let G : set → (set → set → (set → set ) ) → set → (set → set ) ≝ λalpha g ⇒ If_iii (ordinal alpha ) (λz : set ⇒ If_ii (z ∈ SNoS_ (ordsucc alpha ) ) (F z (λw ⇒ g (SNoLev w ) w ) ) default ) (λz : set ⇒ default )
Hypothesis Fr : ∀z, SNo z → ∀g h : set → (set → set ) , (∀ w ∈ SNoS_ (SNoLev z ) , g w = h w ) → F z g = F z h
Proof: Let z be given.
We prove the intermediate
claim L1 :
∀alpha, ∀g h : set → set → (set → set ) , (∀ x ∈ alpha , g x = h x ) → G alpha g = G alpha h .
Let alpha, g and h be given.
We will
prove G alpha g = G alpha h .
Apply xm (ordinal alpha ) to the current goal.
Apply func_ext set (set → set ) to the current goal.
Let z be given.
We will
prove F z (λw ⇒ g (SNoLev w ) w ) = F z (λw ⇒ h (SNoLev w ) w ) .
We will
prove F z (λw ⇒ g (SNoLev w ) w ) = F z (λw ⇒ h (SNoLev w ) w ) .
Apply Fr to the current goal.
An exact proof term for the current goal is Hz3 .
Let w be given.
We prove the intermediate
claim LLw :
SNoLev w ∈ alpha .
Apply H1 to the current goal.
Assume Ha1 _ .
An
exact proof term for the current goal is
Ha1 (SNoLev z ) H2 (SNoLev w ) Hw1 .
rewrite the current goal using H2 (from right to left).
An exact proof term for the current goal is Hw1 .
rewrite the current goal using
Hgh (SNoLev w ) LLw (from left to right).
Use reflexivity.
rewrite the current goal using
In_rec_iii_eq G L1 (from left to right).
An
exact proof term for the current goal is
SNoS_SNoLev z Hz .
∎
End of Section SurrealRecII
Beginning of Section SurrealRec2
Variable F : set → set → (set → set → set ) → set
Let G : set → (set → set → set ) → set → (set → set ) → set ≝ λw f z g ⇒ F w z (λx y ⇒ if x = w then g y else f x y )
Proof: Let w be given.
Let f and k be given.
Let z be given.
Let g and h be given.
We will
prove G w f z g = G w k z h .
Apply Fr to the current goal.
An exact proof term for the current goal is Hw .
An exact proof term for the current goal is Hz .
Let x be given.
Let y be given.
We prove the intermediate
claim Lxw :
x ≠ w .
An
exact proof term for the current goal is
SNoS_In_neq w Hw x Hx .
rewrite the current goal using
If_i_0 (x = w ) (g y ) (f x y ) Lxw (from left to right).
rewrite the current goal using
If_i_0 (x = w ) (h y ) (k x y ) Lxw (from left to right).
We will
prove f x y = k x y .
rewrite the current goal using Hfk x Hx (from left to right).
Use reflexivity.
Let y be given.
rewrite the current goal using
If_i_1 (w = w ) (g y ) (f w y ) (λq H ⇒ H ) (from left to right).
rewrite the current goal using
If_i_1 (w = w ) (h y ) (k w y ) (λq H ⇒ H ) (from left to right).
An exact proof term for the current goal is Hgh y Hy .
∎
Proof: Let w be given.
Let f be given.
We prove the intermediate
claim L1 :
∀z, SNo z → ∀g h : set → set , (∀ u ∈ SNoS_ (SNoLev z ) , g u = h u ) → G w f z g = G w f z h .
Let z be given.
Assume Hz .
Let g and h be given.
Assume Hgh .
Let x be given.
Assume Hx .
Use reflexivity.
An
exact proof term for the current goal is
SNo_rec2_G_prop w Hw f f L1a z Hz g h Hgh .
An
exact proof term for the current goal is
SNo_rec_i_eq (G w f ) L1 .
∎
Proof: Let w be given.
Let z be given.
We prove the intermediate
claim L1 :
∀w, SNo w → ∀g h : set → set → set , (∀ x ∈ SNoS_ (SNoLev w ) , g x = h x ) → H w g = H w h .
Let w be given.
Let g and h be given.
We will
prove H w g = H w h .
Apply func_ext set set to the current goal.
Let z be given.
Apply xm (SNo z ) to the current goal.
Let alpha be given.
Let z be given.
Apply SNoS_E2 alpha Ha z Hz to the current goal.
rewrite the current goal using
SNo_rec2_eq_1 w Hw g z Hz3 (from left to right).
rewrite the current goal using
SNo_rec2_eq_1 w Hw h z Hz3 (from left to right).
Let y be given.
An
exact proof term for the current goal is
IH (SNoLev z ) Hz1 y Hy .
Let x be given.
Let y be given.
We prove the intermediate
claim Lxw :
x ≠ w .
An
exact proof term for the current goal is
SNoS_In_neq w Hw x Hx .
Let y be given.
We prove the intermediate
claim Ly :
SNo y .
An exact proof term for the current goal is Hy3 .
rewrite the current goal using
SNo_rec_ii_eq H L1 w Hw (from left to right).
An exact proof term for the current goal is (λq H ⇒ H ) .
rewrite the current goal using
SNo_rec_ii_eq H L1 w Hw (from left to right).
An exact proof term for the current goal is L2 .
∎
End of Section SurrealRec2
Proof: Let P be given.
Assume H1 .
Let x be given.
An
exact proof term for the current goal is
SNoS_SNoLev x Hx .
An
exact proof term for the current goal is
H1 (ordsucc (SNoLev x ) ) LsLx x LxsLx .
∎
Proof: Let P be given.
Assume H1 .
Let x and y be given.
An
exact proof term for the current goal is
SNoS_SNoLev x Hx .
An
exact proof term for the current goal is
SNoS_SNoLev y Hy .
∎
Proof: Let P be given.
Assume H1 .
Let x, y and z be given.
An
exact proof term for the current goal is
SNoS_SNoLev x Hx .
An
exact proof term for the current goal is
SNoS_SNoLev y Hy .
An
exact proof term for the current goal is
SNoS_SNoLev z Hz .
∎
Proof: Let P be given.
We prove the intermediate
claim L1 :
∀alpha, ordinal alpha → ∀ x ∈ SNoS_ alpha , P x .
Let alpha be given.
Let x be given.
Apply SNoS_E2 alpha Ha x Hx to the current goal.
Apply H1 x Hx3 to the current goal.
An
exact proof term for the current goal is
IH (SNoLev x ) Hx1 .
∎
Proof: Let P be given.
Let alpha be given.
Let beta be given.
Let x be given.
Let y be given.
Apply SNoS_E2 alpha Ha x Hx to the current goal.
Apply H1 x y Hx3 Hy3 to the current goal.
Let w be given.
An
exact proof term for the current goal is
IHa (SNoLev x ) Hx1 beta Hb w Hw y Hy .
An
exact proof term for the current goal is
IHb (SNoLev y ) Hy1 x Hx .
Let w be given.
Let z be given.
An
exact proof term for the current goal is
IHa (SNoLev x ) Hx1 (SNoLev y ) Hy2 w Hw z Hz .
∎
Theorem. (
SNoLev_ind3 ) The following is provable:
∀P : set → set → set → prop , (∀x y z, SNo x → SNo y → SNo z → (∀ u ∈ SNoS_ (SNoLev x ) , P u y z ) → (∀ v ∈ SNoS_ (SNoLev y ) , P x v z ) → (∀ w ∈ SNoS_ (SNoLev z ) , P x y w ) → (∀ u ∈ SNoS_ (SNoLev x ) , ∀ v ∈ SNoS_ (SNoLev y ) , P u v z ) → (∀ u ∈ SNoS_ (SNoLev x ) , ∀ w ∈ SNoS_ (SNoLev z ) , P u y w ) → (∀ v ∈ SNoS_ (SNoLev y ) , ∀ w ∈ SNoS_ (SNoLev z ) , P x v w ) → (∀ u ∈ SNoS_ (SNoLev x ) , ∀ v ∈ SNoS_ (SNoLev y ) , ∀ w ∈ SNoS_ (SNoLev z ) , P u v w ) → P x y z ) → ∀x y z, SNo x → SNo y → SNo z → P x y z
Proof: Let P be given.
Let alpha be given.
Let beta be given.
Let gamma be given.
Let x be given.
Let y be given.
Let z be given.
Apply SNoS_E2 alpha Ha x Hx to the current goal.
Apply SNoS_E2 gamma Hc z Hz to the current goal.
Apply H1 x y z Hx3 Hy3 Hz3 to the current goal.
Let u be given.
An
exact proof term for the current goal is
IHa (SNoLev x ) Hx1 beta Hb gamma Hc u Hu y Hy z Hz .
Let v be given.
An
exact proof term for the current goal is
IHb (SNoLev y ) Hy1 gamma Hc x Hx v Hv z Hz .
An
exact proof term for the current goal is
IHc (SNoLev z ) Hz1 x Hx y Hy .
Let u be given.
Let v be given.
An
exact proof term for the current goal is
IHa (SNoLev x ) Hx1 (SNoLev y ) Hy2 gamma Hc u Hu v Hv z Hz .
Let u be given.
Let w be given.
An
exact proof term for the current goal is
IHa (SNoLev x ) Hx1 beta Hb (SNoLev z ) Hz2 u Hu y Hy w Hw .
Let v be given.
Let w be given.
An
exact proof term for the current goal is
IHb (SNoLev y ) Hy1 (SNoLev z ) Hz2 x Hx v Hv w Hw .
Let u be given.
Let v be given.
Let w be given.
An
exact proof term for the current goal is
IHa (SNoLev x ) Hx1 (SNoLev y ) Hy2 (SNoLev z ) Hz2 u Hu v Hv w Hw .
∎
Theorem. (
SNo_omega ) The following is provable:
Theorem. (
SNoLt_0_1 ) The following is provable:
Proof:
An
exact proof term for the current goal is
In_0_1 .
∎
Theorem. (
SNoLt_0_2 ) The following is provable:
Proof:
An
exact proof term for the current goal is
In_0_2 .
∎
Theorem. (
SNoLt_1_2 ) The following is provable:
Proof:
An
exact proof term for the current goal is
In_1_2 .
∎
Proof: Let x be given.
Assume Hx .
Let alpha be given.
Assume Ha .
We prove the intermediate
claim Lx1 :
SNo_ (SNoLev x ) x .
An
exact proof term for the current goal is
SNoLev_ x Hx .
Apply Lx1 to the current goal.
Apply andI to the current goal.
Let beta be given.
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 Hb .
∎
Theorem. (
restr_SNo ) The following is provable:
Proof: Let x be given.
Assume Hx .
Let alpha be given.
Assume Ha .
We prove the intermediate
claim La :
ordinal alpha .
We prove the intermediate
claim L1 :
SNo_ alpha (x ∩ SNoElts_ alpha ) .
An
exact proof term for the current goal is
restr_SNo_ x Hx alpha Ha .
An
exact proof term for the current goal is
SNo_SNo alpha La (x ∩ SNoElts_ alpha ) L1 .
∎
Proof: Let x be given.
Assume Hx .
Let alpha be given.
Assume Ha .
We prove the intermediate
claim La :
ordinal alpha .
We prove the intermediate
claim L1 :
SNo_ alpha (x ∩ SNoElts_ alpha ) .
An
exact proof term for the current goal is
restr_SNo_ x Hx alpha Ha .
∎
Proof: Let x be given.
Assume Hx .
Let alpha be given.
Assume Ha .
Let beta be given.
Apply iffI to the current goal.
An exact proof term for the current goal is H1 .
An exact proof term for the current goal is Hb .
∎
Proof: Let x be given.
Assume Hx .
Apply SNo_eq to the current goal.
An exact proof term for the current goal is Hx .
An exact proof term for the current goal is L1 .
An exact proof term for the current goal is L2 .
Use symmetry.
An exact proof term for the current goal is L1 .
An exact proof term for the current goal is L2 .
∎
Proof: Let x be given.
Assume Hx .
Apply SNo_eq to the current goal.
An exact proof term for the current goal is Hx .
An exact proof term for the current goal is L1 .
An exact proof term for the current goal is L2 .
Use symmetry.
An exact proof term for the current goal is L1 .
An exact proof term for the current goal is L2 .
∎