Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: ...
...
Let x0 of type ι → ι → ι → ι → ι → ι → ι be given.
Let x1 of type ι → ι → ι → ι → ι → ι → ι be given.
Let x2 of type ι → ι → ι → ι → ι → ι → ι be given.
Let x3 of type ι → ι → ι → ι → ι → ι → ι be given.
Assume H1: Church6_p x0.
Assume H2: Church6_p x1.
Assume H3: Church6_p x2.
Assume H4: Church6_p x3.
Apply unknownprop_b54b6027f17f74407872b79435a97bc6b80bb4e8d1a20c185f9858d492a97c96 with x1, λ x4 : ι → ι → ι → ι → ι → ι → ι . (TwoRamseyGraph_4_6_Church6_squared_a x0 x4 x2 x3 = λ x5 x6 . x5) ⟶ TwoRamseyGraph_4_6_Church6_squared_a x0 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 x0 x4) x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 x2 x3) = λ x5 x6 . x5 leaving 4 subgoals.
The subproof is completed by applying H2.
Assume H5: Church6_lt4p x1.
Apply unknownprop_24d40161be3326708bb1791d69b3030e2d35eb727e96e9ca61ddef06d9651762 with x0, x1, λ x4 x5 : ι → ι → ι → ι → ι → ι → ι . (TwoRamseyGraph_4_6_Church6_squared_a x0 x1 x2 x3 = λ x6 x7 . x6) ⟶ TwoRamseyGraph_4_6_Church6_squared_a x0 x5 x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 x2 x3) = λ x6 x7 . x6 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H5.
Apply unknownprop_b54b6027f17f74407872b79435a97bc6b80bb4e8d1a20c185f9858d492a97c96 with x3, λ x4 : ι → ι → ι → ι → ι → ι → ι . (TwoRamseyGraph_4_6_Church6_squared_a x0 x1 x2 x4 = λ x5 x6 . x5) ⟶ TwoRamseyGraph_4_6_Church6_squared_a x0 (permargs_i_3_2_1_0_4_5 x1) x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 x2 x4) = λ x5 x6 . x5 leaving 4 subgoals.
The subproof is completed by applying H4.
Assume H6: Church6_lt4p x3.
Apply unknownprop_24d40161be3326708bb1791d69b3030e2d35eb727e96e9ca61ddef06d9651762 with x2, x3, λ x4 x5 : ι → ι → ι → ι → ι → ι → ι . (TwoRamseyGraph_4_6_Church6_squared_a x0 x1 x2 x3 = λ x6 x7 . x6) ⟶ TwoRamseyGraph_4_6_Church6_squared_a x0 (permargs_i_3_2_1_0_4_5 x1) x2 x5 = λ x6 x7 . x6 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
Apply unknownprop_6d71764a9a024a8f382431694d77ea6a197ff3b7947ee01f2f148455e062af95 with x0, x1, x2, x3 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H5.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
Apply H5 with λ x4 : ι → ι → ι → ι → ι → ι → ι . (TwoRamseyGraph_4_6_Church6_squared_a x0 x4 x2 (λ x5 x6 x7 x8 x9 x10 . x9) = λ x5 x6 . x5) ⟶ TwoRamseyGraph_4_6_Church6_squared_a x0 (permargs_i_3_2_1_0_4_5 x4) x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 x2 (λ x5 x6 x7 x8 x9 x10 . x9)) = λ x5 x6 . x5 leaving 4 subgoals.
Apply H1 with λ x4 : ι → ι → ι → ι → ι → ι → ι . (TwoRamseyGraph_4_6_Church6_squared_a x4 (λ x5 x6 x7 x8 x9 x10 . x5) x2 (λ x5 x6 x7 x8 x9 x10 . x9) = λ x5 x6 . x5) ⟶ TwoRamseyGraph_4_6_Church6_squared_a x4 (permargs_i_3_2_1_0_4_5 (λ x5 x6 x7 x8 x9 x10 . x5)) x2 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 x2 (λ x5 x6 x7 x8 x9 x10 . x9)) = λ x5 x6 . x5 leaving 6 subgoals.
Apply H3 with λ x4 : ι → ι → ι → ι → ι → ι → ι . (TwoRamseyGraph_4_6_Church6_squared_a (λ x5 x6 x7 x8 x9 x10 . x5) (λ x5 x6 x7 x8 x9 x10 . x5) x4 (λ x5 x6 x7 x8 x9 x10 . x9) = λ x5 x6 . x5) ⟶ TwoRamseyGraph_4_6_Church6_squared_a (λ x5 x6 x7 x8 x9 x10 . x5) (permargs_i_3_2_1_0_4_5 (λ x5 x6 x7 x8 x9 x10 . x5)) x4 (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 x4 (λ x5 x6 x7 x8 x9 x10 . x9)) = λ x5 x6 . x5 leaving 6 subgoals.
Assume H6: TwoRamseyGraph_4_6_Church6_squared_a (λ x4 x5 x6 x7 x8 x9 . x4) (λ x4 x5 x6 x7 x8 x9 . x4) (λ x4 x5 x6 x7 x8 x9 . x4) (λ x4 x5 x6 x7 x8 x9 . x8) = λ x4 x5 . x4.
Let x4 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H7: x4 (TwoRamseyGraph_4_6_Church6_squared_a (λ x5 x6 x7 x8 x9 x10 . x5) (λ x5 x6 x7 x8 x9 x10 . x6) (λ x5 x6 x7 x8 x9 x10 . x5) (λ x5 x6 x7 x8 x9 x10 . x10)) (λ x5 x6 . x5).
The subproof is completed by applying H7.
Assume H6: TwoRamseyGraph_4_6_Church6_squared_a (λ x4 x5 x6 x7 x8 x9 . x4) (λ x4 x5 x6 x7 x8 x9 . x4) (λ x4 x5 x6 x7 x8 x9 . x5) (λ x4 x5 x6 x7 x8 x9 . x8) = λ x4 x5 . x4.
Let x4 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H7: x4 (TwoRamseyGraph_4_6_Church6_squared_a (λ x5 x6 x7 x8 x9 x10 . x5) (λ x5 x6 x7 x8 x9 x10 . x6) (λ x5 x6 x7 x8 x9 x10 . x6) (λ x5 x6 x7 x8 x9 x10 . x10)) (λ x5 x6 . x5).
The subproof is completed by applying H7.
Assume H6: TwoRamseyGraph_4_6_Church6_squared_a (λ x4 x5 x6 x7 x8 x9 . x4) (λ x4 x5 x6 x7 x8 x9 . x4) (λ x4 x5 x6 x7 x8 x9 . x6) (λ x4 x5 x6 x7 x8 x9 . x8) = λ x4 x5 . x4.
Let x4 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H7: x4 (TwoRamseyGraph_4_6_Church6_squared_a (λ x5 x6 x7 x8 x9 x10 . x5) (λ x5 x6 x7 x8 x9 x10 . x6) (λ x5 x6 x7 x8 x9 x10 . x7) (λ x5 x6 x7 x8 x9 x10 . x10)) (λ x5 x6 . x5).
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
■