Search for blocks/addresses/...

Proofgold Proof

pf
Apply unknownprop_24559f3e8e3d3599a5f9c7b8ac8e099f44e3a66c32ff486ef961dc9ddd1e4ecd with Sing 0, λ x0 x1 . 0, λ x0 x1 . 0, λ x0 x1 . 0, Sing 0, λ x0 x1 . 0, λ x0 x1 x2 . 0, λ x0 x1 . 0, λ x0 x1 x2 . 0, λ x0 x1 x2 . 0, λ x0 x1 . 0, λ x0 x1 . 0, λ x0 x1 . 0, λ x0 x1 . 0 leaving 5 subgoals.
The subproof is completed by applying unknownprop_036be7afbdfd2d64ccd6e875f372063621fb6f48dc3df3ba2697af8ad34e123b.
Let x0 of type ι be given.
Assume H0: In x0 (Sing 0).
Let x1 of type ι be given.
Assume H1: In x1 (Sing 0).
Let x2 of type ι → ι → ο be given.
Assume H2: x2 ((λ x3 x4 . 0) x0 x1) ((λ x3 x4 . 0) ((λ x3 x4 . 0) x1 x0) ((λ x3 x4 . 0) x0 x1)).
The subproof is completed by applying H2.
Let x0 of type ι be given.
Assume H0: In x0 (Sing 0).
Let x1 of type ι be given.
Assume H1: In x1 (Sing 0).
Let x2 of type ι be given.
Assume H2: In x2 (Sing 0).
Let x3 of type ι → ι → ο be given.
Assume H3: x3 ((λ x4 x5 x6 . 0) x0 x1 x2) ((λ x4 x5 . 0) ((λ x4 x5 . 0) x0 ((λ x4 x5 . 0) x1 x2)) ((λ x4 x5 . 0) ((λ x4 x5 . 0) x0 x1) x2)).
The subproof is completed by applying H3.
Let x0 of type ι be given.
Assume H0: In x0 (Sing 0).
Let x1 of type ι be given.
Assume H1: In x1 (Sing 0).
Apply unknownprop_9b09b99fce48fbc4294fba4077c15371ba18b57a0bc4e20cfa1cf1c48cd99108 with (λ x2 x3 . 0) x0 x1 = (λ x2 x3 . 0) x0 ((λ x2 x3 . 0) x1 x0), (λ x2 x3 . 0) x0 x1 = (λ x2 x3 . 0) x0 ((λ x2 x3 . 0) x1 ((λ x2 x3 . 0) x0 (Sing 0))), (λ x2 x3 . 0) x0 x1 = (λ x2 x3 . 0) ((λ x2 x3 . 0) ((λ x2 x3 . 0) (Sing 0) x0) x1) x0, (λ x2 x3 . 0) x0 x1 = (λ x2 x3 . 0) ((λ x2 x3 . 0) x0 x1) ((λ x2 x3 . 0) ((λ x2 x3 . 0) x0 (Sing 0)) (Sing 0)), (λ x2 x3 . 0) x0 x1 = (λ x2 x3 . 0) ((λ x2 x3 . 0) (Sing 0) ((λ x2 x3 . 0) (Sing 0) x0)) ((λ x2 x3 . 0) x1 x0) leaving 5 subgoals.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 ((λ x3 x4 . 0) x0 x1) ((λ x3 x4 . 0) x0 ((λ x3 x4 . 0) x1 x0)).
The subproof is completed by applying H2.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 ((λ x3 x4 . 0) x0 x1) ((λ x3 x4 . 0) x0 ((λ x3 x4 . 0) x1 ((λ x3 x4 . 0) x0 (Sing 0)))).
The subproof is completed by applying H2.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 ((λ x3 x4 . 0) x0 x1) ((λ x3 x4 . 0) ((λ x3 x4 . 0) ((λ x3 x4 . 0) (Sing 0) x0) x1) x0).
The subproof is completed by applying H2.
Let x2 of type ι → ι → ο be given.
Assume H2: x2 ((λ x3 x4 . 0) x0 x1) ((λ x3 x4 . 0) ((λ x3 x4 . 0) x0 x1) ((λ x3 x4 . 0) ((λ x3 x4 . 0) ... ...) ...)).
...
...
...
■