Search for blocks/addresses/...

Proofgold Proof

pf
Apply unknownprop_f04ee3f2db7dade92ee7be101bff40fb89f733bb0c0340f09b616cd72154ad93 with λ x0 . ∀ x1 x2 . 02b90.. x1 x2 ⟶ x0 = 02a50.. x1 x2 ⟶ f4dc0.. x0 = 02a50.. (94f9e.. x2 (λ x3 . f4dc0.. x3)) (94f9e.. x1 (λ x3 . f4dc0.. x3)).
Let x0 of type ι be given.
Assume H0: 80242.. x0.
Assume H1: ∀ x1 . prim1 x1 (56ded.. (e4431.. x0)) ⟶ ∀ x2 x3 . 02b90.. x2 x3 ⟶ x1 = 02a50.. x2 x3 ⟶ f4dc0.. x1 = 02a50.. (94f9e.. x3 (λ x4 . f4dc0.. x4)) (94f9e.. x2 (λ x4 . f4dc0.. x4)).
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H2: 02b90.. x1 x2.
Apply H2 with x0 = 02a50.. x1 x2 ⟶ f4dc0.. x0 = 02a50.. (94f9e.. x2 (λ x3 . f4dc0.. x3)) (94f9e.. x1 (λ x3 . f4dc0.. x3)).
Assume H3: and (∀ x3 . prim1 x3 x1 ⟶ 80242.. x3) (∀ x3 . prim1 x3 x2 ⟶ 80242.. x3).
Apply H3 with (∀ x3 . prim1 x3 x1 ⟶ ∀ x4 . prim1 x4 x2 ⟶ 099f3.. x3 x4) ⟶ x0 = 02a50.. x1 x2 ⟶ f4dc0.. x0 = 02a50.. (94f9e.. x2 (λ x3 . f4dc0.. x3)) (94f9e.. x1 (λ x3 . f4dc0.. x3)).
Assume H4: ∀ x3 . prim1 x3 x1 ⟶ 80242.. x3.
Assume H5: ∀ x3 . prim1 x3 x2 ⟶ 80242.. x3.
Assume H6: ∀ x3 . prim1 x3 x1 ⟶ ∀ x4 . prim1 x4 x2 ⟶ 099f3.. x3 x4.
Assume H7: x0 = 02a50.. x1 x2.
Claim L8: ...
...
Claim L9: ...
...
Apply unknownprop_b01da77c5200afb1f524e6033a58358c3303b7f4989ae9962b195b5bb398525b with 94f9e.. x2 (λ x3 . f4dc0.. x3), 94f9e.. x1 (λ x3 . f4dc0.. x3), f4dc0.. x0 = 02a50.. (94f9e.. x2 (λ x3 . f4dc0.. x3)) (94f9e.. x1 (λ x3 . f4dc0.. x3)) leaving 2 subgoals.
The subproof is completed by applying L9.
Assume H10: 80242.. (02a50.. (94f9e.. x2 (λ x3 . f4dc0.. x3)) (94f9e.. x1 (λ x3 . f4dc0.. x3))).
Assume H11: prim1 (e4431.. (02a50.. (94f9e.. x2 (λ x3 . f4dc0.. x3)) (94f9e.. x1 (λ x3 . f4dc0.. x3)))) (4ae4a.. (0ac37.. (a842e.. (94f9e.. x2 (λ x3 . f4dc0.. x3)) (λ x3 . 4ae4a.. (e4431.. x3))) (a842e.. (94f9e.. x1 (λ x3 . f4dc0.. x3)) (λ x3 . 4ae4a.. (e4431.. x3))))).
Assume H12: ∀ x3 . prim1 x3 (94f9e.. x2 (λ x4 . f4dc0.. x4)) ⟶ 099f3.. x3 (02a50.. (94f9e.. x2 (λ x4 . f4dc0.. x4)) (94f9e.. x1 (λ x4 . f4dc0.. x4))).
Assume H13: ∀ x3 . ... ⟶ 099f3.. (02a50.. (94f9e.. x2 (λ x4 . f4dc0.. x4)) (94f9e.. ... ...)) ....
...
■