| pf |
|---|
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ο be given.
Let x3 of type ι → ο be given.
Let x4 of type ι → ο be given.
Assume H3: PNoLt x0 x3 x1 x4. Claim L4: ∀ x5 . In x5 x0 ⟶ iff (x2 x5) (x3 x5)Apply unknownprop_ee0b4b64aba8e6af97035d72b359ab8e1ae1e5e06024c58477c9410cad648356 with λ x5 x6 : ι → (ι → ο) → (ι → ο) → ο . x5 x0 x2 x3.
The subproof is completed by applying H2.
Apply unknownprop_7d798c5794ed96c61cc9ec828963a5831eee43021e8f1ea48be05a5cb53904e0 with x0, x1, x3, x4, PNoLt x0 x2 x1 x4 leaving 4 subgoals.
The subproof is completed by applying H3.
Apply unknownprop_ff2db5d7cd089ead6d3f23ab1904a643f023d611ddbe42c5c85e87e080e26158 with binintersect x0 x1, x3, x4, PNoLt x0 x2 x1 x4 leaving 2 subgoals.
The subproof is completed by applying H5.
Let x5 of type ι be given.
Apply unknownprop_9f9c1680d203bdbb862d1bf6c2b8504d7e3a6fca72f77bd8968e86ad6ad69346 with x0, x1, x5, PNoEq_ x5 x3 x4 ⟶ not (x3 x5) ⟶ x4 x5 ⟶ PNoLt x0 x2 x1 x4 leaving 2 subgoals.
The subproof is completed by applying H6.
Assume H11: x4 x5.
Apply unknownprop_2a38d5561acb46bf4581f375c3fb301a06d08a93dee7d2c06138bdaa38452584 with x0, x1, x2, x4.
Apply unknownprop_d3eaeaf2c92929364f7d313ca2b01dbaa8e7169d84112bc61a6ed9c6cb0d624a with λ x6 x7 : ι → (ι → ο) → (ι → ο) → ο . x7 (binintersect x0 x1) x2 x4.
Let x6 of type ο be given.
Apply H12 with x5.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with In x5 (binintersect x0 x1), and (and (PNoEq_ x5 x2 x4) (not (x2 x5))) (x4 x5) leaving 2 subgoals.
The subproof is completed by applying H6.
Apply unknownprop_c7bf67064987d41cefc55afb6af6ecbbb6b830405f2005e0def6e504b3ca3bf3 with PNoEq_ x5 x2 x4, not (x2 x5), x4 x5 leaving 3 subgoals.
Apply unknownprop_e0f34743af27a604447ff8f709ee0ab4cfc998bf21a330579a3abf15b483f3e6 with x5, x2, x3, x4 leaving 2 subgoals.
Apply unknownprop_385a349774bd141f67c9640b600008e8534ed0c05d891557fd37870b1d687d7f with x2, x3, x0, x5 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H7.
The subproof is completed by applying H2.
The subproof is completed by applying H9.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with x2 x5.
Assume H13: x2 x5.
Apply notE with x3 x5 leaving 2 subgoals.
The subproof is completed by applying H10.
Apply unknownprop_d4c6f9663742385071dd283da85a9397dc2dfd0eede50c9fd289b7b23ca97cdd with x2 x5, x3 x5 leaving 2 subgoals.
Apply L4 with x5.
The subproof is completed by applying H7.
The subproof is completed by applying H13.
The subproof is completed by applying H11.
Assume H7: x4 x0.
Apply unknownprop_b3cbc8d84fae88a28c0902044988016197816c898f2ca1bfc7fbe4f41daf82f2 with x0, x1, x2, x4 leaving 3 subgoals.
The subproof is completed by applying H5.
Apply unknownprop_e0f34743af27a604447ff8f709ee0ab4cfc998bf21a330579a3abf15b483f3e6 with x0, x2, x3, x4 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
Apply unknownprop_16a890d80e582f5663abfcfb5f5942164bae0e65476988fa667ed9ca882547fe with x0, x1, x2, x4 leaving 3 subgoals.
The subproof is completed by applying H5.
Apply unknownprop_e0f34743af27a604447ff8f709ee0ab4cfc998bf21a330579a3abf15b483f3e6 with x1, x2, x3, x4 leaving 2 subgoals.
Apply unknownprop_385a349774bd141f67c9640b600008e8534ed0c05d891557fd37870b1d687d7f with x2, x3, x0, x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H5.
The subproof is completed by applying H2.
The subproof is completed by applying H6.
Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with x2 x1.
Assume H8: x2 x1.
Apply notE with x3 x1 leaving 2 subgoals.
The subproof is completed by applying H7.
Apply unknownprop_d4c6f9663742385071dd283da85a9397dc2dfd0eede50c9fd289b7b23ca97cdd with x2 x1, x3 x1 leaving 2 subgoals.
Apply L4 with x1.
The subproof is completed by applying H5.
The subproof is completed by applying H8.
■ |
|