Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x1 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Assume H0: ChurchNum_3ary_proj_p x0.
Assume H1: ChurchNum_8ary_proj_p x1.
Apply H0 with λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p (ChurchNums_3x8_3_lt1_swap_1_2_ge1_rot2 x2 x1) leaving 3 subgoals.
Apply H1 with λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p (ChurchNums_3x8_3_lt1_swap_1_2_ge1_rot2 (λ x3 x4 x5 : (ι → ι) → ι → ι . x3) x2) leaving 8 subgoals.
The subproof is completed by applying unknownprop_b3205a5f97a9b7efdf9cf8b544efa479d104ae9763ca62a574fc2597b5138348.
The subproof is completed by applying unknownprop_f3fbe0dcd7af60cbd2c45144c1a80d31889ed8fd9e1689678c35da17d6e44ed6.
The subproof is completed by applying unknownprop_f3fbe0dcd7af60cbd2c45144c1a80d31889ed8fd9e1689678c35da17d6e44ed6.
The subproof is completed by applying unknownprop_f3fbe0dcd7af60cbd2c45144c1a80d31889ed8fd9e1689678c35da17d6e44ed6.
The subproof is completed by applying unknownprop_f3fbe0dcd7af60cbd2c45144c1a80d31889ed8fd9e1689678c35da17d6e44ed6.
The subproof is completed by applying unknownprop_f3fbe0dcd7af60cbd2c45144c1a80d31889ed8fd9e1689678c35da17d6e44ed6.
The subproof is completed by applying unknownprop_f3fbe0dcd7af60cbd2c45144c1a80d31889ed8fd9e1689678c35da17d6e44ed6.
The subproof is completed by applying unknownprop_f3fbe0dcd7af60cbd2c45144c1a80d31889ed8fd9e1689678c35da17d6e44ed6.
Apply H1 with λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p (ChurchNums_3x8_3_lt1_swap_1_2_ge1_rot2 (λ x3 x4 x5 : (ι → ι) → ι → ι . x4) x2) leaving 8 subgoals.
The subproof is completed by applying unknownprop_f3fbe0dcd7af60cbd2c45144c1a80d31889ed8fd9e1689678c35da17d6e44ed6.
The subproof is completed by applying unknownprop_e6edcda273718db468f4cfbb333cc08373d8662c42f27ca851ee375409a4b89e.
The subproof is completed by applying unknownprop_e6edcda273718db468f4cfbb333cc08373d8662c42f27ca851ee375409a4b89e.
The subproof is completed by applying unknownprop_e6edcda273718db468f4cfbb333cc08373d8662c42f27ca851ee375409a4b89e.
The subproof is completed by applying unknownprop_e6edcda273718db468f4cfbb333cc08373d8662c42f27ca851ee375409a4b89e.
The subproof is completed by applying unknownprop_e6edcda273718db468f4cfbb333cc08373d8662c42f27ca851ee375409a4b89e.
The subproof is completed by applying unknownprop_e6edcda273718db468f4cfbb333cc08373d8662c42f27ca851ee375409a4b89e.
The subproof is completed by applying unknownprop_e6edcda273718db468f4cfbb333cc08373d8662c42f27ca851ee375409a4b89e.
Apply H1 with λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p (ChurchNums_3x8_3_lt1_swap_1_2_ge1_rot2 (λ x3 x4 x5 : (ι → ι) → ι → ι . x5) x2) leaving 8 subgoals.
The subproof is completed by applying unknownprop_e6edcda273718db468f4cfbb333cc08373d8662c42f27ca851ee375409a4b89e.
The subproof is completed by applying unknownprop_b3205a5f97a9b7efdf9cf8b544efa479d104ae9763ca62a574fc2597b5138348.
The subproof is completed by applying unknownprop_b3205a5f97a9b7efdf9cf8b544efa479d104ae9763ca62a574fc2597b5138348.
The subproof is completed by applying unknownprop_b3205a5f97a9b7efdf9cf8b544efa479d104ae9763ca62a574fc2597b5138348.
The subproof is completed by applying unknownprop_b3205a5f97a9b7efdf9cf8b544efa479d104ae9763ca62a574fc2597b5138348.
The subproof is completed by applying unknownprop_b3205a5f97a9b7efdf9cf8b544efa479d104ae9763ca62a574fc2597b5138348.
The subproof is completed by applying unknownprop_b3205a5f97a9b7efdf9cf8b544efa479d104ae9763ca62a574fc2597b5138348.
The subproof is completed by applying unknownprop_b3205a5f97a9b7efdf9cf8b544efa479d104ae9763ca62a574fc2597b5138348.
■