Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: eb6e9.. x0.
Let x1 of type ι be given.
Assume H1: 69b7e.. x1 x0.
Apply H1 with 21582.. x1 x0.
Assume H2: and (30750.. x0) (30750.. x1).
Assume H3: 93c99.. x0 (λ x2 . λ x3 : ι → ι → ι . 93c99.. x1 (λ x4 . λ x5 : ι → ι → ι . and (and (x1 = 987b2.. x4 x3) (4f2b4.. (987b2.. x4 x3))) (Subq x4 x2))).
Apply H2 with 21582.. x1 x0.
Assume H4: 30750.. x0.
Assume H5: 30750.. x1.
Claim L6: eb6e9.. x0 ⟶ 69b7e.. x1 x0 ⟶ 21582.. x1 x0
Apply H4 with λ x2 . eb6e9.. x2 ⟶ 69b7e.. x1 x2 ⟶ 21582.. x1 x2.
Let x2 of type ι be given.
Let x3 of type ι → ι → ι be given.
Assume H6: ∀ x4 . prim1 x4 x2 ⟶ ∀ x5 . prim1 x5 x2 ⟶ prim1 (x3 x4 x5) x2.
Assume H7: eb6e9.. (987b2.. x2 x3).
Apply unknownprop_2972efc2aa208f3baec53c8c8671cf8384a3e7553df7f03d1bf32cc2d41743f5 with x2, x3, 69b7e.. x1 (987b2.. x2 x3) ⟶ 21582.. x1 (987b2.. x2 x3) leaving 2 subgoals.
The subproof is completed by applying H7.
Assume H8: 4f2b4.. (987b2.. x2 x3).
Assume H9: explicit_abelian x2 x3.
Apply H5 with λ x4 . 69b7e.. x4 (987b2.. x2 x3) ⟶ 21582.. x4 (987b2.. x2 x3).
Let x4 of type ι be given.
Let x5 of type ι → ι → ι be given.
Assume H10: ∀ x6 . prim1 x6 x4 ⟶ ∀ x7 . prim1 x7 x4 ⟶ prim1 (x5 x6 x7) x4.
Assume H11: 69b7e.. (987b2.. x4 x5) (987b2.. x2 x3).
Claim L12: 7fe8f.. x2 x3 x4
Apply unknownprop_8a8b3072385f65c851385b35246a4b711e6bd63000d15cc8311a66f73fe8acbb with x4, x2, x5, x3, 7fe8f.. x2 x3 x4 leaving 2 subgoals.
The subproof is completed by applying H11.
Assume H12: 987b2.. x4 x5 = 987b2.. x4 x3.
Assume H13: 7fe8f.. x2 x3 x4.
The subproof is completed by applying H13.
Claim L13: Subq x4 x2
Apply L12 with Subq x4 x2.
Assume H13: 4f2b4.. (987b2.. x4 x3).
Assume H14: Subq x4 x2.
The subproof is completed by applying H14.
Apply andI with 69b7e.. (987b2.. x4 x5) (987b2.. x2 x3), 93c99.. (987b2.. x2 x3) (λ x6 . λ x7 : ι → ι → ι . 93c99.. (987b2.. x4 x5) (λ x8 . λ x9 : ι → ι → ι . a0fbb.. x6 x7 x8)) leaving 2 subgoals.
The subproof is completed by applying H11.
Apply unknownprop_fd9b414d53f5c8f5d7710355c2b3169e514f24dfdecce1fa008d22140cf4afca with x4, x2, x5, x3, λ x6 x7 : ο . x7 leaving 3 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying L13.
Apply unknownprop_6161122a5731344d666c115fcbcb96cbaecf836949f09b876abbcc2b0e85d6d0 with x2, x3, x4 leaving 3 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying L12.
The subproof is completed by applying H9.
Apply L6 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
■