Search for blocks/addresses/...

Proofgold Proof

pf
Apply unknownprop_e9ef755431cb760bbf47dc0630cd74e38be1fffa1f9d7eecd713121223b57312 with λ x0 x1 x2 . bc82c.. x0 (bc82c.. x1 x2) = bc82c.. (bc82c.. x0 x1) x2.
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: 80242.. x0.
Assume H1: 80242.. x1.
Assume H2: 80242.. x2.
Assume H3: ∀ x3 . prim1 x3 (56ded.. (e4431.. x0)) ⟶ (λ x4 x5 x6 . bc82c.. x4 (bc82c.. x5 x6) = bc82c.. (bc82c.. x4 x5) x6) x3 x1 x2.
Assume H4: ∀ x3 . prim1 x3 (56ded.. (e4431.. x1)) ⟶ (λ x4 x5 x6 . bc82c.. x4 (bc82c.. x5 x6) = bc82c.. (bc82c.. x4 x5) x6) x0 x3 x2.
Assume H5: ∀ x3 . prim1 x3 (56ded.. (e4431.. x2)) ⟶ (λ x4 x5 x6 . bc82c.. x4 (bc82c.. x5 x6) = bc82c.. (bc82c.. x4 x5) x6) x0 x1 x3.
Assume H6: ∀ x3 . prim1 x3 (56ded.. (e4431.. x0)) ⟶ ∀ x4 . prim1 x4 (56ded.. (e4431.. x1)) ⟶ (λ x5 x6 x7 . bc82c.. x5 (bc82c.. x6 x7) = bc82c.. (bc82c.. x5 x6) x7) x3 x4 x2.
Assume H7: ∀ x3 . prim1 x3 (56ded.. (e4431.. x0)) ⟶ ∀ x4 . prim1 x4 (56ded.. (e4431.. x2)) ⟶ (λ x5 x6 x7 . bc82c.. x5 (bc82c.. x6 x7) = bc82c.. (bc82c.. x5 x6) x7) x3 x1 x4.
Assume H8: ∀ x3 . prim1 x3 (56ded.. (e4431.. x1)) ⟶ ∀ x4 . prim1 x4 (56ded.. (e4431.. x2)) ⟶ (λ x5 x6 x7 . bc82c.. x5 (bc82c.. x6 x7) = bc82c.. (bc82c.. x5 x6) x7) x0 x3 x4.
Assume H9: ∀ x3 . prim1 x3 (56ded.. (e4431.. x0)) ⟶ ∀ x4 . prim1 x4 (56ded.. (e4431.. x1)) ⟶ ∀ x5 . prim1 x5 (56ded.. (e4431.. x2)) ⟶ (λ x6 x7 x8 . bc82c.. x6 (bc82c.. x7 x8) = bc82c.. (bc82c.. x6 x7) x8) x3 x4 x5.
Claim L10: ...
...
Claim L11: ...
...
Apply unknownprop_b2d3cb96a6a882d02e5e57dcfc02559b580d1f8621959f82afe70dc68a4b010f with x0, bc82c.. x1 x2, λ x3 x4 . x4 = bc82c.. (bc82c.. x0 x1) x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L11.
Apply unknownprop_b2d3cb96a6a882d02e5e57dcfc02559b580d1f8621959f82afe70dc68a4b010f with bc82c.. x0 x1, x2, λ x3 x4 . 02a50.. (0ac37.. (94f9e.. (23e07.. x0) (λ x5 . bc82c.. x5 (bc82c.. x1 x2))) (94f9e.. (23e07.. (bc82c.. x1 x2)) (bc82c.. x0))) (0ac37.. (94f9e.. (5246e.. x0) (λ x5 . bc82c.. x5 (bc82c.. x1 x2))) (94f9e.. (5246e.. (bc82c.. x1 x2)) (bc82c.. x0))) = x4 leaving 3 subgoals.
The subproof is completed by applying L10.
...
...
■