Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: 80242.. x0.
Apply unknownprop_f4c47e876b581d8d577d2c853ba9f380382521b2987b498decb65a17a2733264 with x0, 4a7ef.., e6316.. x0 4a7ef.. = 4a7ef.. leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_a66a65189a5389c2141d18df52f52fcf5f074fba68040a0bda3b8b81c830611a.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H1: ∀ x3 . prim1 x3 x1 ⟶ ∀ x4 : ο . (∀ x5 . prim1 x5 (23e07.. x0) ⟶ ∀ x6 . prim1 x6 (23e07.. 4a7ef..) ⟶ x3 = bc82c.. (e6316.. x5 4a7ef..) (bc82c.. (e6316.. x0 x6) (f4dc0.. (e6316.. x5 x6))) ⟶ x4) ⟶ (∀ x5 . prim1 x5 (5246e.. x0) ⟶ ∀ x6 . prim1 x6 (5246e.. 4a7ef..) ⟶ x3 = bc82c.. (e6316.. x5 4a7ef..) (bc82c.. (e6316.. x0 x6) (f4dc0.. (e6316.. x5 x6))) ⟶ x4) ⟶ x4.
Assume H2: ∀ x3 . prim1 x3 (23e07.. x0) ⟶ ∀ x4 . prim1 x4 (23e07.. 4a7ef..) ⟶ prim1 (bc82c.. (e6316.. x3 4a7ef..) (bc82c.. (e6316.. x0 x4) (f4dc0.. (e6316.. x3 x4)))) x1.
Assume H3: ∀ x3 . prim1 x3 (5246e.. x0) ⟶ ∀ x4 . prim1 x4 (5246e.. 4a7ef..) ⟶ prim1 (bc82c.. (e6316.. x3 4a7ef..) (bc82c.. (e6316.. x0 x4) (f4dc0.. (e6316.. x3 x4)))) x1.
Assume H4: ∀ x3 . prim1 x3 x2 ⟶ ∀ x4 : ο . (∀ x5 . prim1 x5 (23e07.. x0) ⟶ ∀ x6 . prim1 x6 (5246e.. 4a7ef..) ⟶ x3 = bc82c.. (e6316.. x5 4a7ef..) (bc82c.. (e6316.. x0 x6) (f4dc0.. (e6316.. x5 x6))) ⟶ x4) ⟶ (∀ x5 . prim1 x5 (5246e.. x0) ⟶ ∀ x6 . prim1 x6 (23e07.. 4a7ef..) ⟶ x3 = bc82c.. (e6316.. x5 4a7ef..) (bc82c.. (e6316.. x0 x6) (f4dc0.. (e6316.. x5 x6))) ⟶ x4) ⟶ x4.
Assume H5: ∀ x3 . prim1 x3 (23e07.. x0) ⟶ ∀ x4 . prim1 x4 (5246e.. 4a7ef..) ⟶ prim1 (bc82c.. (e6316.. x3 4a7ef..) (bc82c.. (e6316.. x0 x4) (f4dc0.. (e6316.. x3 x4)))) x2.
Assume H6: ∀ x3 . prim1 x3 (5246e.. x0) ⟶ ∀ x4 . prim1 x4 (23e07.. 4a7ef..) ⟶ prim1 (bc82c.. (e6316.. x3 4a7ef..) (bc82c.. (e6316.. x0 x4) (f4dc0.. (e6316.. x3 x4)))) x2.
Assume H7: e6316.. x0 4a7ef.. = 02a50.. x1 x2.
Apply H7 with λ x3 x4 . x4 = 4a7ef...
Claim L8: ...
...
Claim L9: x2 = 4a7ef..
Apply unknownprop_ea78574cb3264467ecb0cee6dab0f2cbbdf0e0a00f843238d57e1be6acdbe25f with x2.
Let x3 of type ι be given.
Assume H9: prim1 x3 x2.
Apply FalseE with ....
...
Apply L8 with λ x3 x4 . 02a50.. x4 x2 = 4a7ef...
Apply L9 with λ x3 x4 . 02a50.. 4a7ef.. x4 = 4a7ef...
The subproof is completed by applying unknownprop_014025907246c1e7f64513c3536e6f926c4bfe0a9480c1d274e85a7e594377c4.
■