Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ⊆ u24.
Assume H1: atleastp u4 x0.
Assume H2: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . x2 ∈ x0 ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ TwoRamseyGraph_4_5_24 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: ...
...
Apply unknownprop_71f021c030b388b031b0cb54393cd4b453c65667caa2e250dac00458eefad39c with x1, False leaving 2 subgoals.
Apply H0 with x1.
The subproof is completed by applying H3.
Let x5 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x6 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Assume H19: ChurchNum_3ary_proj_p x5.
Assume H20: ChurchNum_8ary_proj_p x6.
Assume H21: x1 = x5 (λ x7 : ι → ι . λ x8 . x8) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 x8)))))))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 (x7 x8)))))))))))))))) ordsucc (x6 (λ x7 : ι → ι . λ x8 . x8) (λ x7 : ι → ι . x7) (λ x7 : ι → ι . λ x8 . x7 (x7 x8)) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 x8))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 x8)))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 x8))))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 x8)))))) (λ x7 : ι → ι . λ x8 . x7 (x7 (x7 (x7 (x7 (x7 (x7 x8))))))) ordsucc 0).
Apply unknownprop_71f021c030b388b031b0cb54393cd4b453c65667caa2e250dac00458eefad39c with x2, False leaving 2 subgoals.
Apply H0 with x2.
The subproof is completed by applying H4.
Let x7 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x8 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Assume H22: ChurchNum_3ary_proj_p x7.
Assume H23: ChurchNum_8ary_proj_p x8.
Assume H24: x2 = x7 (λ x9 : ι → ι . λ x10 . x10) (λ x9 : ι → ι . λ x10 . x9 (x9 (x9 (x9 (x9 (x9 (x9 (x9 x10)))))))) (λ x9 : ι → ι . λ x10 . x9 (x9 (x9 (x9 (x9 (x9 (x9 (x9 (x9 (x9 (x9 (x9 (x9 (x9 (x9 (x9 x10)))))))))))))))) ordsucc (x8 (λ x9 : ι → ι . λ x10 . x10) (λ x9 : ι → ι . x9) (λ x9 : ι → ι . λ x10 . x9 (x9 x10)) (λ x9 : ι → ι . λ x10 . x9 (x9 (x9 x10))) (λ x9 : ι → ι . λ x10 . x9 (x9 (x9 (x9 x10)))) (λ x9 : ι → ι . λ x10 . x9 (x9 (x9 (x9 (x9 x10))))) (λ x9 : ι → ι . λ x10 . x9 (x9 (x9 (x9 ...)))) ... ... 0).
...
■