Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: ordinal x0.
Assume H1: ordinal x1.
Let x2 of type ιο be given.
Let x3 of type ιο be given.
Let x4 of type ιο be given.
Assume H2: PNoEq_ x0 x2 x3.
Assume H3: or (PNoLt x0 x3 x1 x4) (and (x0 = x1) (PNoEq_ x0 x3 x4)).
Apply H3 with or (PNoLt x0 x2 x1 x4) (and (x0 = x1) (PNoEq_ x0 x2 x4)) leaving 2 subgoals.
Assume H4: PNoLt x0 x3 x1 x4.
Apply orIL with PNoLt x0 x2 x1 x4, and (x0 = x1) (PNoEq_ x0 x2 x4).
Apply PNoEqLt_tra with x0, x1, x2, x3, x4 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
Assume H4: and (x0 = x1) (PNoEq_ x0 x3 x4).
Apply H4 with or (PNoLt x0 x2 x1 x4) (and (x0 = x1) (PNoEq_ x0 x2 x4)).
Assume H5: x0 = x1.
Assume H6: PNoEq_ x0 x3 x4.
Apply orIR with PNoLt x0 x2 x1 x4, and (x0 = x1) (PNoEq_ x0 x2 x4).
Apply andI with x0 = x1, PNoEq_ x0 x2 x4 leaving 2 subgoals.
The subproof is completed by applying H5.
Apply PNoEq_tra_ with x0, x2, x3, x4 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H6.