Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ e523d...
Apply unknownprop_d0b18a67181e900ea67f7a0ba30a861268ef122d83dee9e0402983f02611aa3f with x0, c7ce4.. x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Assume H1: x1 ∈ real.
Let x2 of type ι be given.
Assume H2: x2 ∈ real.
Assume H3: x0 = ad280.. x1 x2.
Apply H3 with λ x3 x4 . c7ce4.. x4.
Apply unknownprop_942959aad6790cf3a71a2f8f2b9ffc552b42fb28a7f163a4f5e7e7842fdbd934 with x1, x2 leaving 2 subgoals.
Apply real_SNo with x1.
The subproof is completed by applying H1.
Apply real_SNo with x2.
The subproof is completed by applying H2.
■