Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ e523d...
Apply unknownprop_d0b18a67181e900ea67f7a0ba30a861268ef122d83dee9e0402983f02611aa3f with x0, x0 = a0628.. (28f8d.. x0) (22598.. 8d0f8.. (d634d.. 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 . x4 = a0628.. (28f8d.. x4) (22598.. 8d0f8.. (d634d.. x4)).
Apply unknownprop_b9b7bfb6c9b892d1b6018106403bf15df7213abab01ccecd88c7179d2ef8e566 with x1, x2, λ x3 x4 . ad280.. x1 x2 = a0628.. x4 (22598.. 8d0f8.. (d634d.. (ad280.. x1 x2))) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_fb49976af43b10d0ce8aeb3d9ab418005490959b10197c6c1e0102ac4ae81973 with x1, x2, λ x3 x4 . ad280.. x1 x2 = a0628.. x1 (22598.. 8d0f8.. x4) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_043a3a62e09a1e356d458c560264602babef6a620fa61db7abeb4595eeb25ec6 with x1, λ x3 x4 . ad280.. x1 x2 = ad280.. (add_SNo x4 (28f8d.. (22598.. 8d0f8.. x2))) (add_SNo (d634d.. x1) (d634d.. (22598.. 8d0f8.. x2))) leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_abceab960aaef5df9f001bc1cd13feb6de3a8aec9c7966ceadb450feb60c314d with x1, λ x3 x4 . ad280.. x1 x2 = ad280.. (add_SNo x1 (28f8d.. (22598.. 8d0f8.. x2))) (add_SNo x4 (d634d.. (22598.. 8d0f8.. x2))) leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_2ddf9ebfee65b76198f31be345197bbcbd14c1051a86330ee5479550122ecb8c with x2, λ x3 x4 . ad280.. x1 x2 = ad280.. (add_SNo x1 x4) (add_SNo 0 (d634d.. (22598.. 8d0f8.. x2))) leaving 2 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_87ece1a776d2238d0506557a76a01b60b7fd3659c484870634d9beeaa5ce23c3 with x2, λ x3 x4 . ad280.. x1 x2 = ad280.. (add_SNo x1 0) (add_SNo 0 x4) leaving 2 subgoals.
The subproof is completed by applying H2.
Apply add_SNo_0R with x1, λ x3 x4 . ad280.. x1 x2 = ad280.. x4 (add_SNo 0 x2) leaving 2 subgoals.
Apply real_SNo with x1.
The subproof is completed by applying H1.
Apply add_SNo_0L with x2, λ x3 x4 . ad280.. x1 x2 = ad280.. x1 x4 leaving 2 subgoals.
Apply real_SNo with x2.
The subproof is completed by applying H2.
Let x3 of type ι → ι → ο be given.
Assume H4: x3 (ad280.. x1 x2) (ad280.. x1 x2).
The subproof is completed by applying H4.
■