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.
Assume H3: ∀ x0 x1 . TwoRamseyGraph_3_6_17_buggy x0 x1 ⟶ TwoRamseyGraph_3_6_17_buggy x1 x0.
Assume H4: ∀ x0 . x0 ⊆ u17 ⟶ atleastp u6 x0 ⟶ not (∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ not (TwoRamseyGraph_3_6_17_buggy x1 x2)).
Assume H5: TwoRamseyProp u3 u6 u17.
Apply unknownprop_f9aaf94a696a3a601361748669ef031543f893c9566c95130e38db730b2a265f leaving 6 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply TwoRamseyProp_atleastp_atleastp with u3, u3, u6, u6, u17 leaving 3 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying atleastp_ref with u3.
The subproof is completed by applying atleastp_ref with u6.
■