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.
Let x2 of type ο be given.
Assume H2: x0 = x1 ⟶ x2.
Assume H3: ∀ x3 . prim1 x3 (23e07.. x1) ⟶ prim1 x3 (5246e.. x0) ⟶ x2.
Assume H4: prim1 x0 (23e07.. x1) ⟶ x2.
Assume H5: prim1 x1 (5246e.. x0) ⟶ x2.
Assume H6: ∀ x3 . prim1 x3 (5246e.. x1) ⟶ prim1 x3 (23e07.. x0) ⟶ x2.
Assume H7: prim1 x0 (5246e.. x1) ⟶ x2.
Assume H8: prim1 x1 (23e07.. x0) ⟶ x2.
Apply unknownprop_0ee892b382deeaff7058bdf3a060a6e4c2a4fd7b393d1bfa260184a50103d5bc with x0, x1, x2 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H9: 099f3.. x0 x1.
Apply unknownprop_5b79c7b60026b1292d3a4c99449a3eb71ef42a395180ae8cdfb38d53ce85b7d8 with x0, x1, x2 leaving 6 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H9.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Assume H9: x0 = x1.
Apply H2.
The subproof is completed by applying H9.
Assume H9: 099f3.. x1 x0.
Apply unknownprop_5b79c7b60026b1292d3a4c99449a3eb71ef42a395180ae8cdfb38d53ce85b7d8 with x1, x0, x2 leaving 6 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H9.
Let x3 of type ι be given.
Assume H10: prim1 x3 (23e07.. x0).
Assume H11: prim1 x3 (5246e.. x1).
Apply H6 with x3 leaving 2 subgoals.
The subproof is completed by applying H11.
The subproof is completed by applying H10.
The subproof is completed by applying H8.
The subproof is completed by applying H7.
■