Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: ∀ x0 . ba9d8.. x009364.. x0 = 4ae4a.. x0
Apply unknownprop_f4ee121fb14a7412699d1f11bebf17d33e1718030f72ebf91211f8d97c32541d with λ x0 . 09364.. x0 = 4ae4a.. x0.
Let x0 of type ι be given.
Assume H0: ba9d8.. x0.
Assume H1: ∀ x1 . prim1 x1 x009364.. x1 = 4ae4a.. x1.
Apply set_ext with 09364.. x0, 4ae4a.. x0 leaving 2 subgoals.
Let x1 of type ι be given.
Assume H2: prim1 x1 (09364.. x0).
Apply unknownprop_b16c51a027be568304bbf4d10214f2f7bab4a7ef1f3929990ec85447bbbf7c12 with x0, x1, prim1 x1 (4ae4a.. x0) leaving 3 subgoals.
The subproof is completed by applying H2.
Assume H3: x1 = 4a7ef...
Apply H3 with λ x2 x3 . prim1 x3 (4ae4a.. x0).
Apply unknownprop_7e0c935491619684fa66567f06da9cc071afa3d37e60afae747b20bc8c762543 with x0.
The subproof is completed by applying H0.
Assume H3: ∃ x2 . and (prim1 x2 x0) (x1 = 09364.. x2).
Apply exandE_i with λ x2 . prim1 x2 x0, λ x2 . x1 = 09364.. x2, prim1 x1 (4ae4a.. x0) leaving 2 subgoals.
The subproof is completed by applying H3.
Let x2 of type ι be given.
Assume H4: prim1 x2 x0.
Assume H5: x1 = 09364.. x2.
Apply H5 with λ x3 x4 . prim1 x4 (4ae4a.. x0).
Apply H1 with x2, λ x3 x4 . prim1 x4 (4ae4a.. x0) leaving 2 subgoals.
The subproof is completed by applying H4.
Apply unknownprop_ce7857b9839b8f7083d025f6387f2962c755c06bcc9de82bcdf74f1839394154 with x0, x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Let x1 of type ι be given.
Assume H2: prim1 x1 (4ae4a.. x0).
Apply unknownprop_dec2978c0a72cebd51fcab0a380f03d4d80d1ccd8f826d378953148c305a60f0 with x0, x1, prim1 x1 (09364.. x0) leaving 3 subgoals.
The subproof is completed by applying H2.
Assume H3: prim1 x1 x0.
Apply unknownprop_aca6b7de025ab03c50b497c9de8f58254c0701f6ade5e0855cf800060b35ff63 with x1, prim1 x1 (09364.. x0) leaving 3 subgoals.
Apply unknownprop_e6223cc37d124575a1439a62a8bd81090d2105429a9944c39d898ad59aaee24d with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Assume H4: x1 = 4a7ef...
Apply H4 with λ x2 x3 . prim1 x3 (09364.. x0).
The subproof is completed by applying unknownprop_f2280590a4843dd3047de5e5151d043be723c7f73a981e4edcbfbfe0904566e7 with x0.
Assume H4: ∃ x2 . and (ba9d8.. x2) (x1 = 4ae4a.. x2).
Apply exandE_i with ba9d8.., λ x2 . x1 = 4ae4a.. x2, prim1 x1 (09364.. x0) leaving 2 subgoals.
The subproof is completed by applying H4.
Let x2 of type ι be given.
Assume H5: ba9d8.. x2.
Assume H6: x1 = 4ae4a.. x2.
Apply H6 with λ x3 x4 . prim1 x4 (09364.. x0).
Claim L7: prim1 x2 x1
Apply H6 with λ x3 x4 . prim1 x2 x4.
The subproof is completed by applying unknownprop_38ce50d6b52a0a920b530e7796207ec902a42d65414467df1ecd3efb123f4cb9 with x2.
Claim L8: prim1 x2 x0
Apply unknownprop_43b9163da17f2f66e991f3dd23439608e22bc07ac3880a089612020a7b3f5243 with x0, x1, x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
The subproof is completed by applying L7.
Apply H1 with x2, λ x3 x4 . prim1 x3 (09364.. x0) leaving 2 subgoals.
The subproof is completed by applying L8.
Apply unknownprop_83de80e22aba688e4d8cf3ccc9ec372406ae5110cef0bf0846317bfd1d974b00 with x0, x2.
The subproof is completed by applying L8.
Assume H3: x1 = x0.
Apply H3 with λ x2 x3 . prim1 x3 (09364.. x0).
Apply unknownprop_aca6b7de025ab03c50b497c9de8f58254c0701f6ade5e0855cf800060b35ff63 with x0, prim1 x0 (09364.. x0) leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H4: x0 = 4a7ef...
Apply H4 with λ x2 x3 . prim1 x3 (09364.. x0).
The subproof is completed by applying unknownprop_f2280590a4843dd3047de5e5151d043be723c7f73a981e4edcbfbfe0904566e7 with x0.
Assume H4: ∃ x2 . and (ba9d8.. x2) (x0 = 4ae4a.. x2).
Apply exandE_i with ba9d8.., λ x2 . x0 = 4ae4a.. x2, prim1 x0 (09364.. x0) leaving 2 subgoals.
The subproof is completed by applying H4.
Let x2 of type ι be given.
Assume H5: ba9d8.. x2.
Assume H6: x0 = 4ae4a.. x2.
Apply H6 with λ x3 x4 . prim1 x4 (09364.. x0).
Claim L7: ...
...
Apply H1 with x2, λ x3 x4 . prim1 x3 (09364.. x0) leaving 2 subgoals.
The subproof is completed by applying L7.
Apply unknownprop_83de80e22aba688e4d8cf3ccc9ec372406ae5110cef0bf0846317bfd1d974b00 with ..., ....
...
Let x0 of type ι be given.
Assume H1: ba9d8.. x0.
Apply unknownprop_497ceb2eb28aaf14c46cc38f218092e3e652567d5b5313af58a8c57d6bddfd1b with x0, λ x1 x2 . x2 = 4ae4a.. x0.
Apply L0 with x0.
The subproof is completed by applying H1.