Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ⊆ u6.
Assume H1: atleastp u4 x0.
Assume H2: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_3_6_17 x1 x2).
Apply unknownprop_19c5bea28ef119e30d80f4e7c578df826b34bc3d0b15978a12c7c1b896ec3046 with x0, False leaving 2 subgoals.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Assume H3: x1 ∈ x0.
Let x2 of type ι be given.
Assume H4: x2 ∈ x0.
Let x3 of type ι be given.
Assume H5: x3 ∈ x0.
Let x4 of type ι be given.
Assume H6: x4 ∈ x0.
Assume H7: x1 = x2 ⟶ ∀ x5 : ο . x5.
Assume H8: x1 = x3 ⟶ ∀ x5 : ο . x5.
Assume H9: x1 = x4 ⟶ ∀ x5 : ο . x5.
Assume H10: x2 = x3 ⟶ ∀ x5 : ο . x5.
Assume H11: x2 = x4 ⟶ ∀ x5 : ο . x5.
Assume H12: x3 = x4 ⟶ ∀ x5 : ο . x5.
Claim L13: ...
...
Claim L14: ...
...
Claim L15: ...
...
Claim L16: ...
...
Claim L17: ...
...
Claim L18: ...
...
Claim L19: ...
...
Claim L20: ...
...
Apply unknownprop_2ef847f21a2baf96dadf3ab4d4b77ea6805ffcf213b23d48a9ea8ad87b08dd22 with u17_to_Church17 x1, u17_to_Church17 x2, u17_to_Church17 x3, u17_to_Church17 x4 leaving 10 subgoals.
Apply unknownprop_a4d6616a55062492112fd37476b4f55594835ed1c157cbbc204bd9addd30d061 with x1.
Apply H0 with x1.
The subproof is completed by applying H3.
Apply unknownprop_a4d6616a55062492112fd37476b4f55594835ed1c157cbbc204bd9addd30d061 with x2.
Apply H0 with x2.
The subproof is completed by applying H4.
Apply unknownprop_a4d6616a55062492112fd37476b4f55594835ed1c157cbbc204bd9addd30d061 with x3.
Apply H0 with x3.
The subproof is completed by applying H5.
Apply unknownprop_a4d6616a55062492112fd37476b4f55594835ed1c157cbbc204bd9addd30d061 with x4.
Apply H0 with x4.
The subproof is completed by applying H6.
Apply unknownprop_46a7f5ba218e301f19d33cc265134a2df7adfd3de64e750dc665649ee8f6340d with u17_to_Church17 x1, u17_to_Church17 x2, TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (u17_to_Church17 x2) = λ x5 x6 . x6 leaving 4 subgoals.
The subproof is completed by applying L17.
The subproof is completed by applying L18.
Assume H21: TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (u17_to_Church17 x2) = λ x5 x6 . x5.
Apply FalseE with TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (u17_to_Church17 x2) = λ x5 x6 . x6.
Apply H2 with x1, x2 leaving 4 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H7.
Apply unknownprop_a3161c1a24da07bf7cb898b4bbdd6e6a1dad92a6ebaeb7b53200887c557936fb with x1, x2 leaving 3 subgoals.
The subproof is completed by applying L13.
The subproof is completed by applying L14.
The subproof is completed by applying H21.
Assume H21: TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (u17_to_Church17 x2) = λ x5 x6 . x6.
The subproof is completed by applying H21.
Apply unknownprop_46a7f5ba218e301f19d33cc265134a2df7adfd3de64e750dc665649ee8f6340d with u17_to_Church17 x1, u17_to_Church17 x3, TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (u17_to_Church17 x3) = λ x5 x6 . x6 leaving 4 subgoals.
The subproof is completed by applying L17.
The subproof is completed by applying L19.
Assume H21: TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (u17_to_Church17 x3) = λ x5 x6 . x5.
Apply FalseE with TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (u17_to_Church17 x3) = λ x5 x6 . x6.
Apply H2 with x1, x3 leaving 4 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying H8.
Apply unknownprop_a3161c1a24da07bf7cb898b4bbdd6e6a1dad92a6ebaeb7b53200887c557936fb with x1, x3 leaving 3 subgoals.
The subproof is completed by applying L13.
The subproof is completed by applying L15.
The subproof is completed by applying H21.
Assume H21: TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (u17_to_Church17 x3) = λ x5 x6 . x6.
The subproof is completed by applying H21.
Apply unknownprop_46a7f5ba218e301f19d33cc265134a2df7adfd3de64e750dc665649ee8f6340d with u17_to_Church17 x1, u17_to_Church17 x4, TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (u17_to_Church17 x4) = λ x5 x6 . x6 leaving 4 subgoals.
The subproof is completed by applying L17.
The subproof is completed by applying L20.
Assume H21: TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (u17_to_Church17 x4) = λ x5 x6 . x5.
Apply FalseE with TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (u17_to_Church17 x4) = λ x5 x6 . x6.
Apply H2 with x1, x4 leaving 4 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
The subproof is completed by applying H9.
Apply unknownprop_a3161c1a24da07bf7cb898b4bbdd6e6a1dad92a6ebaeb7b53200887c557936fb with x1, x4 leaving 3 subgoals.
The subproof is completed by applying L13.
The subproof is completed by applying L16.
The subproof is completed by applying H21.
Assume H21: TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x1) (u17_to_Church17 x4) = λ x5 x6 . x6.
The subproof is completed by applying H21.
Apply unknownprop_46a7f5ba218e301f19d33cc265134a2df7adfd3de64e750dc665649ee8f6340d with u17_to_Church17 x2, u17_to_Church17 x3, TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x2) (u17_to_Church17 x3) = λ x5 x6 . x6 leaving 4 subgoals.
The subproof is completed by applying L18.
The subproof is completed by applying L19.
Assume H21: TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x2) (u17_to_Church17 x3) = λ x5 x6 . x5.
Apply FalseE with TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x2) (u17_to_Church17 x3) = λ x5 x6 . x6.
Apply H2 with x2, x3 leaving 4 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H10.
Apply unknownprop_a3161c1a24da07bf7cb898b4bbdd6e6a1dad92a6ebaeb7b53200887c557936fb with x2, x3 leaving 3 subgoals.
The subproof is completed by applying L14.
The subproof is completed by applying L15.
The subproof is completed by applying H21.
Assume H21: TwoRamseyGraph_3_6_Church17 (u17_to_Church17 x2) ... = ....
...
...
...
■