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_a x2 x1 x2 x1 = λ x3 x4 . x3 leaving 6 subgoals.

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

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

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

The subproof is completed by applying H2.

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

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

The subproof is completed by applying H2.

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

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

The subproof is completed by applying H2.

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

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

The subproof is completed by applying H2.

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

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

The subproof is completed by applying H2.

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

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

The subproof is completed by applying H2.

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

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

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

The subproof is completed by applying H2.

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

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

The subproof is completed by applying H2.

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

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

The subproof is completed by applying H2.

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

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

The subproof is completed by applying H2.

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

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

The subproof is completed by applying H2.

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

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

The subproof is completed by applying H2.

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

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

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

The subproof is completed by applying H2.

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

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

The subproof is completed by applying H2.

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

Assume H2: ....

...

...

...

...

...

...

...

■