Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: ∀ x0 . ...∀ x1 . ...∀ x2 x3 : ι → ι → ι . ......(λ x4 x5 . λ x6 : ι → ι → ι . 02a50.. (0ac37.. (94f9e.. (ac767.. (23e07.. x4) (23e07.. x5)) (λ x7 . bc82c.. (x6 (f482f.. x7 4a7ef..) x5) (bc82c.. (x6 x4 (f482f.. x7 (4ae4a.. 4a7ef..))) (f4dc0.. (x6 (f482f.. x7 4a7ef..) (f482f.. x7 (4ae4a.. 4a7ef..))))))) (94f9e.. (ac767.. (5246e.. x4) (5246e.. x5)) (λ x7 . bc82c.. (x6 (f482f.. x7 4a7ef..) x5) (bc82c.. (x6 x4 (f482f.. x7 (4ae4a.. 4a7ef..))) (f4dc0.. (x6 (f482f.. x7 4a7ef..) (f482f.. x7 (4ae4a.. 4a7ef..)))))))) (0ac37.. (94f9e.. (ac767.. (23e07.. x4) (5246e.. x5)) (λ x7 . bc82c.. (x6 (f482f.. x7 4a7ef..) x5) (bc82c.. (x6 x4 (f482f.. x7 (4ae4a.. 4a7ef..))) (f4dc0.. (x6 (f482f.. x7 4a7ef..) (f482f.. x7 (4ae4a.. 4a7ef..))))))) (94f9e.. (ac767.. (5246e.. x4) (23e07.. x5)) (λ x7 . bc82c.. (x6 (f482f.. x7 4a7ef..) x5) (bc82c.. (x6 x4 (f482f.. x7 (4ae4a.. 4a7ef..))) (f4dc0.. (x6 (f482f.. x7 4a7ef..) (f482f.. x7 (4ae4a.. 4a7ef..))))))))) x0 x1 x2 = (λ x4 x5 . λ x6 : ι → ι → ι . 02a50.. ... ...) ... ... ...
...
Apply unknownprop_0d078a833e20a13be15691da098ab7e638a79d34f684fe40cbe56431440f9e3e with λ x0 x1 . λ x2 : ι → ι → ι . 02a50.. (0ac37.. (94f9e.. (ac767.. (23e07.. x0) (23e07.. x1)) (λ x3 . bc82c.. (x2 (f482f.. x3 4a7ef..) x1) (bc82c.. (x2 x0 (f482f.. x3 (4ae4a.. 4a7ef..))) (f4dc0.. (x2 (f482f.. x3 4a7ef..) (f482f.. x3 (4ae4a.. 4a7ef..))))))) (94f9e.. (ac767.. (5246e.. x0) (5246e.. x1)) (λ x3 . bc82c.. (x2 (f482f.. x3 4a7ef..) x1) (bc82c.. (x2 x0 (f482f.. x3 (4ae4a.. 4a7ef..))) (f4dc0.. (x2 (f482f.. x3 4a7ef..) (f482f.. x3 (4ae4a.. 4a7ef..)))))))) (0ac37.. (94f9e.. (ac767.. (23e07.. x0) (5246e.. x1)) (λ x3 . bc82c.. (x2 (f482f.. x3 4a7ef..) x1) (bc82c.. (x2 x0 (f482f.. x3 (4ae4a.. 4a7ef..))) (f4dc0.. (x2 (f482f.. x3 4a7ef..) (f482f.. x3 (4ae4a.. 4a7ef..))))))) (94f9e.. (ac767.. (5246e.. x0) (23e07.. x1)) (λ x3 . bc82c.. (x2 (f482f.. x3 4a7ef..) x1) (bc82c.. (x2 x0 (f482f.. x3 (4ae4a.. 4a7ef..))) (f4dc0.. (x2 (f482f.. x3 4a7ef..) (f482f.. x3 (4ae4a.. 4a7ef..)))))))).
The subproof is completed by applying L0.