Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: 02b90.. x0 x1.
Apply H0 with and (and (and (and (80242.. (02a50.. x0 x1)) (prim1 (e4431.. (02a50.. x0 x1)) (4ae4a.. (0ac37.. (a842e.. x0 (λ x2 . 4ae4a.. (e4431.. x2))) (a842e.. x1 (λ x2 . 4ae4a.. (e4431.. x2))))))) (∀ x2 . prim1 x2 x0099f3.. x2 (02a50.. x0 x1))) (∀ x2 . prim1 x2 x1099f3.. (02a50.. x0 x1) x2)) (∀ x2 . 80242.. x2(∀ x3 . prim1 x3 x0099f3.. x3 x2)(∀ x3 . prim1 x3 x1099f3.. x2 x3)and (Subq (e4431.. (02a50.. x0 x1)) (e4431.. x2)) (SNoEq_ (e4431.. (02a50.. x0 x1)) (02a50.. x0 x1) x2)).
Assume H1: and (∀ x2 . prim1 x2 x080242.. x2) (∀ x2 . prim1 x2 x180242.. x2).
Apply H1 with (∀ x2 . prim1 x2 x0∀ x3 . prim1 x3 x1099f3.. x2 x3)and (and (and (and (80242.. (02a50.. x0 x1)) (prim1 (e4431.. (02a50.. x0 x1)) (4ae4a.. (0ac37.. (a842e.. x0 (λ x2 . 4ae4a.. (e4431.. x2))) (a842e.. x1 (λ x2 . 4ae4a.. (e4431.. x2))))))) (∀ x2 . prim1 x2 x0099f3.. x2 (02a50.. x0 x1))) (∀ x2 . prim1 x2 x1099f3.. (02a50.. x0 x1) x2)) (∀ x2 . 80242.. x2(∀ x3 . prim1 x3 x0099f3.. x3 x2)(∀ x3 . prim1 x3 x1099f3.. x2 x3)and (Subq (e4431.. (02a50.. x0 x1)) (e4431.. x2)) (SNoEq_ (e4431.. (02a50.. x0 x1)) (02a50.. x0 x1) x2)).
Assume H2: ∀ x2 . prim1 x2 x080242.. x2.
Assume H3: ∀ x2 . prim1 x2 x180242.. x2.
Assume H4: ∀ x2 . prim1 x2 x0∀ x3 . prim1 x3 x1099f3.. x2 x3.
Claim L5: ...
...
Claim L6: ...
...
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Apply unknownprop_6419f8fc1ff70ca950cf4e79a0f0cff9b9f9b876ea55c76aec20f2ed9adc5971 with λ x2 . λ x3 : ι → ο . and (ordinal x2) (prim1 (09072.. x2 x3) x0), λ x2 . λ x3 : ι → ο . and (ordinal x2) (prim1 (09072.. x2 x3) x1), 0ac37.. (a842e.. x0 (λ x2 . 4ae4a.. (e4431.. x2))) (a842e.. x1 (λ x2 . 4ae4a.. (e4431.. x2))), and (and (and (and (80242.. (02a50.. x0 ...)) ...) ...) ...) ... leaving 5 subgoals.
...
...
...
...
...