Proofgold Proof

pf

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

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

Assume H0: Church13_p x0.

Assume H1: Church13_p x1.

Apply H0 with λ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . or (TwoRamseyGraph_3_5_Church13 x2 x1 = λ x3 x4 . x3) (TwoRamseyGraph_3_5_Church13 x2 x1 = λ x3 x4 . x4) leaving 13 subgoals.

Apply H1 with λ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . or (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) x2 = λ x3 x4 . x3) (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) x2 = λ x3 x4 . x4) leaving 13 subgoals.

Apply orIR with TwoRamseyGraph_3_5_Church13 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) = λ x2 x3 . x2, TwoRamseyGraph_3_5_Church13 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) = λ x2 x3 . x3.

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

Assume H2: x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)) (λ x3 x4 . x4).

The subproof is completed by applying H2.

Apply orIL with TwoRamseyGraph_3_5_Church13 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x3) = λ x2 x3 . x2, TwoRamseyGraph_3_5_Church13 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x3) = λ x2 x3 . x3.

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

Assume H2: x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x4)) (λ x3 x4 . x3).

The subproof is completed by applying H2.

Apply orIR with TwoRamseyGraph_3_5_Church13 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x4) = λ x2 x3 . x2, TwoRamseyGraph_3_5_Church13 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x4) = λ x2 x3 . x3.

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

Assume H2: x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x5)) (λ x3 x4 . x4).

The subproof is completed by applying H2.

Apply orIR with TwoRamseyGraph_3_5_Church13 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x5) = λ x2 x3 . x2, TwoRamseyGraph_3_5_Church13 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x5) = λ x2 x3 . x3.

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

Assume H2: x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x6)) (λ x3 x4 . x4).

The subproof is completed by applying H2.

Apply orIR with TwoRamseyGraph_3_5_Church13 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x6) = λ x2 x3 . x2, TwoRamseyGraph_3_5_Church13 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x6) = λ x2 x3 . x3.

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

Assume H2: x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x7)) (λ x3 x4 . x4).

The subproof is completed by applying H2.

Apply orIL with TwoRamseyGraph_3_5_Church13 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x7) = λ x2 x3 . x2, TwoRamseyGraph_3_5_Church13 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x7) = λ x2 x3 . x3.

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

Assume H2: x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x8)) (λ x3 x4 . x3).

The subproof is completed by applying H2.

Apply orIR with TwoRamseyGraph_3_5_Church13 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x8) = λ x2 x3 . x2, TwoRamseyGraph_3_5_Church13 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x8) = λ x2 x3 . x3.

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

Assume H2: x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x9)) (λ x3 x4 . x4).

The subproof is completed by applying H2.

Apply orIR with TwoRamseyGraph_3_5_Church13 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x9) = λ x2 x3 . x2, TwoRamseyGraph_3_5_Church13 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x9) = λ x2 x3 . x3.

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

Assume H2: x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x10)) (λ x3 x4 . x4).

The subproof is completed by applying H2.

Apply orIL with TwoRamseyGraph_3_5_Church13 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x10) = λ x2 x3 . x2, TwoRamseyGraph_3_5_Church13 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x10) = λ x2 x3 . x3.

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

Assume H2: x2 ... ....

...

...

...

...

...

...

...

...

...

...

...

...

...

...

...

...

...

■