Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → (ι → ο) → ο be given.
Assume H0: x0 5e331.. 07017...
Assume H1: ∀ x1 x2 . ∀ x3 x4 : ι → ο . 858ff.. x1 x3 ⟶ x0 x1 x3 ⟶ 858ff.. x2 x4 ⟶ x0 x2 x4 ⟶ x0 (a3eb9.. x1 x2) (c0709.. x3 x4).
Assume H2: ∀ x1 x2 . ∀ x3 x4 : ι → ο . 858ff.. x1 x3 ⟶ x0 x1 x3 ⟶ 858ff.. x2 x4 ⟶ x0 x2 x4 ⟶ x0 (bf68c.. x1 x2) (6e020.. x3 x4).
Let x1 of type ι be given.
Let x2 of type ι → ο be given.
Assume H3: 858ff.. x1 x2.
Claim L4: ...
...
Claim L5: ∀ x3 . ∀ x4 : ι → ο . ... ⟶ ... ⟶ (λ x5 . λ x6 : ι → ο . and (858ff.. x5 x6) (x0 x5 x6)) ... ...
...
Claim L6: (λ x3 . λ x4 : ι → ο . and (858ff.. x3 x4) (x0 x3 x4)) x1 x2
Apply H3 with λ x3 . λ x4 : ι → ο . and (858ff.. x3 x4) (x0 x3 x4) leaving 3 subgoals.
Apply L5 with 5e331.., 07017.. leaving 2 subgoals.
The subproof is completed by applying unknownprop_fecdd5feecd0903be897193dc6d5c928cc89dee8ad0003c049becc2b40bb6fd9.
The subproof is completed by applying H0.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι → ο be given.
Let x6 of type ι → ο be given.
Apply L4 with x3, x5, (λ x7 . λ x8 : ι → ο . and (858ff.. x7 x8) (x0 x7 x8)) x4 x6 ⟶ (λ x7 . λ x8 : ι → ο . and (858ff.. x7 x8) (x0 x7 x8)) (a3eb9.. x3 x4) (c0709.. x5 x6).
Assume H6: 858ff.. x3 x5.
Assume H7: x0 x3 x5.
Apply L4 with x4, x6, (λ x7 . λ x8 : ι → ο . and (858ff.. x7 x8) (x0 x7 x8)) (a3eb9.. x3 x4) (c0709.. x5 x6).
Assume H8: 858ff.. x4 x6.
Assume H9: x0 x4 x6.
Apply L5 with a3eb9.. x3 x4, c0709.. x5 x6 leaving 2 subgoals.
Apply unknownprop_5eb4ddfb74eefcd5c762267d7191316fb0217c9ec50cc348a69d4e78ed1a8f5b with x3, x4, x5, x6 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H8.
Apply H1 with x3, x4, x5, x6 leaving 4 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι → ο be given.
Let x6 of type ι → ο be given.
Apply L4 with x3, x5, (λ x7 . λ x8 : ι → ο . and (858ff.. x7 x8) (x0 x7 x8)) x4 x6 ⟶ (λ x7 . λ x8 : ι → ο . and (858ff.. x7 x8) (x0 x7 x8)) (bf68c.. x3 x4) (6e020.. x5 x6).
Assume H6: 858ff.. x3 x5.
Assume H7: x0 x3 x5.
Apply L4 with x4, x6, (λ x7 . λ x8 : ι → ο . and (858ff.. x7 x8) (x0 x7 x8)) (bf68c.. x3 x4) (6e020.. x5 x6).
Assume H8: 858ff.. x4 x6.
Assume H9: x0 x4 x6.
Apply L5 with bf68c.. x3 x4, 6e020.. x5 x6 leaving 2 subgoals.
Apply unknownprop_d89e2d7f5df186af50ca21937230a175df55e9443d213018553bd36068f2a56f with x3, x4, x5, x6 leaving 2 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H8.
Apply H2 with x3, x4, x5, x6 leaving 4 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
Apply L6 with x0 x1 x2.
Assume H7: 858ff.. x1 x2.
Assume H8: x0 x1 x2.
The subproof is completed by applying H8.
■