Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ο be given.
Assume H0: ∀ x1 . (∀ x2 . prim1 x2 x1 ⟶ x0 x2) ⟶ x0 x1.
Let x1 of type ι be given.
Apply dneg with x0 x1.
Assume H1: not (x0 x1).
Claim L2: prim1 x1 (2f2ea.. (e5b72.. x1))
Apply unknownprop_2e5c32a959d94838c299a421422ebbc5429b674377d15bb7aeecc717411104e2 with e5b72.. x1, x1.
The subproof is completed by applying unknownprop_1b39b6239e12488e23a0cc3dcb046ad70d13f361e325cf6f0925987c38e98e86 with x1.
Claim L3: prim1 x1 (1216a.. (2f2ea.. (e5b72.. x1)) (λ x2 . not (x0 x2)))
Apply unknownprop_1dada0fb38ff7f9b45b564ad11d6295d93250427446875218f17ee62431454a6 with 2f2ea.. (e5b72.. x1), λ x2 . not (x0 x2), x1 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H1.
Apply unknownprop_c305b585b05bbd5dfb1f2334fba160b28fdb98c88197eae477bd0e829ec1b7cd with 1216a.. (2f2ea.. (e5b72.. x1)) (λ x2 . not (x0 x2)), x1, False leaving 2 subgoals.
The subproof is completed by applying L3.
Let x2 of type ι be given.
Assume H4: (λ x3 . and (prim1 x3 (1216a.. (2f2ea.. (e5b72.. x1)) (λ x4 . not (x0 x4)))) (not (∃ x4 . and (prim1 x4 (1216a.. (2f2ea.. (e5b72.. x1)) (λ x5 . not (x0 x5)))) (prim1 x4 x3)))) x2.
Apply H4 with False.
Assume H5: prim1 x2 (1216a.. (2f2ea.. (e5b72.. x1)) (λ x3 . not (x0 x3))).
Assume H6: not (∃ x3 . and (prim1 x3 (1216a.. (2f2ea.. (e5b72.. x1)) (λ x4 . not (x0 x4)))) (prim1 x3 x2)).
Apply unknownprop_1a735e0b15c51014edc3ed5f97ce69cf216b51e9e6334150fbd47100bc945680 with 2f2ea.. (e5b72.. x1), λ x3 . not (x0 x3), x2, False leaving 2 subgoals.
The subproof is completed by applying H5.
Assume H7: prim1 x2 (2f2ea.. (e5b72.. x1)).
Assume H8: not (x0 x2).
Apply H8.
Apply H0 with x2.
Let x3 of type ι be given.
Assume H9: prim1 x3 x2.
Apply dneg with x0 x3.
Assume H10: not (x0 x3).
Apply H6.
Let x4 of type ο be given.
Assume H11: ∀ x5 . and (prim1 x5 (1216a.. (2f2ea.. (e5b72.. x1)) (λ x6 . not (x0 x6)))) (prim1 x5 x2) ⟶ x4.
Apply H11 with x3.
Apply andI with prim1 x3 (1216a.. (2f2ea.. (e5b72.. x1)) (λ x5 . not (x0 x5))), prim1 x3 x2 leaving 2 subgoals.
Apply unknownprop_1dada0fb38ff7f9b45b564ad11d6295d93250427446875218f17ee62431454a6 with 2f2ea.. (e5b72.. x1), λ x5 . not (x0 x5), x3 leaving 2 subgoals.
Apply unknownprop_3dcb81eed9b9b1587dd3c36235c8a9bbb36197e6269a3bdd2401c41aabe7298c with e5b72.. x1, x2, x3 leaving 2 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H9.
The subproof is completed by applying H10.
The subproof is completed by applying H9.
■