Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H0: In x0 3.
Assume H1: In x1 3.
Assume H2: In x2 3.
Assume H3: not (x0 = x1).
Assume H4: not (x0 = x2).
Assume H5: not (x1 = x2).
Claim L6: ...
...
Claim L7: ...
...
Claim L8: ...
...
Apply unknownprop_50049cb08ded1102cafef929946d9c8ea6123047d68bb1e4e7608faddaa0e3b3 with 3, λ x3 . ap (lam 3 (λ x4 . If_i (x4 = 0) x0 (If_i (x4 = 1) x1 x2))) x3 leaving 3 subgoals.
Apply unknownprop_077979b790f9097ea9250573e60509ec9410103c35a67e0558983ee18582fb09 with 2.
The subproof is completed by applying unknownprop_d97d6922f54612bc34684069408098060ad6c1b04a8b4fda7efccfad8c5e25b7.
Let x3 of type ι be given.
Assume H9: In x3 3.
Apply unknownprop_f20f08b38429d0914c6a2c13ffdd3fa446ab4342ea7a43d47915b2eca12847ee with x3, λ x4 . In (ap (lam 3 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 x2))) x4) 3 leaving 4 subgoals.
The subproof is completed by applying H9.
Apply unknownprop_72ee6a4729e4d36966f7c731b465de1ffff5565146924f50f9d4e56e3e4f5133 with x0, x1, x2, λ x4 x5 . In x5 3.
The subproof is completed by applying H0.
Apply unknownprop_ad0347fd00c465af5dfdd914ea5ee88ed02126a7c7ef66823f6c720d34ff7b99 with x0, x1, x2, λ x4 x5 . In x5 3.
The subproof is completed by applying H1.
Apply unknownprop_8a884b2bd6ff36eba8856072c2baa52cff32d5e85b68403b704927d5d62d4773 with x0, x1, x2, λ x4 x5 . In x5 3.
The subproof is completed by applying H2.
Let x3 of type ι be given.
Assume H9: In x3 3.
Let x4 of type ι be given.
Assume H10: In x4 3.
Apply unknownprop_f20f08b38429d0914c6a2c13ffdd3fa446ab4342ea7a43d47915b2eca12847ee with x3, λ x5 . ap (lam 3 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 x2))) x5 = ap (lam 3 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 x2))) x4 ⟶ x5 = x4 leaving 4 subgoals.
The subproof is completed by applying H9.
Apply unknownprop_f20f08b38429d0914c6a2c13ffdd3fa446ab4342ea7a43d47915b2eca12847ee with x4, λ x5 . ap (lam 3 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 x2))) 0 = ap (lam 3 (λ x6 . If_i (x6 = 0) x0 (If_i (x6 = 1) x1 x2))) x5 ⟶ 0 = x5 leaving 4 subgoals.
The subproof is completed by applying H10.
Assume H11: ap (lam 3 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 x2))) 0 = ap (lam 3 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 x2))) 0.
Let x5 of type ι → ι → ο be given.
Assume H12: x5 0 0.
The subproof is completed by applying H12.
Apply unknownprop_72ee6a4729e4d36966f7c731b465de1ffff5565146924f50f9d4e56e3e4f5133 with x0, x1, x2, λ x5 x6 . (λ x7 . x6 = ap (lam 3 (λ x8 . If_i (x8 = 0) x0 (If_i (x8 = 1) x1 x2))) x7 ⟶ 0 = x7) 1.
Apply unknownprop_ad0347fd00c465af5dfdd914ea5ee88ed02126a7c7ef66823f6c720d34ff7b99 with x0, x1, x2, λ x5 x6 . x0 = x6 ⟶ 0 = 1.
Assume H11: x0 = x1.
Apply L6 with 0 = 1.
The subproof is completed by applying H11.
Apply unknownprop_72ee6a4729e4d36966f7c731b465de1ffff5565146924f50f9d4e56e3e4f5133 with x0, x1, x2, λ x5 x6 . (λ x7 . x6 = ap (lam 3 (λ x8 . If_i (x8 = 0) ... ...)) ... ⟶ 0 = x7) 2.
...
...
...
■