Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ι → ι → ο be given.
Assume H0: ∀ x1 . d7d78.. c4def.. x1 x1 ⟶ x0 c4def.. x1 x1.
Assume H1: ∀ x1 x2 x3 x4 x5 . d7d78.. x1 x3 x4 ⟶ x0 x1 x3 x4 ⟶ d7d78.. x2 x4 x5 ⟶ x0 x2 x4 x5 ⟶ x0 (6b90c.. x1 x2) x3 x5.
Assume H2: ∀ x1 . d7d78.. c9248.. x1 236c6.. ⟶ x0 c9248.. x1 236c6...
Assume H3: ∀ x1 x2 x3 . d7d78.. x1 x2 x3 ⟶ x0 x1 x2 x3 ⟶ x0 (a6e19.. x1) x2 (0b8ef.. x3).
Assume H4: ∀ x1 x2 x3 . d7d78.. x1 x2 x3 ⟶ x0 x1 x2 x3 ⟶ x0 (2fe34.. x1) x2 (6c5f4.. x3).
Assume H5: ∀ x1 x2 x3 x4 x5 . e05e6.. x2 ⟶ d7d78.. x1 (cfc98.. x3 x4) x5 ⟶ x0 x1 (cfc98.. x3 x4) x5 ⟶ x0 (3e00e.. x1 x2) (cfc98.. (0b8ef.. x3) x4) x5.
Assume H6: ∀ x1 x2 x3 x4 x5 . e05e6.. x1 ⟶ d7d78.. x2 (cfc98.. x3 x4) x5 ⟶ x0 x2 (cfc98.. x3 x4) x5 ⟶ x0 (3e00e.. x1 x2) (cfc98.. (6c5f4.. x3) x4) x5.
Assume H7: ∀ x1 x2 x3 x4 x5 . d7d78.. x1 x3 x4 ⟶ x0 x1 x3 x4 ⟶ d7d78.. x2 x3 x5 ⟶ x0 x2 x3 x5 ⟶ x0 (f9341.. x1 x2) x3 (cfc98.. x4 x5).
Assume H8: ∀ x1 x2 x3 x4 . d7d78.. x1 x2 x4 ⟶ x0 x1 x2 x4 ⟶ x0 (1fa6d.. x1) (cfc98.. x2 x3) x4.
Assume H9: ∀ x1 x2 x3 x4 . d7d78.. x1 x3 x4 ⟶ x0 x1 x3 x4 ⟶ x0 (3a365.. x1) (cfc98.. x2 x3) x4.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Assume H10: d7d78.. x1 x2 x3.
Claim L11: ...
...
Claim L12: ...
...
Claim L13: and (d7d78.. x1 x2 x3) (x0 x1 x2 x3)
Apply H10 with λ x4 x5 x6 . and (d7d78.. x4 x5 x6) (x0 x4 x5 x6) leaving 10 subgoals.
Let x4 of type ι be given.
Apply L12 with c4def.., x4, x4 leaving 2 subgoals.
The subproof is completed by applying unknownprop_7952446787e7ec87974d8b0564aec0660f9849ef8699aeee5e2d5d268814fd9d with x4.
Apply H0 with x4.
The subproof is completed by applying unknownprop_7952446787e7ec87974d8b0564aec0660f9849ef8699aeee5e2d5d268814fd9d with x4.
Let x4 of type ι be given.
Let x5 of type ι be given.
Let x6 of type ι be given.
Let x7 of type ι be given.
Let x8 of type ι be given.
Apply L11 with x4, x6, x7, (λ x9 x10 x11 . and (d7d78.. x9 ... ...) ...) ... ... ... ⟶ (λ x9 x10 x11 . and (d7d78.. x9 x10 x11) (x0 x9 x10 x11)) (6b90c.. x4 x5) x6 x8.
...
...
...
...
...
...
...
...
...
Apply L13 with x0 x1 x2 x3.
Assume H14: d7d78.. x1 x2 x3.
Assume H15: x0 x1 x2 x3.
The subproof is completed by applying H15.
■