Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: ∀ x0 . x0 ∈ u17 ⟶ Church17_p (u17_to_Church17_buggy x0).
Assume H1: ∀ x0 . x0 ∈ u17 ⟶ ∀ x1 . x1 ∈ u17 ⟶ u17_to_Church17_buggy x0 = u17_to_Church17_buggy x1 ⟶ x0 = x1.
Assume H2: ∀ x0 x1 x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ Church17_p x2 ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (TwoRamseyGraph_3_6_Church17 x0 x1 = λ x3 x4 . x3) ⟶ (TwoRamseyGraph_3_6_Church17 x0 x2 = λ x3 x4 . x3) ⟶ (TwoRamseyGraph_3_6_Church17 x1 x2 = λ x3 x4 . x3) ⟶ False.
Let x0 of type ι be given.
Assume H3: x0 ⊆ u17.
Assume H4: atleastp u3 x0.
Assume H5: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ TwoRamseyGraph_3_6_17_buggy x1 x2.
Apply unknownprop_95c6cbd2308b27a7edcd2a1d9389b377988e902d740d05dc7c88e6b8da945ab9 with x0, False leaving 2 subgoals.
The subproof is completed by applying H4.
Let x1 of type ι be given.
Assume H6: x1 ∈ x0.
Let x2 of type ι be given.
Assume H7: x2 ∈ x0.
Let x3 of type ι be given.
Assume H8: x3 ∈ x0.
Assume H9: x1 = x2 ⟶ ∀ x4 : ο . x4.
Assume H10: x1 = x3 ⟶ ∀ x4 : ο . x4.
Assume H11: x2 = x3 ⟶ ∀ x4 : ο . x4.
Claim L12: x1 ∈ u17
Apply H3 with x1.
The subproof is completed by applying H6.
Claim L13: x2 ∈ u17
Apply H3 with x2.
The subproof is completed by applying H7.
Claim L14: x3 ∈ u17
Apply H3 with x3.
The subproof is completed by applying H8.
Claim L15: TwoRamseyGraph_3_6_Church17 (u17_to_Church17_buggy x1) (u17_to_Church17_buggy x2) = λ x4 x5 . x4
Apply H5 with x1, x2 leaving 5 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
The subproof is completed by applying H9.
The subproof is completed by applying L12.
The subproof is completed by applying L13.
Claim L16: TwoRamseyGraph_3_6_Church17 (u17_to_Church17_buggy x2) (u17_to_Church17_buggy x3) = λ x4 x5 . x4
Apply H5 with x2, x3 leaving 5 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H11.
The subproof is completed by applying L13.
The subproof is completed by applying L14.
Claim L17: TwoRamseyGraph_3_6_Church17 (u17_to_Church17_buggy x1) (u17_to_Church17_buggy x3) = λ x4 x5 . x4
Apply H5 with x1, x3 leaving 5 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying H8.
The subproof is completed by applying H10.
The subproof is completed by applying L12.
The subproof is completed by applying L14.
Claim L18: u17_to_Church17_buggy x1 = u17_to_Church17_buggy x2 ⟶ ∀ x4 : ο . x4
Assume H18: u17_to_Church17_buggy x1 = u17_to_Church17_buggy x2.
Apply H9.
Apply H1 with x1, x2 leaving 3 subgoals.
The subproof is completed by applying L12.
The subproof is completed by applying L13.
The subproof is completed by applying H18.
Claim L19: u17_to_Church17_buggy x1 = u17_to_Church17_buggy x3 ⟶ ∀ x4 : ο . x4
Assume H19: u17_to_Church17_buggy x1 = u17_to_Church17_buggy x3.
Apply H10.
Apply H1 with x1, x3 leaving 3 subgoals.
The subproof is completed by applying L12.
The subproof is completed by applying L14.
The subproof is completed by applying H19.
Claim L20: u17_to_Church17_buggy x2 = u17_to_Church17_buggy x3 ⟶ ∀ x4 : ο . x4
Assume H20: u17_to_Church17_buggy x2 = u17_to_Church17_buggy x3.
Apply H11.
Apply H1 with x2, x3 leaving 3 subgoals.
The subproof is completed by applying L13.
The subproof is completed by applying L14.
The subproof is completed by applying H20.
Apply H2 with u17_to_Church17_buggy x1, u17_to_Church17_buggy x2, u17_to_Church17_buggy x3 leaving 9 subgoals.
Apply H0 with x1.
The subproof is completed by applying L12.
Apply H0 with x2.
The subproof is completed by applying L13.
Apply H0 with x3.
The subproof is completed by applying L14.
The subproof is completed by applying L18.
The subproof is completed by applying L19.
The subproof is completed by applying L20.
The subproof is completed by applying L15.
The subproof is completed by applying L17.
The subproof is completed by applying L16.
■