Search for blocks/addresses/...
Proofgold Address
address
PUK1bKUKofX7u1tPMcmFhy78CZ3qtEeqBQn
total
0
mg
-
conjpub
-
current assets
db51e..
/
d0b08..
bday:
4949
doc published by
Pr6Pc..
Theorem
eq_i_tra
eq_i_tra
:
∀ x0 x1 x2 .
x0
=
x1
⟶
x1
=
x2
⟶
x0
=
x2
(proof)
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Definition
TransSet
TransSet
:=
λ x0 .
∀ x1 .
x1
∈
x0
⟶
x1
⊆
x0
Param
ordsucc
ordsucc
:
ι
→
ι
Definition
or
or
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Known
ordsuccE
ordsuccE
:
∀ x0 x1 .
x1
∈
ordsucc
x0
⟶
or
(
x1
∈
x0
)
(
x1
=
x0
)
Known
Subq_ref
Subq_ref
:
∀ x0 .
x0
⊆
x0
Theorem
TransSet_In_ordsucc_Subq
TransSet_In_ordsucc_Subq
:
∀ x0 x1 .
TransSet
x1
⟶
x0
∈
ordsucc
x1
⟶
x0
⊆
x1
(proof)
Known
set_ext
set_ext
:
∀ x0 x1 .
x0
⊆
x1
⟶
x1
⊆
x0
⟶
x0
=
x1
Known
ReplE_impred
ReplE_impred
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
prim5
x0
x1
⟶
∀ x3 : ο .
(
∀ x4 .
x4
∈
x0
⟶
x2
=
x1
x4
⟶
x3
)
⟶
x3
Known
ReplI
ReplI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
x0
⟶
x1
x2
∈
prim5
x0
x1
Theorem
inv_Repl_eq
inv_Repl_eq
:
∀ x0 .
∀ x1 x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x1
(
x2
x3
)
=
x3
)
⟶
prim5
(
prim5
x0
x2
)
x1
=
x0
(proof)
Theorem
invol_Repl_eq
invol_Repl_eq
:
∀ x0 .
∀ x1 :
ι → ι
.
(
∀ x2 .
x2
∈
x0
⟶
x1
(
x1
x2
)
=
x2
)
⟶
prim5
(
prim5
x0
x1
)
x1
=
x0
(proof)
Param
SNo
SNo
:
ι
→
ο
Param
SNoLt
SNoLt
:
ι
→
ι
→
ο
Known
SNoLt_trichotomy_or
SNoLt_trichotomy_or
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
or
(
or
(
SNoLt
x0
x1
)
(
x0
=
x1
)
)
(
SNoLt
x1
x0
)
Theorem
SNoLt_trichotomy_or_impred
SNoLt_trichotomy_or_impred
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
∀ x2 : ο .
(
SNoLt
x0
x1
⟶
x2
)
⟶
(
x0
=
x1
⟶
x2
)
⟶
(
SNoLt
x1
x0
⟶
x2
)
⟶
x2
(proof)
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Definition
SNoCutP
SNoCutP
:=
λ x0 x1 .
and
(
and
(
∀ x2 .
x2
∈
x0
⟶
SNo
x2
)
(
∀ x2 .
x2
∈
x1
⟶
SNo
x2
)
)
(
∀ x2 .
x2
∈
x0
⟶
∀ x3 .
x3
∈
x1
⟶
SNoLt
x2
x3
)
Param
SNoCut
SNoCut
:
ι
→
ι
→
ι
Param
SNoLev
SNoLev
:
ι
→
ι
Param
binunion
binunion
:
ι
→
ι
→
ι
Param
famunion
famunion
:
ι
→
(
ι
→
ι
) →
ι
Param
SNoEq_
SNoEq_
:
ι
→
ι
→
ι
→
ο
Known
SNoCutP_SNoCut
SNoCutP_SNoCut
:
∀ x0 x1 .
SNoCutP
x0
x1
⟶
and
(
and
(
and
(
and
(
SNo
(
SNoCut
x0
x1
)
)
(
SNoLev
(
SNoCut
x0
x1
)
∈
ordsucc
(
binunion
(
famunion
x0
(
λ x2 .
ordsucc
(
SNoLev
x2
)
)
)
(
famunion
x1
(
λ x2 .
ordsucc
(
SNoLev
x2
)
)
)
)
)
)
(
∀ x2 .
x2
∈
x0
⟶
SNoLt
x2
(
SNoCut
x0
x1
)
)
)
(
∀ x2 .
x2
∈
x1
⟶
SNoLt
(
SNoCut
x0
x1
)
x2
)
)
(
∀ x2 .
SNo
x2
⟶
(
∀ x3 .
x3
∈
x0
⟶
SNoLt
x3
x2
)
⟶
(
∀ x3 .
x3
∈
x1
⟶
SNoLt
x2
x3
)
⟶
and
(
SNoLev
(
SNoCut
x0
x1
)
⊆
SNoLev
x2
)
(
SNoEq_
(
SNoLev
(
SNoCut
x0
x1
)
)
(
SNoCut
x0
x1
)
x2
)
)
Theorem
SNoCutP_SNoCut_impred
SNoCutP_SNoCut_impred
:
∀ x0 x1 .
SNoCutP
x0
x1
⟶
∀ x2 : ο .
(
SNo
(
SNoCut
x0
x1
)
⟶
SNoLev
(
SNoCut
x0
x1
)
∈
ordsucc
(
binunion
(
famunion
x0
(
λ x3 .
ordsucc
(
SNoLev
x3
)
)
)
(
famunion
x1
(
λ x3 .
ordsucc
(
SNoLev
x3
)
)
)
)
⟶
(
∀ x3 .
x3
∈
x0
⟶
SNoLt
x3
(
SNoCut
x0
x1
)
)
⟶
(
∀ x3 .
x3
∈
x1
⟶
SNoLt
(
SNoCut
x0
x1
)
x3
)
⟶
(
∀ x3 .
SNo
x3
⟶
(
∀ x4 .
x4
∈
x0
⟶
SNoLt
x4
x3
)
⟶
(
∀ x4 .
x4
∈
x1
⟶
SNoLt
x3
x4
)
⟶
and
(
SNoLev
(
SNoCut
x0
x1
)
⊆
SNoLev
x3
)
(
SNoEq_
(
SNoLev
(
SNoCut
x0
x1
)
)
(
SNoCut
x0
x1
)
x3
)
)
⟶
x2
)
⟶
x2
(proof)
Definition
ordinal
ordinal
:=
λ x0 .
and
(
TransSet
x0
)
(
∀ x1 .
x1
∈
x0
⟶
TransSet
x1
)
Known
ordinal_In_Or_Subq
ordinal_In_Or_Subq
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
or
(
x0
∈
x1
)
(
x1
⊆
x0
)
Definition
False
False
:=
∀ x0 : ο .
x0
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Known
SNoLt_irref
SNoLt_irref
:
∀ x0 .
not
(
SNoLt
x0
x0
)
Param
SNoLe
SNoLe
:
ι
→
ι
→
ο
Known
SNoLtLe_tra
SNoLtLe_tra
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
x0
x1
⟶
SNoLe
x1
x2
⟶
SNoLt
x0
x2
Known
ordinal_SNo
ordinal_SNo
:
∀ x0 .
ordinal
x0
⟶
SNo
x0
Known
ordinal_Subq_SNoLe
ordinal_Subq_SNoLe
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
x0
⊆
x1
⟶
SNoLe
x0
x1
Theorem
ordinal_SNoLt_In
ordinal_SNoLt_In
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
SNoLt
x0
x1
⟶
x0
∈
x1
(proof)
Known
SNoLeLt_tra
SNoLeLt_tra
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLe
x0
x1
⟶
SNoLt
x1
x2
⟶
SNoLt
x0
x2
Known
ordinal_In_SNoLt
ordinal_In_SNoLt
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
x1
∈
x0
⟶
SNoLt
x1
x0
Theorem
ordinal_SNoLe_Subq
ordinal_SNoLe_Subq
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
SNoLe
x0
x1
⟶
x0
⊆
x1
(proof)
Param
Sep
Sep
:
ι
→
(
ι
→
ο
) →
ι
Param
SNoS_
SNoS_
:
ι
→
ι
Definition
SNoL
SNoL
:=
λ x0 .
{x1 ∈
SNoS_
(
SNoLev
x0
)
|
SNoLt
x1
x0
}
Known
Sep_Subq
Sep_Subq
:
∀ x0 .
∀ x1 :
ι → ο
.
Sep
x0
x1
⊆
x0
Theorem
SNoL_SNoS_
SNoL_SNoS_
:
∀ x0 .
SNoL
x0
⊆
SNoS_
(
SNoLev
x0
)
(proof)
Definition
SNoR
SNoR
:=
λ x0 .
Sep
(
SNoS_
(
SNoLev
x0
)
)
(
SNoLt
x0
)
Theorem
SNoR_SNoS_
SNoR_SNoS_
:
∀ x0 .
SNoR
x0
⊆
SNoS_
(
SNoLev
x0
)
(proof)
Known
SNoL_E
SNoL_E
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
x1
∈
SNoL
x0
⟶
∀ x2 : ο .
(
SNo
x1
⟶
SNoLev
x1
∈
SNoLev
x0
⟶
SNoLt
x1
x0
⟶
x2
)
⟶
x2
Known
SNoS_I2
SNoS_I2
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLev
x0
∈
SNoLev
x1
⟶
x0
∈
SNoS_
(
SNoLev
x1
)
Param
SNo_
SNo_
:
ι
→
ι
→
ο
Known
SNoS_E2
SNoS_E2
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
x1
∈
SNoS_
x0
⟶
∀ x2 : ο .
(
SNoLev
x1
∈
x0
⟶
ordinal
(
SNoLev
x1
)
⟶
SNo
x1
⟶
SNo_
(
SNoLev
x1
)
x1
⟶
x2
)
⟶
x2
Known
SNoL_I
SNoL_I
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
SNo
x1
⟶
SNoLev
x1
∈
SNoLev
x0
⟶
SNoLt
x1
x0
⟶
x1
∈
SNoL
x0
Known
ordinal_SNoLev_max
ordinal_SNoLev_max
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
SNo
x1
⟶
SNoLev
x1
∈
x0
⟶
SNoLt
x1
x0
Known
ordinal_SNoLev
ordinal_SNoLev
:
∀ x0 .
ordinal
x0
⟶
SNoLev
x0
=
x0
Theorem
ordinal_SNoL
ordinal_SNoL
:
∀ x0 .
ordinal
x0
⟶
SNoL
x0
=
SNoS_
x0
(proof)
Known
Empty_Subq_eq
Empty_Subq_eq
:
∀ x0 .
x0
⊆
0
⟶
x0
=
0
Known
SNoR_E
SNoR_E
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
x1
∈
SNoR
x0
⟶
∀ x2 : ο .
(
SNo
x1
⟶
SNoLev
x1
∈
SNoLev
x0
⟶
SNoLt
x0
x1
⟶
x2
)
⟶
x2
Known
SNoLt_tra
SNoLt_tra
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
x0
x1
⟶
SNoLt
x1
x2
⟶
SNoLt
x0
x2
Theorem
ordinal_SNoR
ordinal_SNoR
:
∀ x0 .
ordinal
x0
⟶
SNoR
x0
=
0
(proof)
Known
SNoCutP_SNoL_SNoR
SNoCutP_SNoL_SNoR
:
∀ x0 .
SNo
x0
⟶
SNoCutP
(
SNoL
x0
)
(
SNoR
x0
)
Theorem
ordinal_SNoCutP
ordinal_SNoCutP
:
∀ x0 .
ordinal
x0
⟶
SNoCutP
(
SNoS_
x0
)
0
(proof)
Known
SNo_eta
SNo_eta
:
∀ x0 .
SNo
x0
⟶
x0
=
SNoCut
(
SNoL
x0
)
(
SNoR
x0
)
Theorem
ordinal_SNoCut_eta
ordinal_SNoCut_eta
:
∀ x0 .
ordinal
x0
⟶
x0
=
SNoCut
(
SNoS_
x0
)
0
(proof)
Known
ordinal_Empty
ordinal_Empty
:
ordinal
0
Theorem
SNo_0
SNo_0
:
SNo
0
(proof)
Theorem
SNoLev_0
SNoLev_0
:
SNoLev
0
=
0
(proof)
Definition
nIn
nIn
:=
λ x0 x1 .
not
(
x0
∈
x1
)
Known
EmptyE
EmptyE
:
∀ x0 .
nIn
x0
0
Theorem
SNoL_0
SNoL_0
:
SNoL
0
=
0
(proof)
Theorem
SNoR_0
SNoR_0
:
SNoR
0
=
0
(proof)
Known
SNoLeE
SNoLeE
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLe
x0
x1
⟶
or
(
SNoLt
x0
x1
)
(
x0
=
x1
)
Param
binintersect
binintersect
:
ι
→
ι
→
ι
Known
SNoLtE
SNoLtE
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLt
x0
x1
⟶
∀ x2 : ο .
(
∀ x3 .
SNo
x3
⟶
SNoLev
x3
∈
binintersect
(
SNoLev
x0
)
(
SNoLev
x1
)
⟶
SNoEq_
(
SNoLev
x3
)
x3
x0
⟶
SNoEq_
(
SNoLev
x3
)
x3
x1
⟶
SNoLt
x0
x3
⟶
SNoLt
x3
x1
⟶
nIn
(
SNoLev
x3
)
x0
⟶
SNoLev
x3
∈
x1
⟶
x2
)
⟶
(
SNoLev
x0
∈
SNoLev
x1
⟶
SNoEq_
(
SNoLev
x0
)
x0
x1
⟶
SNoLev
x0
∈
x1
⟶
x2
)
⟶
(
SNoLev
x1
∈
SNoLev
x0
⟶
SNoEq_
(
SNoLev
x1
)
x0
x1
⟶
nIn
(
SNoLev
x1
)
x0
⟶
x2
)
⟶
x2
Known
SNoS_I
SNoS_I
:
∀ x0 .
ordinal
x0
⟶
∀ x1 x2 .
x2
∈
x0
⟶
SNo_
x2
x1
⟶
x1
∈
SNoS_
x0
Known
SNoLev_
SNoLev_
:
∀ x0 .
SNo
x0
⟶
SNo_
(
SNoLev
x0
)
x0
Known
In_irref
In_irref
:
∀ x0 .
nIn
x0
x0
Known
ordinal_SNoLev_max_2
ordinal_SNoLev_max_2
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
SNo
x1
⟶
SNoLev
x1
∈
ordsucc
x0
⟶
SNoLe
x1
x0
Known
ordsuccI2
ordsuccI2
:
∀ x0 .
x0
∈
ordsucc
x0
Known
SNoLev_ordinal
SNoLev_ordinal
:
∀ x0 .
SNo
x0
⟶
ordinal
(
SNoLev
x0
)
Theorem
SNo_max_SNoLev
SNo_max_SNoLev
:
∀ x0 .
SNo
x0
⟶
(
∀ x1 .
x1
∈
SNoS_
(
SNoLev
x0
)
⟶
SNoLt
x1
x0
)
⟶
SNoLev
x0
=
x0
(proof)
Theorem
SNo_max_ordinal
SNo_max_ordinal
:
∀ x0 .
SNo
x0
⟶
(
∀ x1 .
x1
∈
SNoS_
(
SNoLev
x0
)
⟶
SNoLt
x1
x0
)
⟶
ordinal
x0
(proof)
Param
SNo_extend0
SNo_extend0
:
ι
→
ι
Known
SNoLtI3
SNoLtI3
:
∀ x0 x1 .
SNoLev
x1
∈
SNoLev
x0
⟶
SNoEq_
(
SNoLev
x1
)
x0
x1
⟶
nIn
(
SNoLev
x1
)
x0
⟶
SNoLt
x0
x1
Known
SNo_extend0_SNoLev
SNo_extend0_SNoLev
:
∀ x0 .
SNo
x0
⟶
SNoLev
(
SNo_extend0
x0
)
=
ordsucc
(
SNoLev
x0
)
Known
SNo_extend0_SNoEq
SNo_extend0_SNoEq
:
∀ x0 .
SNo
x0
⟶
SNoEq_
(
SNoLev
x0
)
(
SNo_extend0
x0
)
x0
Known
SNo_extend0_nIn
SNo_extend0_nIn
:
∀ x0 .
SNo
x0
⟶
nIn
(
SNoLev
x0
)
(
SNo_extend0
x0
)
Theorem
SNo_extend0_Lt
SNo_extend0_Lt
:
∀ x0 .
SNo
x0
⟶
SNoLt
(
SNo_extend0
x0
)
x0
(proof)
Param
SNo_extend1
SNo_extend1
:
ι
→
ι
Known
SNoLtI2
SNoLtI2
:
∀ x0 x1 .
SNoLev
x0
∈
SNoLev
x1
⟶
SNoEq_
(
SNoLev
x0
)
x0
x1
⟶
SNoLev
x0
∈
x1
⟶
SNoLt
x0
x1
Known
SNo_extend1_SNoLev
SNo_extend1_SNoLev
:
∀ x0 .
SNo
x0
⟶
SNoLev
(
SNo_extend1
x0
)
=
ordsucc
(
SNoLev
x0
)
Known
SNoEq_sym_
SNoEq_sym_
:
∀ x0 x1 x2 .
SNoEq_
x0
x1
x2
⟶
SNoEq_
x0
x2
x1
Known
SNo_extend1_SNoEq
SNo_extend1_SNoEq
:
∀ x0 .
SNo
x0
⟶
SNoEq_
(
SNoLev
x0
)
(
SNo_extend1
x0
)
x0
Known
SNo_extend1_In
SNo_extend1_In
:
∀ x0 .
SNo
x0
⟶
SNoLev
x0
∈
SNo_extend1
x0
Theorem
SNo_extend1_Gt
SNo_extend1_Gt
:
∀ x0 .
SNo
x0
⟶
SNoLt
x0
(
SNo_extend1
x0
)
(proof)
Param
In_rec_ii
In_rec_ii
:
(
ι
→
(
ι
→
ι
→
ι
) →
ι
→
ι
) →
ι
→
ι
→
ι
Param
If_ii
If_ii
:
ο
→
(
ι
→
ι
) →
(
ι
→
ι
) →
ι
→
ι
Param
If_i
If_i
:
ο
→
ι
→
ι
→
ι
Param
True
True
:
ο
Definition
SNo_rec_i
SNo_rec_i
:=
λ x0 :
ι →
(
ι → ι
)
→ ι
.
λ x1 .
In_rec_ii
(
λ x2 .
λ x3 :
ι →
ι → ι
.
If_ii
(
ordinal
x2
)
(
λ x4 .
If_i
(
x4
∈
SNoS_
(
ordsucc
x2
)
)
(
x0
x4
(
λ x5 .
x3
(
SNoLev
x5
)
x5
)
)
(
prim0
(
λ x5 .
True
)
)
)
(
λ x4 .
prim0
(
λ x5 .
True
)
)
)
(
SNoLev
x1
)
x1
Known
In_rec_ii_eq
In_rec_ii_eq
:
∀ x0 :
ι →
(
ι →
ι → ι
)
→
ι → ι
.
(
∀ x1 .
∀ x2 x3 :
ι →
ι → ι
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
In_rec_ii
x0
x1
=
x0
x1
(
In_rec_ii
x0
)
Known
If_ii_1
If_ii_1
:
∀ x0 : ο .
∀ x1 x2 :
ι → ι
.
x0
⟶
If_ii
x0
x1
x2
=
x1
Known
If_i_1
If_i_1
:
∀ x0 : ο .
∀ x1 x2 .
x0
⟶
If_i
x0
x1
x2
=
x1
Known
SNoS_SNoLev
SNoS_SNoLev
:
∀ x0 .
SNo
x0
⟶
x0
∈
SNoS_
(
ordsucc
(
SNoLev
x0
)
)
Known
xm
xm
:
∀ x0 : ο .
or
x0
(
not
x0
)
Known
ordinal_ordsucc
ordinal_ordsucc
:
∀ x0 .
ordinal
x0
⟶
ordinal
(
ordsucc
x0
)
Known
If_i_0
If_i_0
:
∀ x0 : ο .
∀ x1 x2 .
not
x0
⟶
If_i
x0
x1
x2
=
x2
Known
If_ii_0
If_ii_0
:
∀ x0 : ο .
∀ x1 x2 :
ι → ι
.
not
x0
⟶
If_ii
x0
x1
x2
=
x2
Theorem
SNo_rec_i_eq
SNo_rec_i_eq
:
∀ x0 :
ι →
(
ι → ι
)
→ ι
.
(
∀ x1 .
SNo
x1
⟶
∀ x2 x3 :
ι → ι
.
(
∀ x4 .
x4
∈
SNoS_
(
SNoLev
x1
)
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
SNo
x1
⟶
SNo_rec_i
x0
x1
=
x0
x1
(
SNo_rec_i
x0
)
(proof)
Param
In_rec_iii
In_rec_iii
:
(
ι
→
(
ι
→
ι
→
ι
→
ι
) →
ι
→
ι
→
ι
) →
ι
→
ι
→
ι
→
ι
Param
If_iii
If_iii
:
ο
→
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
ι
→
ι
→
ι
Param
Descr_ii
Descr_ii
:
(
(
ι
→
ι
) →
ο
) →
ι
→
ι
Definition
SNo_rec_ii
SNo_rec_ii
:=
λ x0 :
ι →
(
ι →
ι → ι
)
→
ι → ι
.
λ x1 .
In_rec_iii
(
λ x2 .
λ x3 :
ι →
ι →
ι → ι
.
If_iii
(
ordinal
x2
)
(
λ x4 .
If_ii
(
x4
∈
SNoS_
(
ordsucc
x2
)
)
(
x0
x4
(
λ x5 .
x3
(
SNoLev
x5
)
x5
)
)
(
Descr_ii
(
λ x5 :
ι → ι
.
True
)
)
)
(
λ x4 .
Descr_ii
(
λ x5 :
ι → ι
.
True
)
)
)
(
SNoLev
x1
)
x1
Known
In_rec_iii_eq
In_rec_iii_eq
:
∀ x0 :
ι →
(
ι →
ι →
ι → ι
)
→
ι →
ι → ι
.
(
∀ x1 .
∀ x2 x3 :
ι →
ι →
ι → ι
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
In_rec_iii
x0
x1
=
x0
x1
(
In_rec_iii
x0
)
Known
If_iii_1
If_iii_1
:
∀ x0 : ο .
∀ x1 x2 :
ι →
ι → ι
.
x0
⟶
If_iii
x0
x1
x2
=
x1
Known
If_iii_0
If_iii_0
:
∀ x0 : ο .
∀ x1 x2 :
ι →
ι → ι
.
not
x0
⟶
If_iii
x0
x1
x2
=
x2
Theorem
SNo_rec_ii_eq
SNo_rec_ii_eq
:
∀ x0 :
ι →
(
ι →
ι → ι
)
→
ι → ι
.
(
∀ x1 .
SNo
x1
⟶
∀ x2 x3 :
ι →
ι → ι
.
(
∀ x4 .
x4
∈
SNoS_
(
SNoLev
x1
)
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x2
=
x0
x1
x3
)
⟶
∀ x1 .
SNo
x1
⟶
SNo_rec_ii
x0
x1
=
x0
x1
(
SNo_rec_ii
x0
)
(proof)
Known
SNoS_In_neq
SNoS_In_neq
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
x1
∈
SNoS_
(
SNoLev
x0
)
⟶
x1
=
x0
⟶
∀ x2 : ο .
x2
Theorem
SNo_rec2_G_prop
SNo_rec2_G_prop
:
∀ x0 :
ι →
ι →
(
ι →
ι → ι
)
→ ι
.
(
∀ x1 .
SNo
x1
⟶
∀ x2 .
SNo
x2
⟶
∀ x3 x4 :
ι →
ι → ι
.
(
∀ x5 .
x5
∈
SNoS_
(
SNoLev
x1
)
⟶
∀ x6 .
SNo
x6
⟶
x3
x5
x6
=
x4
x5
x6
)
⟶
(
∀ x5 .
x5
∈
SNoS_
(
SNoLev
x2
)
⟶
x3
x1
x5
=
x4
x1
x5
)
⟶
x0
x1
x2
x3
=
x0
x1
x2
x4
)
⟶
∀ x1 .
SNo
x1
⟶
∀ x2 x3 :
ι →
ι → ι
.
(
∀ x4 .
x4
∈
SNoS_
(
SNoLev
x1
)
⟶
x2
x4
=
x3
x4
)
⟶
∀ x4 .
SNo
x4
⟶
∀ x5 x6 :
ι → ι
.
(
∀ x7 .
x7
∈
SNoS_
(
SNoLev
x4
)
⟶
x5
x7
=
x6
x7
)
⟶
x0
x1
x4
(
λ x8 x9 .
If_i
(
x8
=
x1
)
(
x5
x9
)
(
x2
x8
x9
)
)
=
x0
x1
x4
(
λ x8 x9 .
If_i
(
x8
=
x1
)
(
x6
x9
)
(
x3
x8
x9
)
)
(proof)
Theorem
SNo_rec2_eq_1
SNo_rec2_eq_1
:
∀ x0 :
ι →
ι →
(
ι →
ι → ι
)
→ ι
.
(
∀ x1 .
SNo
x1
⟶
∀ x2 .
SNo
x2
⟶
∀ x3 x4 :
ι →
ι → ι
.
(
∀ x5 .
x5
∈
SNoS_
(
SNoLev
x1
)
⟶
∀ x6 .
SNo
x6
⟶
x3
x5
x6
=
x4
x5
x6
)
⟶
(
∀ x5 .
x5
∈
SNoS_
(
SNoLev
x2
)
⟶
x3
x1
x5
=
x4
x1
x5
)
⟶
x0
x1
x2
x3
=
x0
x1
x2
x4
)
⟶
∀ x1 .
SNo
x1
⟶
∀ x2 :
ι →
ι → ι
.
∀ x3 .
SNo
x3
⟶
SNo_rec_i
(
λ x5 .
λ x6 :
ι → ι
.
x0
x1
x5
(
λ x7 x8 .
If_i
(
x7
=
x1
)
(
x6
x8
)
(
x2
x7
x8
)
)
)
x3
=
x0
x1
x3
(
λ x5 x6 .
If_i
(
x5
=
x1
)
(
SNo_rec_i
(
λ x7 .
λ x8 :
ι → ι
.
x0
x1
x7
(
λ x9 x10 .
If_i
(
x9
=
x1
)
(
x8
x10
)
(
x2
x9
x10
)
)
)
x6
)
(
x2
x5
x6
)
)
(proof)
Definition
SNo_rec2
SNo_rec2
:=
λ x0 :
ι →
ι →
(
ι →
ι → ι
)
→ ι
.
SNo_rec_ii
(
λ x1 .
λ x2 :
ι →
ι → ι
.
λ x3 .
If_i
(
SNo
x3
)
(
SNo_rec_i
(
λ x4 .
λ x5 :
ι → ι
.
x0
x1
x4
(
λ x6 x7 .
If_i
(
x6
=
x1
)
(
x5
x7
)
(
x2
x6
x7
)
)
)
x3
)
0
)
Known
ordinal_ind
ordinal_ind
:
∀ x0 :
ι → ο
.
(
∀ x1 .
ordinal
x1
⟶
(
∀ x2 .
x2
∈
x1
⟶
x0
x2
)
⟶
x0
x1
)
⟶
∀ x1 .
ordinal
x1
⟶
x0
x1
Theorem
SNo_rec2_eq
SNo_rec2_eq
:
∀ x0 :
ι →
ι →
(
ι →
ι → ι
)
→ ι
.
(
∀ x1 .
SNo
x1
⟶
∀ x2 .
SNo
x2
⟶
∀ x3 x4 :
ι →
ι → ι
.
(
∀ x5 .
x5
∈
SNoS_
(
SNoLev
x1
)
⟶
∀ x6 .
SNo
x6
⟶
x3
x5
x6
=
x4
x5
x6
)
⟶
(
∀ x5 .
x5
∈
SNoS_
(
SNoLev
x2
)
⟶
x3
x1
x5
=
x4
x1
x5
)
⟶
x0
x1
x2
x3
=
x0
x1
x2
x4
)
⟶
∀ x1 .
SNo
x1
⟶
∀ x2 .
SNo
x2
⟶
SNo_rec2
x0
x1
x2
=
x0
x1
x2
(
SNo_rec2
x0
)
(proof)
Theorem
SNo_ordinal_ind
SNo_ordinal_ind
:
∀ x0 :
ι → ο
.
(
∀ x1 .
ordinal
x1
⟶
∀ x2 .
x2
∈
SNoS_
x1
⟶
x0
x2
)
⟶
∀ x1 .
SNo
x1
⟶
x0
x1
(proof)
Theorem
SNo_ordinal_ind2
SNo_ordinal_ind2
:
∀ x0 :
ι →
ι → ο
.
(
∀ x1 .
ordinal
x1
⟶
∀ x2 .
ordinal
x2
⟶
∀ x3 .
x3
∈
SNoS_
x1
⟶
∀ x4 .
x4
∈
SNoS_
x2
⟶
x0
x3
x4
)
⟶
∀ x1 x2 .
SNo
x1
⟶
SNo
x2
⟶
x0
x1
x2
(proof)
Theorem
SNo_ordinal_ind3
SNo_ordinal_ind3
:
∀ x0 :
ι →
ι →
ι → ο
.
(
∀ x1 .
ordinal
x1
⟶
∀ x2 .
ordinal
x2
⟶
∀ x3 .
ordinal
x3
⟶
∀ x4 .
x4
∈
SNoS_
x1
⟶
∀ x5 .
x5
∈
SNoS_
x2
⟶
∀ x6 .
x6
∈
SNoS_
x3
⟶
x0
x4
x5
x6
)
⟶
∀ x1 x2 x3 .
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
x0
x1
x2
x3
(proof)
Theorem
SNoLev_ind
SNoLev_ind
:
∀ x0 :
ι → ο
.
(
∀ x1 .
SNo
x1
⟶
(
∀ x2 .
x2
∈
SNoS_
(
SNoLev
x1
)
⟶
x0
x2
)
⟶
x0
x1
)
⟶
∀ x1 .
SNo
x1
⟶
x0
x1
(proof)
Theorem
SNoLev_ind2
SNoLev_ind2
:
∀ x0 :
ι →
ι → ο
.
(
∀ x1 x2 .
SNo
x1
⟶
SNo
x2
⟶
(
∀ x3 .
x3
∈
SNoS_
(
SNoLev
x1
)
⟶
x0
x3
x2
)
⟶
(
∀ x3 .
x3
∈
SNoS_
(
SNoLev
x2
)
⟶
x0
x1
x3
)
⟶
(
∀ x3 .
x3
∈
SNoS_
(
SNoLev
x1
)
⟶
∀ x4 .
x4
∈
SNoS_
(
SNoLev
x2
)
⟶
x0
x3
x4
)
⟶
x0
x1
x2
)
⟶
∀ x1 x2 .
SNo
x1
⟶
SNo
x2
⟶
x0
x1
x2
(proof)
Theorem
SNoLev_ind3
SNoLev_ind3
:
∀ x0 :
ι →
ι →
ι → ο
.
(
∀ x1 x2 x3 .
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
(
∀ x4 .
x4
∈
SNoS_
(
SNoLev
x1
)
⟶
x0
x4
x2
x3
)
⟶
(
∀ x4 .
x4
∈
SNoS_
(
SNoLev
x2
)
⟶
x0
x1
x4
x3
)
⟶
(
∀ x4 .
x4
∈
SNoS_
(
SNoLev
x3
)
⟶
x0
x1
x2
x4
)
⟶
(
∀ x4 .
x4
∈
SNoS_
(
SNoLev
x1
)
⟶
∀ x5 .
x5
∈
SNoS_
(
SNoLev
x2
)
⟶
x0
x4
x5
x3
)
⟶
(
∀ x4 .
x4
∈
SNoS_
(
SNoLev
x1
)
⟶
∀ x5 .
x5
∈
SNoS_
(
SNoLev
x3
)
⟶
x0
x4
x2
x5
)
⟶
(
∀ x4 .
x4
∈
SNoS_
(
SNoLev
x2
)
⟶
∀ x5 .
x5
∈
SNoS_
(
SNoLev
x3
)
⟶
x0
x1
x4
x5
)
⟶
(
∀ x4 .
x4
∈
SNoS_
(
SNoLev
x1
)
⟶
∀ x5 .
x5
∈
SNoS_
(
SNoLev
x2
)
⟶
∀ x6 .
x6
∈
SNoS_
(
SNoLev
x3
)
⟶
x0
x4
x5
x6
)
⟶
x0
x1
x2
x3
)
⟶
∀ x1 x2 x3 .
SNo
x1
⟶
SNo
x2
⟶
SNo
x3
⟶
x0
x1
x2
x3
(proof)
Param
nat_p
nat_p
:
ι
→
ο
Known
nat_p_ordinal
nat_p_ordinal
:
∀ x0 .
nat_p
x0
⟶
ordinal
x0
Known
nat_1
nat_1
:
nat_p
1
Theorem
SNo_1
SNo_1
:
SNo
1
(proof)
Known
nat_2
nat_2
:
nat_p
2
Theorem
SNo_2
SNo_2
:
SNo
2
(proof)
Param
omega
omega
:
ι
Known
omega_ordinal
omega_ordinal
:
ordinal
omega
Theorem
SNo_omega
SNo_omega
:
SNo
omega
(proof)
Known
ordinal_1
ordinal_1
:
ordinal
1
Known
In_0_1
In_0_1
:
0
∈
1
Theorem
SNoLt_0_1
SNoLt_0_1
:
SNoLt
0
1
(proof)
Known
ordinal_2
ordinal_2
:
ordinal
2
Known
In_0_2
In_0_2
:
0
∈
2
Theorem
SNoLt_0_2
SNoLt_0_2
:
SNoLt
0
2
(proof)
Known
In_1_2
In_1_2
:
1
∈
2
Theorem
SNoLt_1_2
SNoLt_1_2
:
SNoLt
1
2
(proof)
Definition
minus_SNo
minus_SNo
:=
SNo_rec_i
(
λ x0 .
λ x1 :
ι → ι
.
SNoCut
(
prim5
(
SNoR
x0
)
x1
)
(
prim5
(
SNoL
x0
)
x1
)
)
Known
ReplEq_ext
ReplEq_ext
:
∀ x0 .
∀ x1 x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x0
⟶
x1
x3
=
x2
x3
)
⟶
prim5
x0
x1
=
prim5
x0
x2
Known
SNoL_SNoS
SNoL_SNoS
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
x1
∈
SNoL
x0
⟶
x1
∈
SNoS_
(
SNoLev
x0
)
Known
SNoR_SNoS
SNoR_SNoS
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
x1
∈
SNoR
x0
⟶
x1
∈
SNoS_
(
SNoLev
x0
)
Theorem
minus_SNo_eq
minus_SNo_eq
:
∀ x0 .
SNo
x0
⟶
minus_SNo
x0
=
SNoCut
(
prim5
(
SNoR
x0
)
minus_SNo
)
(
prim5
(
SNoL
x0
)
minus_SNo
)
(proof)
Known
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Known
and3I
and3I
:
∀ x0 x1 x2 : ο .
x0
⟶
x1
⟶
x2
⟶
and
(
and
x0
x1
)
x2
Known
SNoCutP_SNoCut_R
SNoCutP_SNoCut_R
:
∀ x0 x1 .
SNoCutP
x0
x1
⟶
∀ x2 .
x2
∈
x1
⟶
SNoLt
(
SNoCut
x0
x1
)
x2
Known
SNoCutP_SNoCut_L
SNoCutP_SNoCut_L
:
∀ x0 x1 .
SNoCutP
x0
x1
⟶
∀ x2 .
x2
∈
x0
⟶
SNoLt
x2
(
SNoCut
x0
x1
)
Known
SNoCutP_SNo_SNoCut
SNoCutP_SNo_SNoCut
:
∀ x0 x1 .
SNoCutP
x0
x1
⟶
SNo
(
SNoCut
x0
x1
)
Known
SNoLev_prop
SNoLev_prop
:
∀ x0 .
SNo
x0
⟶
and
(
ordinal
(
SNoLev
x0
)
)
(
SNo_
(
SNoLev
x0
)
x0
)
Known
binintersectE
binintersectE
:
∀ x0 x1 x2 .
x2
∈
binintersect
x0
x1
⟶
and
(
x2
∈
x0
)
(
x2
∈
x1
)
Known
SepI
SepI
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
x0
⟶
x1
x2
⟶
x2
∈
Sep
x0
x1
Theorem
minus_SNo_prop1
minus_SNo_prop1
:
∀ x0 .
SNo
x0
⟶
and
(
and
(
and
(
SNo
(
minus_SNo
x0
)
)
(
∀ x1 .
x1
∈
SNoL
x0
⟶
SNoLt
(
minus_SNo
x0
)
(
minus_SNo
x1
)
)
)
(
∀ x1 .
x1
∈
SNoR
x0
⟶
SNoLt
(
minus_SNo
x1
)
(
minus_SNo
x0
)
)
)
(
SNoCutP
(
prim5
(
SNoR
x0
)
minus_SNo
)
(
prim5
(
SNoL
x0
)
minus_SNo
)
)
(proof)
Theorem
SNo_minus_SNo
SNo_minus_SNo
:
∀ x0 .
SNo
x0
⟶
SNo
(
minus_SNo
x0
)
(proof)
Theorem
minus_SNo_Lt_contra
minus_SNo_Lt_contra
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLt
x0
x1
⟶
SNoLt
(
minus_SNo
x1
)
(
minus_SNo
x0
)
(proof)
Known
SNoLtLe
SNoLtLe
:
∀ x0 x1 .
SNoLt
x0
x1
⟶
SNoLe
x0
x1
Known
SNoLe_ref
SNoLe_ref
:
∀ x0 .
SNoLe
x0
x0
Theorem
minus_SNo_Le_contra
minus_SNo_Le_contra
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLe
x0
x1
⟶
SNoLe
(
minus_SNo
x1
)
(
minus_SNo
x0
)
(proof)
Theorem
minus_SNo_SNoCutP
minus_SNo_SNoCutP
:
∀ x0 .
SNo
x0
⟶
SNoCutP
(
prim5
(
SNoR
x0
)
minus_SNo
)
(
prim5
(
SNoL
x0
)
minus_SNo
)
(proof)
Theorem
minus_SNo_SNoCutP_gen
minus_SNo_SNoCutP_gen
:
∀ x0 x1 .
SNoCutP
x0
x1
⟶
SNoCutP
(
prim5
x1
minus_SNo
)
(
prim5
x0
minus_SNo
)
(proof)
Known
binunionE
binunionE
:
∀ x0 x1 x2 .
x2
∈
binunion
x0
x1
⟶
or
(
x2
∈
x0
)
(
x2
∈
x1
)
Known
famunionE
famunionE
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
famunion
x0
x1
⟶
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
x0
)
(
x2
∈
x1
x4
)
⟶
x3
)
⟶
x3
Known
In_no2cycle
In_no2cycle
:
∀ x0 x1 .
x0
∈
x1
⟶
x1
∈
x0
⟶
False
Known
ordinal_Hered
ordinal_Hered
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
x1
∈
x0
⟶
ordinal
x1
Known
ordinal_ordsucc_In_eq
ordinal_ordsucc_In_eq
:
∀ x0 x1 .
ordinal
x0
⟶
x1
∈
x0
⟶
or
(
ordsucc
x1
∈
x0
)
(
x0
=
ordsucc
x1
)
Known
ordinal_binunion
ordinal_binunion
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
ordinal
(
binunion
x0
x1
)
Known
ordinal_famunion
ordinal_famunion
:
∀ x0 .
∀ x1 :
ι → ι
.
(
∀ x2 .
x2
∈
x0
⟶
ordinal
(
x1
x2
)
)
⟶
ordinal
(
famunion
x0
x1
)
Theorem
minus_SNo_Lev_lem1
minus_SNo_Lev_lem1
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
x1
∈
SNoS_
x0
⟶
SNoLev
(
minus_SNo
x1
)
⊆
SNoLev
x1
(proof)
Theorem
minus_SNo_Lev_lem2
minus_SNo_Lev_lem2
:
∀ x0 .
SNo
x0
⟶
SNoLev
(
minus_SNo
x0
)
⊆
SNoLev
x0
(proof)
Known
SNo_ind
SNo_ind
:
∀ x0 :
ι → ο
.
(
∀ x1 x2 .
SNoCutP
x1
x2
⟶
(
∀ x3 .
x3
∈
x1
⟶
x0
x3
)
⟶
(
∀ x3 .
x3
∈
x2
⟶
x0
x3
)
⟶
x0
(
SNoCut
x1
x2
)
)
⟶
∀ x1 .
SNo
x1
⟶
x0
x1
Known
SNo_eq
SNo_eq
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLev
x0
=
SNoLev
x1
⟶
SNoEq_
(
SNoLev
x0
)
x0
x1
⟶
x0
=
x1
Known
Subq_tra
Subq_tra
:
∀ x0 x1 x2 .
x0
⊆
x1
⟶
x1
⊆
x2
⟶
x0
⊆
x2
Known
SNoCutP_SNoCut_fst
SNoCutP_SNoCut_fst
:
∀ x0 x1 .
SNoCutP
x0
x1
⟶
∀ x2 .
SNo
x2
⟶
(
∀ x3 .
x3
∈
x0
⟶
SNoLt
x3
x2
)
⟶
(
∀ x3 .
x3
∈
x1
⟶
SNoLt
x2
x3
)
⟶
and
(
SNoLev
(
SNoCut
x0
x1
)
⊆
SNoLev
x2
)
(
SNoEq_
(
SNoLev
(
SNoCut
x0
x1
)
)
(
SNoCut
x0
x1
)
x2
)
Theorem
minus_SNo_invol
minus_SNo_invol
:
∀ x0 .
SNo
x0
⟶
minus_SNo
(
minus_SNo
x0
)
=
x0
(proof)
Theorem
minus_SNo_Lev
minus_SNo_Lev
:
∀ x0 .
SNo
x0
⟶
SNoLev
(
minus_SNo
x0
)
=
SNoLev
x0
(proof)
Known
SNoLev_uniq2
SNoLev_uniq2
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
SNo_
x0
x1
⟶
SNoLev
x1
=
x0
Known
SNo_SNo
SNo_SNo
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
SNo_
x0
x1
⟶
SNo
x1
Theorem
minus_SNo_SNo_
minus_SNo_SNo_
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
SNo_
x0
x1
⟶
SNo_
x0
(
minus_SNo
x1
)
(proof)
Theorem
minus_SNo_SNoS_
minus_SNo_SNoS_
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
x1
∈
SNoS_
x0
⟶
minus_SNo
x1
∈
SNoS_
x0
(proof)
Theorem
minus_SNoCut_eq_lem
minus_SNoCut_eq_lem
:
∀ x0 .
SNo
x0
⟶
∀ x1 x2 .
SNoCutP
x1
x2
⟶
x0
=
SNoCut
x1
x2
⟶
minus_SNo
x0
=
SNoCut
(
prim5
x2
minus_SNo
)
(
prim5
x1
minus_SNo
)
(proof)
Theorem
minus_SNoCut_eq
minus_SNoCut_eq
:
∀ x0 x1 .
SNoCutP
x0
x1
⟶
minus_SNo
(
SNoCut
x0
x1
)
=
SNoCut
(
prim5
x1
minus_SNo
)
(
prim5
x0
minus_SNo
)
(proof)
Theorem
minus_SNo_Lt_contra1
minus_SNo_Lt_contra1
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLt
(
minus_SNo
x0
)
x1
⟶
SNoLt
(
minus_SNo
x1
)
x0
(proof)
Theorem
minus_SNo_Lt_contra2
minus_SNo_Lt_contra2
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLt
x0
(
minus_SNo
x1
)
⟶
SNoLt
x1
(
minus_SNo
x0
)
(proof)
Theorem
minus_SNo_Lt_contra3
minus_SNo_Lt_contra3
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNoLt
(
minus_SNo
x0
)
(
minus_SNo
x1
)
⟶
SNoLt
x1
x0
(proof)
Theorem
SNo_momega
SNo_momega
:
SNo
(
minus_SNo
omega
)
(proof)
Theorem
mordinal_SNo
mordinal_SNo
:
∀ x0 .
ordinal
x0
⟶
SNo
(
minus_SNo
x0
)
(proof)
Theorem
mordinal_SNoLev
mordinal_SNoLev
:
∀ x0 .
ordinal
x0
⟶
SNoLev
(
minus_SNo
x0
)
=
x0
(proof)
Theorem
mordinal_SNoLev_min
mordinal_SNoLev_min
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
SNo
x1
⟶
SNoLev
x1
∈
x0
⟶
SNoLt
(
minus_SNo
x0
)
x1
(proof)
Theorem
mordinal_SNoLev_min_2
mordinal_SNoLev_min_2
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
SNo
x1
⟶
SNoLev
x1
∈
ordsucc
x0
⟶
SNoLe
(
minus_SNo
x0
)
x1
(proof)
Definition
add_SNo
add_SNo
:=
SNo_rec2
(
λ x0 x1 .
λ x2 :
ι →
ι → ι
.
SNoCut
(
binunion
{
x2
x3
x1
|x3 ∈
SNoL
x0
}
(
prim5
(
SNoL
x1
)
(
x2
x0
)
)
)
(
binunion
{
x2
x3
x1
|x3 ∈
SNoR
x0
}
(
prim5
(
SNoR
x1
)
(
x2
x0
)
)
)
)
Theorem
add_SNo_eq
add_SNo_eq
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
SNo
x1
⟶
add_SNo
x0
x1
=
SNoCut
(
binunion
{
add_SNo
x3
x1
|x3 ∈
SNoL
x0
}
(
prim5
(
SNoL
x1
)
(
add_SNo
x0
)
)
)
(
binunion
{
add_SNo
x3
x1
|x3 ∈
SNoR
x0
}
(
prim5
(
SNoR
x1
)
(
add_SNo
x0
)
)
)
(proof)
Param
setprod
setprod
:
ι
→
ι
→
ι
Param
ap
ap
:
ι
→
ι
→
ι
Definition
mul_SNo
mul_SNo
:=
SNo_rec2
(
λ x0 x1 .
λ x2 :
ι →
ι → ι
.
SNoCut
(
binunion
{
add_SNo
(
x2
(
ap
x3
0
)
x1
)
(
add_SNo
(
x2
x0
(
ap
x3
1
)
)
(
minus_SNo
(
x2
(
ap
x3
0
)
(
ap
x3
1
)
)
)
)
|x3 ∈
setprod
(
SNoL
x0
)
(
SNoL
x1
)
}
{
add_SNo
(
x2
(
ap
x3
0
)
x1
)
(
add_SNo
(
x2
x0
(
ap
x3
1
)
)
(
minus_SNo
(
x2
(
ap
x3
0
)
(
ap
x3
1
)
)
)
)
|x3 ∈
setprod
(
SNoR
x0
)
(
SNoR
x1
)
}
)
(
binunion
{
add_SNo
(
x2
(
ap
x3
0
)
x1
)
(
add_SNo
(
x2
x0
(
ap
x3
1
)
)
(
minus_SNo
(
x2
(
ap
x3
0
)
(
ap
x3
1
)
)
)
)
|x3 ∈
setprod
(
SNoL
x0
)
(
SNoR
x1
)
}
{
add_SNo
(
x2
(
ap
x3
0
)
x1
)
(
add_SNo
(
x2
x0
(
ap
x3
1
)
)
(
minus_SNo
(
x2
(
ap
x3
0
)
(
ap
x3
1
)
)
)
)
|x3 ∈
setprod
(
SNoR
x0
)
(
SNoL
x1
)
}
)
)
Known
ReplEq_setprod_ext
ReplEq_setprod_ext
:
∀ x0 x1 .
∀ x2 x3 :
ι →
ι → ι
.
(
∀ x4 .
x4
∈
x0
⟶
∀ x5 .
x5
∈
x1
⟶
x2
x4
x5
=
x3
x4
x5
)
⟶
{
x2
(
ap
x5
0
)
(
ap
x5
1
)
|x5 ∈
setprod
x0
x1
}
=
{
x3
(
ap
x5
0
)
(
ap
x5
1
)
|x5 ∈
setprod
x0
x1
}
Theorem
mul_SNo_eq
mul_SNo_eq
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
SNo
x1
⟶
mul_SNo
x0
x1
=
SNoCut
(
binunion
{
add_SNo
(
mul_SNo
(
ap
x3
0
)
x1
)
(
add_SNo
(
mul_SNo
x0
(
ap
x3
1
)
)
(
minus_SNo
(
mul_SNo
(
ap
x3
0
)
(
ap
x3
1
)
)
)
)
|x3 ∈
setprod
(
SNoL
x0
)
(
SNoL
x1
)
}
{
add_SNo
(
mul_SNo
(
ap
x3
0
)
x1
)
(
add_SNo
(
mul_SNo
x0
(
ap
x3
1
)
)
(
minus_SNo
(
mul_SNo
(
ap
x3
0
)
(
ap
x3
1
)
)
)
)
|x3 ∈
setprod
(
SNoR
x0
)
(
SNoR
x1
)
}
)
(
binunion
{
add_SNo
(
mul_SNo
(
ap
x3
0
)
x1
)
(
add_SNo
(
mul_SNo
x0
(
ap
x3
1
)
)
(
minus_SNo
(
mul_SNo
(
ap
x3
0
)
(
ap
x3
1
)
)
)
)
|x3 ∈
setprod
(
SNoL
x0
)
(
SNoR
x1
)
}
{
add_SNo
(
mul_SNo
(
ap
x3
0
)
x1
)
(
add_SNo
(
mul_SNo
x0
(
ap
x3
1
)
)
(
minus_SNo
(
mul_SNo
(
ap
x3
0
)
(
ap
x3
1
)
)
)
)
|x3 ∈
setprod
(
SNoR
x0
)
(
SNoL
x1
)
}
)
(proof)
Param
explicit_Reals
explicit_Reals
:
ι
→
ι
→
ι
→
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ι
) →
(
ι
→
ι
→
ο
) →
ο
Definition
Eps_i_realset
:=
prim0
(
λ x0 .
and
(
∀ x1 .
x1
∈
x0
⟶
SNo
x1
)
(
explicit_Reals
x0
0
1
add_SNo
mul_SNo
SNoLe
)
)
previous assets