Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: ...
...
Let x0 of type ι be given.
Assume H1: x0 ∈ u16.
Let x1 of type ι be given.
Apply unknownprop_485b5a544f4a752392d62c01e55a5e36a8748d64fd7af6f27349bd2453284446 with x0, λ x2 . x1 ∈ x2 ⟶ TwoRamseyGraph_3_6_17 (u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 x2) (u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 x1) ⟶ TwoRamseyGraph_3_6_17 x2 x1 leaving 17 subgoals.
The subproof is completed by applying H1.
Assume H2: x1 ∈ 0.
Apply FalseE with TwoRamseyGraph_3_6_17 (u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 0) (u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 x1) ⟶ TwoRamseyGraph_3_6_17 0 x1.
Apply EmptyE with x1.
The subproof is completed by applying H2.
Assume H2: x1 ∈ u1.
Apply cases_1 with x1, λ x2 . TwoRamseyGraph_3_6_17 (u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u1) (u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 x2) ⟶ TwoRamseyGraph_3_6_17 u1 x2 leaving 2 subgoals.
The subproof is completed by applying H2.
Assume H3: TwoRamseyGraph_3_6_17 (u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u1) (u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 0).
Assume H4: u1 ∈ u17.
Assume H5: 0 ∈ u17.
Apply unknownprop_f880a8473dab9f58d69fbf332c8547d500ca315e405258a93c99a34f8560efb6 with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_3_6_Church17 x3 (u17_to_Church17 0) = λ x4 x5 . x4.
Apply unknownprop_84aaefca7211a57d89e0df96a1f742653d3cc05f82d5ab568090ade3cb9ffcfd with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_3_6_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x5) x3 = λ x4 x5 . x4.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H6: x2 (TwoRamseyGraph_3_6_Church17 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x4) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3)) (λ x3 x4 . x3).
The subproof is completed by applying H6.
Assume H2: x1 ∈ u2.
Apply cases_2 with x1, λ x2 . TwoRamseyGraph_3_6_17 (u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u2) (u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 x2) ⟶ TwoRamseyGraph_3_6_17 u2 x2 leaving 3 subgoals.
The subproof is completed by applying H2.
Assume H3: TwoRamseyGraph_3_6_17 (u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u2) (u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 0).
Assume H4: u2 ∈ u17.
Assume H5: 0 ∈ u17.
Apply unknownprop_7c154441ca7b7a9fe09539322ad6531c3f48333c7018e2f8c866c0af44719d1a with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_3_6_Church17 x3 (u17_to_Church17 0) = λ x4 x5 . x4.
Apply unknownprop_84aaefca7211a57d89e0df96a1f742653d3cc05f82d5ab568090ade3cb9ffcfd with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_3_6_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x6) x3 = λ x4 x5 . x4.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H6: x2 (TwoRamseyGraph_3_6_Church17 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x5) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x3)) (λ x3 x4 . x3).
The subproof is completed by applying H6.
Apply unknownprop_5f23a09617e395d3412bcd886825a830fcbca9dbfaa3bb762a6b0286bbba2699 with λ x2 x3 . TwoRamseyGraph_3_6_17 x3 (u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 1) ⟶ TwoRamseyGraph_3_6_17 u2 1.
Apply unknownprop_3ce04bff2a395cf5fe0b94d0636cc8dbea0e46272d1360d7109558a625b43849 with λ x2 x3 . TwoRamseyGraph_3_6_17 0 x3 ⟶ TwoRamseyGraph_3_6_17 u2 1.
Apply unknownprop_84aaefca7211a57d89e0df96a1f742653d3cc05f82d5ab568090ade3cb9ffcfd with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (0 ∈ u17 ⟶ u3 ∈ u17 ⟶ TwoRamseyGraph_3_6_Church17 x3 (u17_to_Church17 u3) = λ x4 x5 . x4) ⟶ TwoRamseyGraph_3_6_17 u2 u1.
Apply unknownprop_50de3f92839624b98789d3fa24556e40d38a727836b3c2bd366269421355b28d with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (0 ∈ u17 ⟶ u3 ∈ u17 ⟶ TwoRamseyGraph_3_6_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x4) x3 = λ x4 x5 . x4) ⟶ TwoRamseyGraph_3_6_17 u2 u1.
Assume H3: 0 ∈ u17 ⟶ u3 ∈ u17 ⟶ TwoRamseyGraph_3_6_Church17 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x5) = λ x2 x3 . x2.
Apply FalseE with TwoRamseyGraph_3_6_17 u2 u1.
Apply L0.
Apply H3 leaving 2 subgoals.
The subproof is completed by applying unknownprop_9851dfe301262128a9dc5def6f083cbb499c4d0eace7612e5dc050c4fe5ba3c7.
The subproof is completed by applying unknownprop_515e04c9d20f4760fa1f9ec9f7d43a79e2cf83cd96ac9929a00f63e10a33bee6.
Assume H2: x1 ∈ u3.
Apply cases_3 with x1, λ x2 . TwoRamseyGraph_3_6_17 (u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 u3) (u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 x2) ⟶ TwoRamseyGraph_3_6_17 u3 x2 leaving 4 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_2deda5cc0874f100e0fcd31fbab30140488390c1e46b9b2da484e79975ce6ae8 with λ x2 x3 . TwoRamseyGraph_3_6_17 x3 (u17_perm_1_3_0_2_5_7_4_6_10_8_11_9_13_14_15_12 0) ⟶ TwoRamseyGraph_3_6_17 u3 0.
Apply unknownprop_ddfd049a99d8a8d08a5969e20f08be40e16f962ab49dd05ba7dcd1cfd68e7645 with λ x2 x3 . TwoRamseyGraph_3_6_17 u2 x3 ⟶ TwoRamseyGraph_3_6_17 u3 0.
Apply unknownprop_7c154441ca7b7a9fe09539322ad6531c3f48333c7018e2f8c866c0af44719d1a with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (u2 ∈ u17 ⟶ u1 ∈ u17 ⟶ TwoRamseyGraph_3_6_Church17 x3 (u17_to_Church17 u1) = λ x4 x5 . x4) ⟶ TwoRamseyGraph_3_6_17 u3 0.
Apply unknownprop_f880a8473dab9f58d69fbf332c8547d500ca315e405258a93c99a34f8560efb6 with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (... ⟶ ... ⟶ TwoRamseyGraph_3_6_Church17 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 . x6) x3 = ...) ⟶ TwoRamseyGraph_3_6_17 u3 0.
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
■