Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: ordinal x0.
Assume H1: ordinal x1.
Assume H2: ordinal x2.
Let x3 of type ι → ο be given.
Let x4 of type ι → ο be given.
Let x5 of type ι → ο be given.
Assume H3: or (40dde.. x0 x3 x1 x4) (and (x0 = x1) (PNoEq_ x0 x3 x4)).
Assume H4: 35b9b.. x1 x4 x2 x5.
Apply H3 with 35b9b.. x0 x3 x2 x5 leaving 2 subgoals.
Assume H5: 40dde.. x0 x3 x1 x4.
Apply orIL with 40dde.. x0 x3 x2 x5, and (x0 = x2) (PNoEq_ x0 x3 x5).
Apply unknownprop_f27aa4f44dd3356cd94acc385318a128a0f6600b661fa984e48e2fd277a08f76 with x0, x1, x2, x3, x4, x5 leaving 5 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 H5.
The subproof is completed by applying H4.
Assume H5: and (x0 = x1) (PNoEq_ x0 x3 x4).
Apply H5 with 35b9b.. x0 x3 x2 x5.
Assume H6: x0 = x1.
Assume H7: PNoEq_ x0 x3 x4.
Apply H6 with λ x6 x7 . 35b9b.. x7 x3 x2 x5.
Claim L8: PNoEq_ x1 x3 x4
Apply H6 with λ x6 x7 . PNoEq_ x6 x3 x4.
The subproof is completed by applying H7.
Apply unknownprop_d81166a516850c398272ee6d885342023555ef2970270537509bbcd7d13c1cf9 with x1, x2, x3, x4, x5 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying L8.
The subproof is completed by applying H4.
■