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: or (40dde.. x0 x2 x1 x3) (and (x0 = x1) (PNoEq_ x0 x2 x3)).
Assume H3: PNoEq_ x1 x3 x4.
Apply H2 with or (40dde.. x0 x2 x1 x4) (and (x0 = x1) (PNoEq_ x0 x2 x4)) leaving 2 subgoals.
Assume H4: 40dde.. x0 x2 x1 x3.
Apply orIL with 40dde.. x0 x2 x1 x4, and (x0 = x1) (PNoEq_ x0 x2 x4).
Apply unknownprop_8400f668ce579075dd52a6b0bc8eaa2c816f68129d64497b65439b55d60266f7 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 H4.
The subproof is completed by applying H3.
Assume H4: and (x0 = x1) (PNoEq_ x0 x2 x3).
Apply H4 with or (40dde.. x0 x2 x1 x4) (and (x0 = x1) (PNoEq_ x0 x2 x4)).
Assume H5: x0 = x1.
Assume H6: PNoEq_ x0 x2 x3.
Apply orIR with 40dde.. 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 H6.
Apply H5 with λ x5 x6 . PNoEq_ x6 x3 x4.
The subproof is completed by applying H3.