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.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι be given.
Assume H0: 80242.. x0.
Assume H1: 80242.. x1.
Assume H2: 80242.. x2.
Assume H3: 80242.. x3.
Assume H4: 80242.. x4.
Assume H5: 80242.. x5.
Assume H6: 099f3.. (bc82c.. x0 x4) (bc82c.. x2 x5).
Assume H7: 099f3.. (bc82c.. x1 x5) (bc82c.. x3 x4).
Apply unknownprop_36f11cc7571fa2487251d5a7c42936b64e63f594759a4c4f588173d9cd2aec53 with bc82c.. x0 x1, bc82c.. x4 x5, bc82c.. x2 x3 leaving 4 subgoals.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with x4, x5 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with x2, x3 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply unknownprop_30c79c0e02402151cd3152635d98c753ad546bc3a622bfa516c8603d0e4e28fb with x0, x1, x4, x5, λ x6 x7 . 099f3.. x7 (bc82c.. (bc82c.. x2 x3) (bc82c.. 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 H4.
The subproof is completed by applying H5.
Claim L8: bc82c.. (bc82c.. x2 x3) (bc82c.. x4 x5) = bc82c.. (bc82c.. x2 x5) (bc82c.. x3 x4)
Apply unknownprop_d8f468fc749efab866c779febbe4cd601b5e2eeaa90e3f207f17de20f4ab68ab with x2, x3, bc82c.. x4 x5, λ x6 x7 . x6 = bc82c.. (bc82c.. x2 x5) (bc82c.. x3 x4) leaving 4 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with x4, x5 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Apply unknownprop_d8f468fc749efab866c779febbe4cd601b5e2eeaa90e3f207f17de20f4ab68ab with x2, x5, bc82c.. x3 x4, λ x6 x7 . bc82c.. x2 (bc82c.. x3 (bc82c.. x4 x5)) = x6 leaving 4 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H5.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with x3, x4 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
set y6 to be bc82c.. x2 (bc82c.. x3 (bc82c.. x4 x5))
set y7 to be bc82c.. x3 (bc82c.. y6 (bc82c.. x4 x5))
Claim L8: ∀ x8 : ι → ο . x8 y7x8 y6
Let x8 of type ιο be given.
Assume H8: x8 (bc82c.. x4 (bc82c.. y7 (bc82c.. x5 y6))).
set y9 to be λ x9 . x8
Apply unknownprop_4e34a620b1f5496f1d776caaa0190761feb7cd3a7f3cd78c34f9288c12df6d94 with x5, y6, y7, λ x10 x11 . y9 (bc82c.. x4 x10) (bc82c.. x4 x11) leaving 4 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H8.
Let x8 of type ιιο be given.
Apply L8 with λ x9 . x8 x9 y7x8 y7 x9.
Assume H9: x8 y7 y7.
The subproof is completed by applying H9.
Apply L8 with λ x6 x7 . 099f3.. (bc82c.. (bc82c.. x0 x4) (bc82c.. x1 x5)) x7.
Apply unknownprop_05217a7ee3979c752afdb6976b4b09416f9f3c51faced83e1d8281aef2596f24 with bc82c.. x0 x4, bc82c.. x1 x5, bc82c.. x2 x5, bc82c.. x3 x4 leaving 6 subgoals.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with x0, x4 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with x1, x5 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H5.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with x2, x5 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H5.
Apply unknownprop_299d30a485627b811b1bc1069c06f437dd2ea8a2672044e2fbff59d7e1d539c2 with x3, x4 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H6.
The subproof is completed by applying H7.