Search for blocks/addresses/...

Proofgold Proof

pf
Apply unknownprop_b01da77c5200afb1f524e6033a58358c3303b7f4989ae9962b195b5bb398525b with 4a7ef.., 4a7ef.., 02a50.. 4a7ef.. 4a7ef.. = 4a7ef.. leaving 2 subgoals.
The subproof is completed by applying unknownprop_ab73c81bad9b0bc12f7b25a40b099a542950fe0dc2eef2db876de2324d1cbfe7.
Assume H0: 80242.. (02a50.. 4a7ef.. 4a7ef..).
Apply unknownprop_a26d742a27f422bbd55009ea9b717bdec6c830941e6651a76a9cdb8f0820477c with λ x0 . 4ae4a.. (e4431.. x0), λ x0 x1 . prim1 (e4431.. (02a50.. 4a7ef.. 4a7ef..)) (4ae4a.. (0ac37.. x1 x1)) ⟶ (∀ x2 . prim1 x2 4a7ef.. ⟶ 099f3.. x2 (02a50.. 4a7ef.. 4a7ef..)) ⟶ (∀ x2 . prim1 x2 4a7ef.. ⟶ 099f3.. (02a50.. 4a7ef.. 4a7ef..) x2) ⟶ (∀ x2 . 80242.. x2 ⟶ (∀ x3 . prim1 x3 4a7ef.. ⟶ 099f3.. x3 x2) ⟶ (∀ x3 . prim1 x3 4a7ef.. ⟶ 099f3.. x2 x3) ⟶ and (Subq (e4431.. (02a50.. 4a7ef.. 4a7ef..)) (e4431.. x2)) (SNoEq_ (e4431.. (02a50.. 4a7ef.. 4a7ef..)) (02a50.. 4a7ef.. 4a7ef..) x2)) ⟶ 02a50.. 4a7ef.. 4a7ef.. = 4a7ef...
Apply unknownprop_fc17ae1257247ccbad94ae05ce6b26282126a44d809f22e0209b526a567506af with 4a7ef.., λ x0 x1 . prim1 (e4431.. (02a50.. 4a7ef.. 4a7ef..)) (4ae4a.. x1) ⟶ (∀ x2 . prim1 x2 4a7ef.. ⟶ 099f3.. x2 (02a50.. 4a7ef.. 4a7ef..)) ⟶ (∀ x2 . prim1 x2 4a7ef.. ⟶ 099f3.. (02a50.. 4a7ef.. 4a7ef..) x2) ⟶ (∀ x2 . 80242.. x2 ⟶ (∀ x3 . prim1 x3 4a7ef.. ⟶ 099f3.. x3 x2) ⟶ (∀ x3 . prim1 x3 4a7ef.. ⟶ 099f3.. x2 x3) ⟶ and (Subq (e4431.. (02a50.. 4a7ef.. 4a7ef..)) (e4431.. x2)) (SNoEq_ (e4431.. (02a50.. 4a7ef.. 4a7ef..)) (02a50.. 4a7ef.. 4a7ef..) x2)) ⟶ 02a50.. 4a7ef.. 4a7ef.. = 4a7ef...
Assume H1: prim1 (e4431.. (02a50.. 4a7ef.. 4a7ef..)) (4ae4a.. 4a7ef..).
Assume H2: ∀ x0 . prim1 x0 4a7ef.. ⟶ 099f3.. x0 (02a50.. 4a7ef.. 4a7ef..).
Assume H3: ∀ x0 . prim1 x0 4a7ef.. ⟶ 099f3.. (02a50.. 4a7ef.. 4a7ef..) x0.
Assume H4: ∀ x0 . 80242.. x0 ⟶ (∀ x1 . prim1 x1 4a7ef.. ⟶ 099f3.. x1 x0) ⟶ (∀ x1 . prim1 x1 4a7ef.. ⟶ 099f3.. x0 x1) ⟶ and (Subq (e4431.. (02a50.. 4a7ef.. 4a7ef..)) (e4431.. x0)) (SNoEq_ (e4431.. (02a50.. 4a7ef.. 4a7ef..)) (02a50.. 4a7ef.. 4a7ef..) x0).
Claim L5: ...
...
Apply unknownprop_c3102c186c7aa1001a5c1b1b7ecab6b25bcd639e713104221ece8bf414726a69 with 02a50.. 4a7ef.. 4a7ef.., 4a7ef.. leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_a66a65189a5389c2141d18df52f52fcf5f074fba68040a0bda3b8b81c830611a.
set y0 to be e4431.. (02a50.. 4a7ef.. 4a7ef..)
set y1 to be e4431.. 4a7ef..
Claim L6: ∀ x2 : ι → ο . x2 y1 ⟶ x2 y0
Let x2 of type ι → ο be given.
Assume H6: x2 (e4431.. 4a7ef..).
Apply L5 with λ x3 . x2.
set y3 to be λ x3 . x2
Apply unknownprop_514ace28c9a90c94edf6ffd2272d2d1fb4fe92ef818112b7c45dc1e893a67196 with λ x4 x5 . y3 x5 x4.
The subproof is completed by applying H6.
Let x2 of type ι → ι → ο be given.
Apply L6 with λ x3 . x2 x3 y1 ⟶ x2 y1 x3.
Assume H7: x2 y1 y1.
The subproof is completed by applying H7.
...
■