Proofgold Proof

pf

Let x0 of type ι → ι → ι → ι → ι → ι → ι be given.

Let x1 of type ι → ι → ι → ι → ι → ι → ι be given.

Assume H0: Church6_p x0.

Assume H1: Church6_p x1.

Apply H0 with λ x2 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_b x2 x1 (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8) = λ x3 x4 . x4 leaving 6 subgoals.

Apply H1 with λ x2 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_b (λ x3 x4 x5 x6 x7 x8 . x3) x2 (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8) = λ x3 x4 . x4 leaving 6 subgoals.

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

Assume H2: x2 (TwoRamseyGraph_4_6_Church6_squared_b (λ x3 x4 x5 x6 x7 x8 . x3) (λ x3 x4 x5 x6 x7 x8 . x3) (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8)) (λ x3 x4 . x4).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_4_6_Church6_squared_b (λ x3 x4 x5 x6 x7 x8 . x3) (λ x3 x4 x5 x6 x7 x8 . x4) (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8)) (λ x3 x4 . x4).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_4_6_Church6_squared_b (λ x3 x4 x5 x6 x7 x8 . x3) (λ x3 x4 x5 x6 x7 x8 . x5) (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8)) (λ x3 x4 . x4).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_4_6_Church6_squared_b (λ x3 x4 x5 x6 x7 x8 . x3) (λ x3 x4 x5 x6 x7 x8 . x6) (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8)) (λ x3 x4 . x4).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_4_6_Church6_squared_b (λ x3 x4 x5 x6 x7 x8 . x3) (λ x3 x4 x5 x6 x7 x8 . x7) (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8)) (λ x3 x4 . x4).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_4_6_Church6_squared_b (λ x3 x4 x5 x6 x7 x8 . x3) (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8)) (λ x3 x4 . x4).

The subproof is completed by applying H2.

Apply H1 with λ x2 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_b (λ x3 x4 x5 x6 x7 x8 . x4) x2 (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8) = λ x3 x4 . x4 leaving 6 subgoals.

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

Assume H2: x2 (TwoRamseyGraph_4_6_Church6_squared_b (λ x3 x4 x5 x6 x7 x8 . x4) (λ x3 x4 x5 x6 x7 x8 . x3) (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8)) (λ x3 x4 . x4).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_4_6_Church6_squared_b (λ x3 x4 x5 x6 x7 x8 . x4) (λ x3 x4 x5 x6 x7 x8 . x4) (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8)) (λ x3 x4 . x4).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_4_6_Church6_squared_b (λ x3 x4 x5 x6 x7 x8 . x4) (λ x3 x4 x5 x6 x7 x8 . x5) (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8)) (λ x3 x4 . x4).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_4_6_Church6_squared_b (λ x3 x4 x5 x6 x7 x8 . x4) (λ x3 x4 x5 x6 x7 x8 . x6) (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8)) (λ x3 x4 . x4).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_4_6_Church6_squared_b (λ x3 x4 x5 x6 x7 x8 . x4) (λ x3 x4 x5 x6 x7 x8 . x7) (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8)) (λ x3 x4 . x4).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_4_6_Church6_squared_b (λ x3 x4 x5 x6 x7 x8 . x4) (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8)) (λ x3 x4 . x4).

The subproof is completed by applying H2.

Apply H1 with λ x2 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_b (λ x3 x4 x5 x6 x7 x8 . x5) x2 (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8) = λ x3 x4 . x4 leaving 6 subgoals.

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

Assume H2: x2 (TwoRamseyGraph_4_6_Church6_squared_b (λ x3 x4 x5 x6 x7 x8 . x5) (λ x3 x4 x5 x6 x7 x8 . x3) (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8)) (λ x3 x4 . x4).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_4_6_Church6_squared_b (λ x3 x4 x5 x6 x7 x8 . x5) (λ x3 x4 x5 x6 x7 x8 . x4) (λ x3 x4 x5 x6 x7 x8 . x8) (λ x3 x4 x5 x6 x7 x8 . x8)) ....

...

...

...

...

...

...

...

...

■