Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ο be given.
Let x1 of type ι → ο be given.
Apply ordinal_ind with λ x2 . or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0).
Let x2 of type ι be given.
Assume H0: ordinal x2.
Assume H1: ∀ x3 . prim1 x3 x2 ⟶ or (or (PNoLt_ x3 x0 x1) (PNoEq_ x3 x0 x1)) (PNoLt_ x3 x1 x0).
Apply xm with PNoEq_ x2 x0 x1, or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0) leaving 2 subgoals.
Assume H2: PNoEq_ x2 x0 x1.
Apply orIL with or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1), PNoLt_ x2 x1 x0.
Apply orIR with PNoLt_ x2 x0 x1, PNoEq_ x2 x0 x1.
The subproof is completed by applying H2.
Assume H2: not (PNoEq_ x2 x0 x1).
Claim L3: ...
...
Apply L3 with or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0).
Let x3 of type ι be given.
Assume H4: not (prim1 x3 x2 ⟶ iff (x0 x3) (x1 x3)).
Claim L5: ...
...
Apply L5 with or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0).
Assume H6: prim1 x3 x2.
Assume H7: not (iff (x0 x3) (x1 x3)).
Apply H1 with x3, or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0) leaving 3 subgoals.
The subproof is completed by applying H6.
Assume H8: or (PNoLt_ x3 x0 x1) (PNoEq_ x3 x0 x1).
Apply H8 with or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0) leaving 2 subgoals.
Assume H9: PNoLt_ x3 x0 x1.
Apply orIL with or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1), PNoLt_ x2 x1 x0.
Apply orIL with PNoLt_ x2 x0 x1, PNoEq_ x2 x0 x1.
Apply PNoLt_mon_ with x0, x1, x2, x3 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H6.
The subproof is completed by applying H9.
Assume H9: PNoEq_ x3 x0 x1.
Apply xm with x0 x3, or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0) leaving 2 subgoals.
Assume H10: x0 x3.
Apply xm with x1 x3, or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 x0 x1)) (PNoLt_ x2 x1 x0) leaving 2 subgoals.
Assume H11: x1 x3.
Apply FalseE with or (or (PNoLt_ x2 x0 x1) (PNoEq_ x2 ... ...)) ....
...
...
...
...
■