Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x1 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Assume H0: ChurchNum_8ary_proj_p x0.
Apply H0 with λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x1 ⟶ ChurchNum_3ary_proj_p (ChurchNums_8x3_to_3_lt4_id_ge4_rot2 x2 x1) leaving 8 subgoals.
Assume H1: ChurchNum_3ary_proj_p x1.
The subproof is completed by applying H1.
Assume H1: ChurchNum_3ary_proj_p x1.
The subproof is completed by applying H1.
Assume H1: ChurchNum_3ary_proj_p x1.
The subproof is completed by applying H1.
Assume H1: ChurchNum_3ary_proj_p x1.
The subproof is completed by applying H1.
Assume H1: ChurchNum_3ary_proj_p x1.
Apply unknownprop_5881c3490ed9d7d79e8da4ec398853ff06374776f16caecd18fd5e637a25c01e with x1.
The subproof is completed by applying H1.
Assume H1: ChurchNum_3ary_proj_p x1.
Apply unknownprop_5881c3490ed9d7d79e8da4ec398853ff06374776f16caecd18fd5e637a25c01e with x1.
The subproof is completed by applying H1.
Assume H1: ChurchNum_3ary_proj_p x1.
Apply unknownprop_5881c3490ed9d7d79e8da4ec398853ff06374776f16caecd18fd5e637a25c01e with x1.
The subproof is completed by applying H1.
Assume H1: ChurchNum_3ary_proj_p x1.
Apply unknownprop_5881c3490ed9d7d79e8da4ec398853ff06374776f16caecd18fd5e637a25c01e with x1.
The subproof is completed by applying H1.
■