Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ordinal x0.
Let x1 of type ι → ο be given.
Apply PNo_bd_pred with PNoCutL x0 x1, PNoCutR x0 x1, x0, PNo_bd (PNoCutL x0 x1) (PNoCutR x0 x1) = x0 leaving 5 subgoals.
Apply PNoCut_pwise with x0, x1.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
The subproof is completed by applying PNoCutL_lenbdd with x0, x1.
The subproof is completed by applying PNoCutR_lenbdd with x0, x1.
Assume H1: and (ordinal (PNo_bd (PNoCutL x0 x1) (PNoCutR x0 x1))) (PNo_strict_imv (PNoCutL x0 x1) (PNoCutR x0 x1) (PNo_bd (PNoCutL x0 x1) (PNoCutR x0 x1)) (PNo_pred (PNoCutL x0 x1) (PNoCutR x0 x1))).
Apply H1 with (∀ x2 . x2 ∈ PNo_bd (PNoCutL x0 x1) (PNoCutR x0 x1) ⟶ ∀ x3 : ι → ο . not (PNo_strict_imv (PNoCutL x0 x1) (PNoCutR x0 x1) x2 x3)) ⟶ PNo_bd (PNoCutL x0 x1) (PNoCutR x0 x1) = x0.
Assume H2: ordinal (PNo_bd (PNoCutL x0 x1) (PNoCutR x0 x1)).
Assume H3: PNo_strict_imv (PNoCutL x0 x1) (PNoCutR x0 x1) (PNo_bd (PNoCutL x0 x1) (PNoCutR x0 x1)) (PNo_pred (PNoCutL x0 x1) (PNoCutR x0 x1)).
Assume H4: ∀ x2 . x2 ∈ PNo_bd (PNoCutL x0 x1) (PNoCutR x0 x1) ⟶ ∀ x3 : ι → ο . not (PNo_strict_imv (PNoCutL x0 x1) (PNoCutR x0 x1) x2 x3).
Apply H3 with PNo_bd (PNoCutL x0 x1) (PNoCutR x0 x1) = x0.
Assume H5: PNo_strict_upperbd (PNoCutL x0 x1) (PNo_bd (PNoCutL x0 x1) (PNoCutR x0 x1)) (PNo_pred (PNoCutL x0 x1) (PNoCutR x0 x1)).
Assume H6: PNo_strict_lowerbd (PNoCutR x0 x1) (PNo_bd (PNoCutL x0 x1) (PNoCutR x0 x1)) (PNo_pred (PNoCutL x0 x1) (PNoCutR x0 x1)).
Apply ordinal_trichotomy_or with PNo_bd (PNoCutL x0 x1) (PNoCutR x0 x1), x0, PNo_bd (PNoCutL x0 x1) (PNoCutR x0 x1) = x0 leaving 4 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H0.
Assume H7: or (PNo_bd (PNoCutL x0 x1) (PNoCutR x0 x1) ∈ x0) (PNo_bd (PNoCutL x0 x1) (PNoCutR x0 x1) = x0).
Apply H7 with PNo_bd (PNoCutL x0 x1) (PNoCutR x0 x1) = x0 leaving 2 subgoals.
Assume H8: PNo_bd (PNoCutL x0 x1) (PNoCutR x0 x1) ∈ x0.
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Apply PNoLt_trichotomy_or with PNo_bd (PNoCutL x0 x1) (PNoCutR x0 x1), x0, PNo_pred (PNoCutL x0 x1) (PNoCutR x0 x1), x1, PNo_bd (PNoCutL x0 x1) ... = ... leaving 4 subgoals.
...
...
...
...
...
...
■