Search for blocks/addresses/...

Proofgold Proof

pf
Apply unknownprop_98dce570015dab8b9107dc33a5e2e4ea0417c490e1cfe00b91b6267d26e82089 with λ x0 x1 . e6316.. (f4dc0.. x0) x1 = f4dc0.. (e6316.. x0 x1).
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: 80242.. x0.
Assume H1: 80242.. x1.
Assume H2: ∀ x2 . prim1 x2 (56ded.. (e4431.. x0)) ⟶ e6316.. (f4dc0.. x2) x1 = f4dc0.. (e6316.. x2 x1).
Assume H3: ∀ x2 . prim1 x2 (56ded.. (e4431.. x1)) ⟶ e6316.. (f4dc0.. x0) x2 = f4dc0.. (e6316.. x0 x2).
Assume H4: ∀ x2 . prim1 x2 (56ded.. (e4431.. x0)) ⟶ ∀ x3 . prim1 x3 (56ded.. (e4431.. x1)) ⟶ e6316.. (f4dc0.. x2) x3 = f4dc0.. (e6316.. x2 x3).
Claim L5: ...
...
Apply unknownprop_0bba6b6e1ff88cb6fe93e4b3f72d170fee2180507070ff2fab0f5b4dc92e6b37 with x0, x1, e6316.. (f4dc0.. x0) x1 = f4dc0.. (e6316.. x0 x1) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Let x3 of type ι be given.
Assume H6: 02b90.. x2 x3.
Assume H7: ∀ x4 . prim1 x4 x2 ⟶ ∀ x5 : ο . (∀ x6 . prim1 x6 (23e07.. x0) ⟶ ∀ x7 . prim1 x7 (23e07.. x1) ⟶ x4 = bc82c.. (e6316.. x6 x1) (bc82c.. (e6316.. x0 x7) (f4dc0.. (e6316.. x6 x7))) ⟶ x5) ⟶ (∀ x6 . prim1 x6 (5246e.. x0) ⟶ ∀ x7 . prim1 x7 (5246e.. x1) ⟶ x4 = bc82c.. (e6316.. x6 x1) (bc82c.. (e6316.. x0 x7) (f4dc0.. (e6316.. x6 x7))) ⟶ x5) ⟶ x5.
Assume H8: ∀ x4 . prim1 x4 (23e07.. x0) ⟶ ∀ x5 . prim1 x5 (23e07.. x1) ⟶ prim1 (bc82c.. (e6316.. x4 x1) (bc82c.. (e6316.. x0 x5) (f4dc0.. (e6316.. x4 x5)))) x2.
Assume H9: ∀ x4 . prim1 x4 (5246e.. x0) ⟶ ∀ x5 . prim1 x5 (5246e.. x1) ⟶ prim1 (bc82c.. (e6316.. x4 x1) (bc82c.. (e6316.. x0 x5) (f4dc0.. (e6316.. x4 x5)))) x2.
Assume H10: ∀ x4 . prim1 x4 x3 ⟶ ∀ x5 : ο . (∀ x6 . prim1 x6 (23e07.. x0) ⟶ ∀ x7 . prim1 x7 (5246e.. x1) ⟶ x4 = bc82c.. (e6316.. x6 x1) (bc82c.. (e6316.. x0 x7) (f4dc0.. (e6316.. x6 x7))) ⟶ x5) ⟶ (∀ x6 . prim1 x6 (5246e.. x0) ⟶ ∀ x7 . prim1 x7 (23e07.. x1) ⟶ x4 = bc82c.. (e6316.. x6 x1) (bc82c.. (e6316.. x0 x7) (f4dc0.. (e6316.. x6 x7))) ⟶ x5) ⟶ x5.
Assume H11: ∀ x4 . ... ⟶ ∀ x5 . ... ⟶ prim1 (bc82c.. (e6316.. x4 x1) (bc82c.. (e6316.. ... ...) ...)) ....
...
■