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__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5 x0 x4) x2 (Church6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5 x2 x3) = λ x5 x6 . x5 leaving 4 subgoals.
The subproof is completed by applying H2.
Assume H5: Church6_lt4p x1.
Apply unknownprop_0e22f978562dc11600b4a135ff8bf16b6b22cc758598e8948a6ed9acd3e10295 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__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_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_2_3_0_1_4_5 x1) x2 (Church6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5 x2 x4) = λ x5 x6 . x5 leaving 4 subgoals.
The subproof is completed by applying H4.
Assume H6: Church6_lt4p x3.
Apply unknownprop_0e22f978562dc11600b4a135ff8bf16b6b22cc758598e8948a6ed9acd3e10295 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_2_3_0_1_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_34d0445a9eb4349bf533e02609a62eed06fba8535ef9778cc7a04d99c2765d4b 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_2_3_0_1_4_5 x4) x2 (Church6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_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_2_3_0_1_4_5 (λ x5 x6 x7 x8 x9 x10 . x5)) x2 (Church6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_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_2_3_0_1_4_5 (λ x5 x6 x7 x8 x9 x10 . x5)) x4 (Church6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_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).
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
■