Search for blocks/addresses/...

Proofgold Proof

pf
Apply unknownprop_aca6546ca70975227cfdd401f01c6af1ee4084a6127606b8f15131e520646158 with λ x0 x1 x2 . ∀ x3 x4 : ι → ο . 858ff.. x1 x3858ff.. x2 x4∀ x5 x6 . x3 x5d7d78.. x0 x5 x6x4 x6 leaving 9 subgoals.
Let x0 of type ι be given.
Assume H0: 74e69.. x0.
Let x1 of type ιο be given.
Let x2 of type ιο be given.
Assume H1: 858ff.. x0 x1.
Assume H2: 858ff.. x0 x2.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H3: x1 x3.
Assume H4: d7d78.. c4def.. x3 x4.
Claim L5: x1 = x2
Apply unknownprop_117be7573c60b7d0abaafc299d87847fec12e93691ef0a29fced62dc7418d130 with x0, x1, x2 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Claim L6: x3 = x4
Apply unknownprop_ae1e79e1a2bccfe8aebcb1e813103c4afd5b26690657ff2ca9061fbf87b7bf35 with x3, x4.
The subproof is completed by applying H4.
Apply L5 with λ x5 x6 : ι → ο . x5 x4.
Apply L6 with λ x5 x6 . x1 x5.
The subproof is completed by applying H3.
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 H0: 762f0.. x3 x0 x1.
Assume H1: ∀ x5 x6 : ι → ο . 858ff.. x0 x5858ff.. x1 x6∀ x7 x8 . x5 x7d7d78.. x3 x7 x8x6 x8.
Assume H2: 762f0.. x4 x1 x2.
Assume H3: ∀ x5 x6 : ι → ο . 858ff.. x1 x5858ff.. x2 x6∀ x7 x8 . x5 x7d7d78.. x4 x7 x8x6 x8.
Let x5 of type ιο be given.
Let x6 of type ιο be given.
Assume H4: 858ff.. x0 x5.
Assume H5: 858ff.. x2 x6.
Let x7 of type ι be given.
Let x8 of type ι be given.
Assume H6: x5 x7.
Assume H7: d7d78.. (6b90c.. x3 x4) x7 x8.
Claim L8: ∃ x9 . and (d7d78.. x3 x7 x9) (d7d78.. x4 x9 x8)
Apply unknownprop_cff582124c579af9c23894076366d9c1d4be330d88106ca325a9ffd28cc0a5c6 with x3, x4, x7, x8.
The subproof is completed by applying H7.
Apply L8 with x6 x8.
Let x9 of type ι be given.
Assume H9: (λ x10 . and (d7d78.. x3 x7 x10) (d7d78.. x4 x10 x8)) x9.
Apply H9 with x6 x8.
Assume H10: d7d78.. x3 x7 x9.
Assume H11: d7d78.. x4 x9 x8.
Apply unknownprop_ba62a7b985827e5b6d2adfd88e1946699da89cb2c580e048e15cbf1151f093ec with x3, x0, x1, x6 x8 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H12: and (e05e6.. x3) (74e69.. x0).
Assume H13: 74e69.. x1.
Claim L14: ∃ x10 : ι → ο . 858ff.. x1 x10
Apply unknownprop_7bb51105313454d4aa8c466e57e3cafc9a19eebc0a8b69682b3e7f6ddfb8275a with x1.
The subproof is completed by applying H13.
Apply L14 with x6 x8.
Let x10 of type ιο be given.
Assume H15: 858ff.. x1 x10.
Claim L16: x10 x9
Apply H1 with x5, x10, x7, x9 leaving 4 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H15.
The subproof is completed by applying H6.
The subproof is completed by applying H10.
Apply H3 with x10, x6, x9, x8 leaving 4 subgoals.
The subproof is completed by applying H15.
The subproof is completed by applying H5.
The subproof is completed by applying L16.
The subproof is completed by applying H11.
Let x0 of type ι be given.
Assume H0: 74e69.. x0.
Let x1 of type ιο be given.
Let x2 of type ιο be given.
Assume H1: 858ff.. x0 x1.
Assume H2: 858ff.. 5e331.. x2.
Let x3 of type ι be given.
Let x4 of type ι be given.
Assume H3: x1 x3.
Assume H4: d7d78.. c9248.. x3 x4.
Claim L5: x2 = 07017..
Apply unknownprop_117be7573c60b7d0abaafc299d87847fec12e93691ef0a29fced62dc7418d130 with 5e331.., x2, 07017.. leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying unknownprop_fecdd5feecd0903be897193dc6d5c928cc89dee8ad0003c049becc2b40bb6fd9.
Apply L5 with λ x5 x6 : ι → ο . x6 x4.
Apply unknownprop_11ab5ad84446dc0c8599e250d04348a580b4e461b777edde7bd671068dfc2d3a with x3, x4.
The subproof is completed by applying H4.
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Assume H0: 74e69.. x2.
...
...
...
...
...
...