Proofgold Proof

pf

Let x0 of type ι be given.

Assume H0: x0 ∈ u6.

Apply unknownprop_d3b792af1adffec16ce4fc340f1433694e312f9a299dc66e7bdd660386d0095e with λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_a x2 x2 (nth_6_tuple u5) (nth_6_tuple x0) = λ x3 x4 . x3.

Apply unknownprop_d1ab6c05d827ab2f0497648eeb2e74b0b0260f4e004a74cbc06a5c0a175e4a2a with λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_a (λ x3 x4 x5 x6 x7 x8 . x7) (λ x3 x4 x5 x6 x7 x8 . x7) x2 (nth_6_tuple x0) = λ x3 x4 . x3.

Apply cases_6 with x0, λ x1 . TwoRamseyGraph_4_6_Church6_squared_a (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x7) (nth_6_tuple x1) = λ x2 x3 . x2 leaving 7 subgoals.

The subproof is completed by applying H0.

Apply unknownprop_5e063b347ef5ac56a92183cc00c589df53087ab1e0b6353a236a973dc2f46966 with λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_a (λ x3 x4 x5 x6 x7 x8 . x7) (λ x3 x4 x5 x6 x7 x8 . x7) (λ x3 x4 x5 x6 x7 x8 . x8) x2 = λ x3 x4 . x3.

Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.

Assume H1: x1 (TwoRamseyGraph_4_6_Church6_squared_a (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x7) (λ x2 x3 x4 x5 x6 x7 . x2)) (λ x2 x3 . x2).

The subproof is completed by applying H1.

Apply unknownprop_487e017004ecabac0b8e518f0fcaf45b502b6f60f5af04ddefe015bde12eaf50 with λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_a (λ x3 x4 x5 x6 x7 x8 . x7) (λ x3 x4 x5 x6 x7 x8 . x7) (λ x3 x4 x5 x6 x7 x8 . x8) x2 = λ x3 x4 . x3.

Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.

Assume H1: x1 (TwoRamseyGraph_4_6_Church6_squared_a (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x7) (λ x2 x3 x4 x5 x6 x7 . x3)) (λ x2 x3 . x2).

The subproof is completed by applying H1.

Apply unknownprop_9205282ef77caa3eed787eb4fa460a34079ef649c9bf4aa55e938da8cedd6fa2 with λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_a (λ x3 x4 x5 x6 x7 x8 . x7) (λ x3 x4 x5 x6 x7 x8 . x7) (λ x3 x4 x5 x6 x7 x8 . x8) x2 = λ x3 x4 . x3.

Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.

Assume H1: x1 (TwoRamseyGraph_4_6_Church6_squared_a (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x7) (λ x2 x3 x4 x5 x6 x7 . x4)) (λ x2 x3 . x2).

The subproof is completed by applying H1.

Apply unknownprop_d77aca9102a0a7995bbfb825c57cbe3520e1f56683b5c476fb6c9389a8c86331 with λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_a (λ x3 x4 x5 x6 x7 x8 . x7) (λ x3 x4 x5 x6 x7 x8 . x7) (λ x3 x4 x5 x6 x7 x8 . x8) x2 = λ x3 x4 . x3.

Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.

Assume H1: x1 (TwoRamseyGraph_4_6_Church6_squared_a (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x7) (λ x2 x3 x4 x5 x6 x7 . x5)) (λ x2 x3 . x2).

The subproof is completed by applying H1.

Apply unknownprop_d3b792af1adffec16ce4fc340f1433694e312f9a299dc66e7bdd660386d0095e with λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_a (λ x3 x4 x5 x6 x7 x8 . x7) (λ x3 x4 x5 x6 x7 x8 . x7) (λ x3 x4 x5 x6 x7 x8 . x8) x2 = λ x3 x4 . x3.

Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.

Assume H1: x1 (TwoRamseyGraph_4_6_Church6_squared_a (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x7) (λ x2 x3 x4 x5 x6 x7 . x6)) (λ x2 x3 . x2).

The subproof is completed by applying H1.

Apply unknownprop_d1ab6c05d827ab2f0497648eeb2e74b0b0260f4e004a74cbc06a5c0a175e4a2a with λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_a (λ x3 x4 x5 x6 x7 x8 . x7) (λ x3 x4 x5 x6 x7 x8 . x7) (λ x3 x4 x5 x6 x7 x8 . x8) x2 = λ x3 x4 . x3.

Let x1 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.

Assume H1: x1 (TwoRamseyGraph_4_6_Church6_squared_a (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x7) (λ x2 x3 x4 x5 x6 x7 . x7)) (λ x2 x3 . x2).

The subproof is completed by applying H1.

■