Search for blocks/addresses/...

Proofgold Proof

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