Search for blocks/addresses/...
Proofgold Proof
pf
Assume H0:
∀ x0 x1 .
SNoLev
x0
∈
omega
⟶
SNo
x0
⟶
SNo
x1
⟶
ordinal
(
SNoLev
(
add_SNo
x0
x1
)
)
⟶
SNoLev
(
add_SNo
x0
x1
)
∈
omega
.
Claim L1:
SNoLev
0
∈
omega
Apply SNoLev_0 with
λ x0 x1 .
x1
∈
omega
.
Apply nat_p_omega with
0
.
The subproof is completed by applying nat_0.
Claim L2:
SNo
0
The subproof is completed by applying SNo_0.
Claim L3:
SNo
omega
The subproof is completed by applying SNo_omega.
Claim L4:
not
(
ordinal
(
SNoLev
(
add_SNo
0
omega
)
)
⟶
SNoLev
(
add_SNo
0
omega
)
∈
omega
)
Apply add_SNo_0L with
omega
,
λ x0 x1 .
not
(
ordinal
(
SNoLev
x1
)
⟶
SNoLev
x1
∈
omega
)
leaving 2 subgoals.
The subproof is completed by applying L3.
Apply ordinal_SNoLev with
omega
,
λ x0 x1 .
not
(
ordinal
x1
⟶
x1
∈
omega
)
leaving 2 subgoals.
The subproof is completed by applying omega_ordinal.
Assume H4:
ordinal
omega
⟶
omega
∈
omega
.
Apply In_irref with
omega
.
Apply H4.
The subproof is completed by applying omega_ordinal.
Apply L4.
Apply H0 with
0
,
omega
leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
■