Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: ...
...
Let x0 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x1 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
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.
Assume H1: ChurchNum_3ary_proj_p x0.
Assume H2: ChurchNum_3ary_proj_p x1.
Assume H3: ChurchNum_3ary_proj_p x2.
Assume H4: ChurchNum_8ary_proj_p x3.
Assume H5: ChurchNum_8ary_proj_p x4.
Assume H6: ChurchNum_8ary_proj_p x5.
Apply xm with ∀ x6 : ο . ((x0 = λ x7 x8 x9 : (ι → ι) → ι → ι . x7) ⟶ (x3 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x11) ⟶ x6) ⟶ ((x0 = λ x7 x8 x9 : (ι → ι) → ι → ι . x8) ⟶ (x3 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x8) ⟶ x6) ⟶ ((x0 = λ x7 x8 x9 : (ι → ι) → ι → ι . x8) ⟶ (x3 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x14) ⟶ x6) ⟶ ((x0 = λ x7 x8 x9 : (ι → ι) → ι → ι . x9) ⟶ (x3 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x11) ⟶ x6) ⟶ x6, (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x0 x3 = λ x6 x7 . x6) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x1 x4 = λ x6 x7 . x6) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x2 x5 = λ x6 x7 . x6) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x3 x1 x4 = λ x6 x7 . x6) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x3 x2 x5 = λ x6 x7 . x6) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x4 x2 x5 = λ x6 x7 . x6) ⟶ ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x0 x3 ⟶ ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x1 x4 ⟶ ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x2 x5 ⟶ ChurchNums_3x8_neq x0 x3 x1 x4 ⟶ ChurchNums_3x8_neq x0 x3 x2 x5 ⟶ ChurchNums_3x8_neq x1 x4 x2 x5 ⟶ False leaving 2 subgoals.
Assume H7: ∀ x6 : ο . ((x0 = λ x7 x8 x9 : (ι → ι) → ι → ι . x7) ⟶ (x3 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x11) ⟶ x6) ⟶ ((x0 = λ x7 x8 x9 : (ι → ι) → ι → ι . x8) ⟶ (x3 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x8) ⟶ x6) ⟶ ((x0 = λ x7 x8 x9 : (ι → ι) → ι → ι . x8) ⟶ (x3 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x14) ⟶ x6) ⟶ ((x0 = λ x7 x8 x9 : (ι → ι) → ι → ι . x9) ⟶ (x3 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x11) ⟶ x6) ⟶ x6.
Apply xm with ∀ x6 : ο . ((x1 = λ x7 x8 x9 : (ι → ι) → ι → ι . x7) ⟶ (x4 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x11) ⟶ x6) ⟶ ((x1 = λ x7 x8 x9 : (ι → ι) → ι → ι . x8) ⟶ (x4 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x8) ⟶ x6) ⟶ ((x1 = λ x7 x8 x9 : (ι → ι) → ι → ι . x8) ⟶ (x4 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x14) ⟶ x6) ⟶ ((x1 = λ x7 x8 x9 : (ι → ι) → ι → ι . x9) ⟶ (x4 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x11) ⟶ x6) ⟶ x6, ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x4 x2 x5 = ... ⟶ ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x0 x3 ⟶ ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x1 x4 ⟶ ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x2 x5 ⟶ ChurchNums_3x8_neq x0 x3 x1 x4 ⟶ ChurchNums_3x8_neq x0 x3 x2 x5 ⟶ ChurchNums_3x8_neq x1 x4 x2 x5 ⟶ False leaving 2 subgoals.
...
...
...
■