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_lt2_id_ge2_rot1 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.
Apply unknownprop_b16663a4709f3780eaa894042f5cda662025d92844722e880355abe7e12fa986 with x1.
The subproof is completed by applying H1.
Assume H1: ChurchNum_3ary_proj_p x1.
Apply unknownprop_b16663a4709f3780eaa894042f5cda662025d92844722e880355abe7e12fa986 with x1.
The subproof is completed by applying H1.
Assume H1: ChurchNum_3ary_proj_p x1.
Apply unknownprop_b16663a4709f3780eaa894042f5cda662025d92844722e880355abe7e12fa986 with x1.
The subproof is completed by applying H1.
Assume H1: ChurchNum_3ary_proj_p x1.
Apply unknownprop_b16663a4709f3780eaa894042f5cda662025d92844722e880355abe7e12fa986 with x1.
The subproof is completed by applying H1.
Assume H1: ChurchNum_3ary_proj_p x1.
Apply unknownprop_b16663a4709f3780eaa894042f5cda662025d92844722e880355abe7e12fa986 with x1.
The subproof is completed by applying H1.
Assume H1: ChurchNum_3ary_proj_p x1.
Apply unknownprop_b16663a4709f3780eaa894042f5cda662025d92844722e880355abe7e12fa986 with x1.
The subproof is completed by applying H1.
■