Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 x4 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ∀ x5 x6 x7 x8 x9 : ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → (ι → ι) → ι → ι . ChurchNum_3ary_proj_p x0 ⟶ ChurchNum_8ary_proj_p x5 ⟶ x1 = ChurchNums_8x3_to_3_lt5_id_ge5_rot2 x5 x0 ⟶ x6 = ChurchNums_8_perm_3_4_5_6_7_0_1_2 x5 ⟶ ChurchNum_3ary_proj_p x2 ⟶ ChurchNum_3ary_proj_p x3 ⟶ ChurchNum_3ary_proj_p x4 ⟶ ChurchNum_8ary_proj_p x7 ⟶ ChurchNum_8ary_proj_p x8 ⟶ ChurchNum_8ary_proj_p x9 ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x2 x7 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x3 x8 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x5 x4 x9 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x6 x2 x7 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x6 x3 x8 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x6 x4 x9 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x7 x3 x8 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x2 x7 x4 x9 = λ x11 x12 . x12) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x3 x8 x4 x9 = λ x11 x12 . x12) ⟶ False

as obj
-

as prop
1b4dc..

theory
HotG

stx
f2682..

address
TMVDi..