Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: ordinal x0.
Let x1 of type ι → ο be given.
Let x2 of type ι → ο be given.
Let x3 of type ι → ο be given.
Assume H1: PNoLt_ x0 x1 x2.
Assume H2: PNoLt_ x0 x2 x3.
Apply unknownprop_d3eaeaf2c92929364f7d313ca2b01dbaa8e7169d84112bc61a6ed9c6cb0d624a with λ x4 x5 : ι → (ι → ο) → (ι → ο) → ο . x5 x0 x1 x3.
Apply unknownprop_ff2db5d7cd089ead6d3f23ab1904a643f023d611ddbe42c5c85e87e080e26158 with x0, x1, x2, ∃ x4 . and (In x4 x0) (and (and (PNoEq_ x4 x1 x3) (not (x1 x4))) (x3 x4)) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x4 of type ι be given.
Assume H3: In x4 x0.
Assume H4: PNoEq_ x4 x1 x2.
Assume H5: not (x1 x4).
Assume H6: x2 x4.
Apply unknownprop_ff2db5d7cd089ead6d3f23ab1904a643f023d611ddbe42c5c85e87e080e26158 with x0, x2, x3, ∃ x5 . and (In x5 x0) (and (and (PNoEq_ x5 x1 x3) (not (x1 x5))) (x3 x5)) leaving 2 subgoals.
The subproof is completed by applying H2.
Let x5 of type ι be given.
Assume H7: In x5 x0.
Assume H8: PNoEq_ x5 x2 x3.
Assume H9: not (x2 x5).
Assume H10: x3 x5.
Claim L11: ...
...
Claim L12: ...
...
Claim L13: ...
...
Claim L14: ...
...
Apply unknownprop_497ef0b809178e9ac674acf0f41f994a7e76b824de0430efd934f6540a71daab with x4, x5, ∃ x6 . and (In x6 x0) (and (and (PNoEq_ x6 x1 x3) (not (x1 x6))) (x3 x6)) leaving 5 subgoals.
The subproof is completed by applying L11.
The subproof is completed by applying L12.
Assume H15: In x4 x5.
Let x6 of type ο be given.
Assume H16: ∀ x7 . and (In x7 x0) (and (and (PNoEq_ x7 x1 x3) (not (x1 x7))) (x3 x7)) ⟶ x6.
Apply H16 with x4.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with In x4 x0, and (and (PNoEq_ x4 x1 x3) (not (x1 x4))) (x3 x4) leaving 2 subgoals.
The subproof is completed by applying H3.
Apply unknownprop_c7bf67064987d41cefc55afb6af6ecbbb6b830405f2005e0def6e504b3ca3bf3 with PNoEq_ x4 x1 x3, not (x1 x4), x3 x4 leaving 3 subgoals.
Apply unknownprop_e0f34743af27a604447ff8f709ee0ab4cfc998bf21a330579a3abf15b483f3e6 with x4, x1, x2, x3 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply unknownprop_385a349774bd141f67c9640b600008e8534ed0c05d891557fd37870b1d687d7f with x2, x3, x5, x4 leaving 3 subgoals.
The subproof is completed by applying L12.
The subproof is completed by applying H15.
The subproof is completed by applying H8.
The subproof is completed by applying H5.
Apply unknownprop_d4c6f9663742385071dd283da85a9397dc2dfd0eede50c9fd289b7b23ca97cdd with x2 x4, x3 x4 leaving 2 subgoals.
Apply L14 with x4.
The subproof is completed by applying H15.
The subproof is completed by applying H6.
Assume H15: x4 = x5.
Let x6 of type ο be given.
Assume H16: ∀ x7 . and (In x7 x0) (and (and (PNoEq_ x7 x1 x3) (not (x1 x7))) (x3 x7)) ⟶ x6.
Apply H16 with x4.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with In x4 x0, and (and (PNoEq_ x4 x1 x3) (not (x1 x4))) (x3 x4) leaving 2 subgoals.
The subproof is completed by applying H3.
Apply unknownprop_c7bf67064987d41cefc55afb6af6ecbbb6b830405f2005e0def6e504b3ca3bf3 with PNoEq_ x4 x1 x3, not (x1 x4), x3 x4 leaving 3 subgoals.
Apply unknownprop_e0f34743af27a604447ff8f709ee0ab4cfc998bf21a330579a3abf15b483f3e6 with x4, x1, x2, x3 leaving 2 subgoals.
The subproof is completed by applying H4.
Apply H15 with λ x7 x8 . PNoEq_ x8 x2 x3.
The subproof is completed by applying H8.
The subproof is completed by applying H5.
Apply H15 with λ x7 x8 . x3 x8.
The subproof is completed by applying H10.
Assume H15: In x5 x4.
Let x6 of type ο be given.
Assume H16: ∀ x7 . and (In x7 x0) (and (and (PNoEq_ x7 x1 x3) (not (x1 x7))) (x3 x7)) ⟶ x6.
Apply H16 with x5.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with In x5 x0, and (and (PNoEq_ x5 x1 x3) ...) ... leaving 2 subgoals.
...
...
■