Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: 80242.. x0.
Assume H1: 80242.. x1.
Apply unknownprop_b7caf5f70ae79c72282a4433b7742206b9e82c71b0701b7f8019ceccbdfb80a7 with x0, x1, 80242.. (bc82c.. x0 x1) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H2: and (and (and (and (80242.. (bc82c.. x0 x1)) (∀ x2 . prim1 x2 (23e07.. x0) ⟶ 099f3.. (bc82c.. x2 x1) (bc82c.. x0 x1))) (∀ x2 . prim1 x2 (5246e.. x0) ⟶ 099f3.. (bc82c.. x0 x1) (bc82c.. x2 x1))) (∀ x2 . prim1 x2 (23e07.. x1) ⟶ 099f3.. (bc82c.. x0 x2) (bc82c.. x0 x1))) (∀ x2 . prim1 x2 (5246e.. x1) ⟶ 099f3.. (bc82c.. x0 x1) (bc82c.. x0 x2)).
Apply H2 with 02b90.. (0ac37.. (94f9e.. (23e07.. x0) (λ x2 . bc82c.. x2 x1)) (94f9e.. (23e07.. x1) (bc82c.. x0))) (0ac37.. (94f9e.. (5246e.. x0) (λ x2 . bc82c.. x2 x1)) (94f9e.. (5246e.. x1) (bc82c.. x0))) ⟶ 80242.. (bc82c.. x0 x1).
Assume H3: and (and (and (80242.. (bc82c.. x0 x1)) (∀ x2 . prim1 x2 (23e07.. x0) ⟶ 099f3.. (bc82c.. x2 x1) (bc82c.. x0 x1))) (∀ x2 . prim1 x2 (5246e.. x0) ⟶ 099f3.. (bc82c.. x0 x1) (bc82c.. x2 x1))) (∀ x2 . prim1 x2 (23e07.. x1) ⟶ 099f3.. (bc82c.. x0 x2) (bc82c.. x0 x1)).
Apply H3 with (∀ x2 . prim1 x2 (5246e.. x1) ⟶ 099f3.. (bc82c.. x0 x1) (bc82c.. x0 x2)) ⟶ 02b90.. (0ac37.. (94f9e.. (23e07.. x0) (λ x2 . bc82c.. x2 x1)) (94f9e.. (23e07.. x1) (bc82c.. x0))) (0ac37.. (94f9e.. (5246e.. x0) (λ x2 . bc82c.. x2 x1)) (94f9e.. (5246e.. x1) (bc82c.. x0))) ⟶ 80242.. (bc82c.. x0 x1).
Assume H4: and (and (80242.. (bc82c.. x0 x1)) (∀ x2 . prim1 x2 (23e07.. x0) ⟶ 099f3.. (bc82c.. x2 x1) (bc82c.. x0 x1))) (∀ x2 . prim1 x2 (5246e.. x0) ⟶ 099f3.. (bc82c.. x0 x1) (bc82c.. x2 x1)).
Apply H4 with ... ⟶ (∀ x2 . ... ⟶ 099f3.. (bc82c.. ... ...) ...) ⟶ 02b90.. (0ac37.. (94f9e.. (23e07.. x0) (λ x2 . bc82c.. x2 x1)) (94f9e.. (23e07.. x1) (bc82c.. x0))) (0ac37.. (94f9e.. (5246e.. x0) (λ x2 . bc82c.. x2 x1)) (94f9e.. (5246e.. x1) (bc82c.. x0))) ⟶ 80242.. (bc82c.. x0 x1).
...
■