Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ο be given.
Assume H0: x0 0.
Assume H1: ∀ x1 . x1 ∈ omega ⟶ x0 x1 ⟶ x0 (ordsucc x1).
Claim L2: ∀ x1 . nat_p x1 ⟶ x0 x1
Apply nat_ind with λ x1 . x0 x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Assume H2: nat_p x1.
Assume H3: x0 x1.
Apply H1 with x1 leaving 2 subgoals.
Apply nat_p_omega with x1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Let x1 of type ι be given.
Assume H3: x1 ∈ omega.
Apply L2 with x1.
Apply omega_nat_p with x1.
The subproof is completed by applying H3.
■