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__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5 x0 x4) x2 (Church6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5 x2 x3) = λ x5 x6 . x5 leaving 4 subgoals.
The subproof is completed by applying H2.
Assume H5: Church6_lt4p x1.
Apply unknownprop_c35e210bc890655bb18f2c72273114a4004d14748f0b7fe9ea498c0e3375abc0 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__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_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_1_0_3_2_4_5 x1) x2 (Church6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5 x2 x4) = λ x5 x6 . x5 leaving 4 subgoals.
The subproof is completed by applying H4.
Assume H6: Church6_lt4p x3.
Apply unknownprop_c35e210bc890655bb18f2c72273114a4004d14748f0b7fe9ea498c0e3375abc0 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_1_0_3_2_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_a5e13a507ed763e1221778c5f185d9665cca8a2887500ac259a9b8c3fa36c3a9 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_1_0_3_2_4_5 x4) x2 (Church6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_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_1_0_3_2_4_5 (λ x5 x6 x7 x8 x9 x10 . x5)) x2 (Church6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_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_1_0_3_2_4_5 (λ x5 x6 x7 x8 x9 x10 . x5)) x4 (Church6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_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).
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
■