Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Assume H0: ChurchNum_3ary_proj_p x0.
Apply H0 with λ x1 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x2 : ο . (∀ x3 x4 : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (∀ x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x5 ⟶ ChurchNum_3ary_proj_p (x3 x5)) ⟶ (∀ x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x5 ⟶ ChurchNum_3ary_proj_p (x4 x5)) ⟶ (∀ x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x3 (x4 x5) = x5) ⟶ (∀ x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x4 (x3 x5) = x5) ⟶ (∀ x5 x6 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x7 x8 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . TwoRamseyGraph_4_5_24_ChurchNums_3x8 x5 x7 x6 x8 = TwoRamseyGraph_4_5_24_ChurchNums_3x8 (x3 x5) x7 (x3 x6) x8) ⟶ (x3 x1 = λ x5 x6 x7 : (ι → ι) → ι → ι . x5) ⟶ x2) ⟶ x2 leaving 3 subgoals.
Let x1 of type ο be given.
Assume H1: ∀ x2 x3 : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (∀ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x4 ⟶ ChurchNum_3ary_proj_p (x2 x4)) ⟶ (∀ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x4 ⟶ ChurchNum_3ary_proj_p (x3 x4)) ⟶ (∀ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x2 (x3 x4) = x4) ⟶ (∀ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x3 (x2 x4) = x4) ⟶ (∀ x4 x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x6 x7 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . TwoRamseyGraph_4_5_24_ChurchNums_3x8 x4 x6 x5 x7 = TwoRamseyGraph_4_5_24_ChurchNums_3x8 (x2 x4) x6 (x2 x5) x7) ⟶ (x2 (λ x4 x5 x6 : (ι → ι) → ι → ι . x4) = λ x4 x5 x6 : (ι → ι) → ι → ι . x4) ⟶ x1.
Apply H1 with λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x2, λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x2 leaving 6 subgoals.
Let x2 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Assume H2: ChurchNum_3ary_proj_p x2.
The subproof is completed by applying H2.
Let x2 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Assume H2: ChurchNum_3ary_proj_p x2.
The subproof is completed by applying H2.
Let x2 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x3 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H2: x3 ((λ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x4) x2) x2.
The subproof is completed by applying H2.
Let x2 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x3 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H2: x3 ((λ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x4) x2) x2.
The subproof is completed by applying H2.
Let x2 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x3 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x4 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x5 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x6 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H2: x6 (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x4 x3 x5) (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x4 x3 x5).
The subproof is completed by applying H2.
Let x2 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H2: x2 (λ x3 x4 x5 : (ι → ι) → ι → ι . x3) (λ x3 x4 x5 : (ι → ι) → ι → ι . x3).
The subproof is completed by applying H2.
Let x1 of type ο be given.
Assume H1: ∀ x2 x3 : (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . (∀ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x4 ⟶ ChurchNum_3ary_proj_p (x2 x4)) ⟶ (∀ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x4 ⟶ ChurchNum_3ary_proj_p (x3 x4)) ⟶ (∀ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x2 (x3 x4) = x4) ⟶ (∀ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . x3 (x2 x4) = x4) ⟶ (∀ x4 x5 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x6 x7 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . TwoRamseyGraph_4_5_24_ChurchNums_3x8 x4 x6 x5 x7 = TwoRamseyGraph_4_5_24_ChurchNums_3x8 (x2 x4) x6 (x2 x5) x7) ⟶ (x2 (λ x4 x5 x6 : (ι → ι) → ι → ι . x5) = λ x4 x5 x6 : (ι → ι) → ι → ι . x4) ⟶ x1.
Apply H1 with λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x3 x4 x5 : (ι → ι) → ι → ι . x2 x5 x3 x4, λ x2 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x3 x4 x5 : (ι → ι) → ι → ι . x2 x4 x5 x3 leaving 6 subgoals.
The subproof is completed by applying unknownprop_b16663a4709f3780eaa894042f5cda662025d92844722e880355abe7e12fa986.
The subproof is completed by applying unknownprop_5881c3490ed9d7d79e8da4ec398853ff06374776f16caecd18fd5e637a25c01e.
Let x2 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x3 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H2: x3 (λ x4 x5 x6 : (ι → ι) → ι → ι . (λ x7 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x8 x9 x10 : (ι → ι) → ι → ι . x7 x9 x10 x8) x2 x6 x4 x5) x2.
The subproof is completed by applying H2.
Let x2 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x3 of type (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → (((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι)) → ο be given.
Assume H2: x3 ((λ x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . λ x5 x6 x7 : (ι → ι) → ι → ι . x4 x6 x7 x5) (λ x4 x5 x6 : (ι → ι) → ι → ι . x2 x6 x4 x5)) x2.
The subproof is completed by applying H2.
Let x2 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x3 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x4 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x5 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x6 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H2: x6 (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x4 ... ...) ....
...
...
...
■