Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: SNo_ omega x0.
Let x1 of type ι be given.
Assume H1: x1 ∈ SNoS_ omega.
Assume H2: ∀ x2 . x2 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x1 (minus_SNo x0))) (eps_ x2).
Apply SNoS_E2 with omega, x1, or (and (nIn (SNoLev x1) x0) (∀ x2 . x2 ∈ omega ⟶ SNoLev x1 ∈ x2 ⟶ x2 ∈ x0)) (and (SNoLev x1 ∈ x0) (∀ x2 . x2 ∈ omega ⟶ SNoLev x1 ∈ x2 ⟶ nIn x2 x0)) leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H1.
Assume H3: SNoLev x1 ∈ omega.
Assume H4: ordinal (SNoLev x1).
Assume H5: SNo x1.
Assume H6: SNo_ (SNoLev x1) x1.
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Claim L12: ...
...
Claim L13: ...
...
Claim L14: ...
...
Claim L15: ...
...
Claim L16: ...
...
Claim L17: ...
...
Claim L18: ...
...
Claim L19: ...
...
Claim L20: ...
...
Claim L21: ...
...
Claim L22: ...
...
Apply xm with SNoLev x1 ∈ x0, or (and (nIn (SNoLev x1) x0) (∀ x2 . x2 ∈ omega ⟶ SNoLev x1 ∈ x2 ⟶ x2 ∈ x0)) (and (SNoLev x1 ∈ x0) (∀ x2 . x2 ∈ omega ⟶ SNoLev x1 ∈ x2 ⟶ nIn x2 x0)) leaving 2 subgoals.
Assume H23: SNoLev x1 ∈ x0.
Apply orIR with and (nIn (SNoLev x1) x0) (∀ x2 . x2 ∈ omega ⟶ SNoLev x1 ∈ x2 ⟶ x2 ∈ x0), and (SNoLev x1 ∈ x0) (∀ x2 . x2 ∈ omega ⟶ SNoLev x1 ∈ x2 ⟶ nIn x2 x0).
Apply andI with SNoLev x1 ∈ x0, ∀ x2 . x2 ∈ omega ⟶ SNoLev x1 ∈ x2 ⟶ nIn x2 x0 leaving 2 subgoals.
The subproof is completed by applying H23.
Let x2 of type ι be given.
Assume H24: x2 ∈ omega.
Assume H25: SNoLev x1 ∈ x2.
Assume H26: x2 ∈ x0.
Claim L27: ...
...
Apply SNoS_E2 with omega, binintersect x0 (SNoElts_ x2), False leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying L27.
Assume H28: SNoLev (binintersect x0 (SNoElts_ x2)) ∈ omega.
Assume H29: ordinal (SNoLev (binintersect x0 (SNoElts_ x2))).
Assume H30: SNo (binintersect x0 (SNoElts_ x2)).
Assume H31: SNo_ (SNoLev (binintersect x0 (SNoElts_ x2))) (binintersect x0 (SNoElts_ x2)).
Claim L32: ...
...
Apply SNoS_E2 with omega, add_SNo (binintersect x0 (SNoElts_ x2)) (minus_SNo x1), False leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying L32.
Assume H33: SNoLev (add_SNo (binintersect x0 (SNoElts_ x2)) (minus_SNo x1)) ∈ omega.
Assume H34: ordinal (SNoLev (add_SNo (binintersect x0 (SNoElts_ x2)) (minus_SNo x1))).
Assume H35: SNo (add_SNo (binintersect x0 (SNoElts_ x2)) (minus_SNo x1)).
Assume H36: SNo_ (SNoLev (add_SNo (binintersect x0 (SNoElts_ x2)) (minus_SNo x1))) (add_SNo (binintersect x0 (SNoElts_ x2)) (minus_SNo x1)).
Claim L37: ...
...
Apply L16 with x2, False leaving 3 subgoals.
The subproof is completed by applying H24.
The subproof is completed by applying L37.
Let x3 of type ι be given.
Assume H38: (λ x4 . and ... ...) ....
...
...
■