Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: TwoRamseyGraph_4_5_24 x0 x1.
Let x2 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x3 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x4 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Let x5 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.
Assume H1: ChurchNum_3ary_proj_p x2.
Assume H2: ChurchNum_3ary_proj_p x3.
Assume H3: ChurchNum_8ary_proj_p x4.
Assume H4: ChurchNum_8ary_proj_p x5.
Assume H5: x1 = x2 (λ x6 : ι → ι . λ x7 . x7) (λ x6 : ι → ι . λ x7 . x6 (x6 (x6 (x6 (x6 (x6 (x6 (x6 x7)))))))) (λ x6 : ι → ι . λ x7 . x6 (x6 (x6 (x6 (x6 (x6 (x6 (x6 (x6 (x6 (x6 (x6 (x6 (x6 (x6 (x6 x7)))))))))))))))) ordsucc (x4 (λ x6 : ι → ι . λ x7 . x7) (λ x6 : ι → ι . x6) (λ x6 : ι → ι . λ x7 . x6 (x6 x7)) (λ x6 : ι → ι . λ x7 . x6 (x6 (x6 x7))) (λ x6 : ι → ι . λ x7 . x6 (x6 (x6 (x6 x7)))) (λ x6 : ι → ι . λ x7 . x6 (x6 (x6 (x6 (x6 x7))))) (λ x6 : ι → ι . λ x7 . x6 (x6 (x6 (x6 (x6 (x6 x7)))))) (λ x6 : ι → ι . λ x7 . x6 (x6 (x6 (x6 (x6 (x6 (x6 x7))))))) ordsucc 0).
Assume H6: x0 = x3 (λ x6 : ι → ι . λ x7 . x7) (λ x6 : ι → ι . λ x7 . x6 (x6 (x6 (x6 (x6 (x6 (x6 (x6 x7)))))))) (λ x6 : ι → ι . λ x7 . x6 (x6 (x6 (x6 (x6 (x6 (x6 (x6 (x6 (x6 (x6 (x6 (x6 (x6 (x6 (x6 x7)))))))))))))))) ordsucc (x5 (λ x6 : ι → ι . λ x7 . x7) (λ x6 : ι → ι . x6) (λ x6 : ι → ι . λ x7 . x6 (x6 x7)) (λ x6 : ι → ι . λ x7 . x6 (x6 (x6 x7))) (λ x6 : ι → ι . λ x7 . x6 (x6 (x6 (x6 x7)))) (λ x6 : ι → ι . λ x7 . x6 (x6 (x6 (x6 (x6 x7))))) (λ x6 : ι → ι . λ x7 . x6 (x6 (x6 (x6 (x6 (x6 x7)))))) (λ x6 : ι → ι . λ x7 . x6 (x6 (x6 (x6 (x6 (x6 (x6 x7))))))) ordsucc 0).
Apply unknownprop_181a8ee5dd2d442dca537df686e4f4d3c055613608d0b734890d85952682b94f with x2, x3, x4, x5, λ x6 x7 : ι → ι → ι . x7 = λ x8 x9 . x8 leaving 5 subgoals.
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 H0 with x3, x2, x5, x4 leaving 6 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
The subproof is completed by applying H3.
The subproof is completed by applying H6.
The subproof is completed by applying H5.
■