Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο be given.
Assume H0: x0 Church10_0 Church10_1.
Assume H1: x0 Church10_0 Church10_2.
Assume H2: x0 Church10_1 Church10_2.
Assume H3: x0 Church10_0 Church10_3.
Assume H4: x0 Church10_1 Church10_3.
Assume H5: x0 Church10_2 Church10_3.
Assume H6: x0 Church10_0 Church10_4.
Assume H7: x0 Church10_1 Church10_4.
Assume H8: x0 Church10_2 Church10_4.
Assume H9: x0 Church10_3 Church10_4.
Assume H10: x0 Church10_0 Church10_5.
Assume H11: x0 Church10_1 Church10_5.
Assume H12: x0 Church10_2 Church10_5.
Assume H13: x0 Church10_3 Church10_5.
Assume H14: x0 Church10_4 Church10_5.
Assume H15: x0 Church10_0 Church10_6.
Assume H16: x0 Church10_1 Church10_6.
Assume H17: x0 Church10_2 Church10_6.
Assume H18: x0 Church10_3 Church10_6.
Assume H19: x0 Church10_4 Church10_6.
Assume H20: x0 Church10_5 Church10_6.
Assume H21: x0 Church10_0 Church10_7.
Assume H22: x0 Church10_1 Church10_7.
Assume H23: x0 Church10_2 Church10_7.
Assume H24: x0 Church10_3 Church10_7.
Assume H25: x0 Church10_4 Church10_7.
Assume H26: x0 Church10_5 Church10_7.
Assume H27: x0 Church10_6 Church10_7.
Assume H28: x0 Church10_0 Church10_8.
Assume H29: x0 Church10_1 Church10_8.
Assume H30: x0 Church10_2 Church10_8.
Assume H31: x0 Church10_3 Church10_8.
Assume H32: x0 Church10_4 Church10_8.
Assume H33: x0 Church10_5 Church10_8.
Assume H34: x0 Church10_6 Church10_8.
Assume H35: x0 Church10_7 Church10_8.
Assume H36: x0 Church10_0 Church10_9.
Assume H37: x0 Church10_1 Church10_9.
Assume H38: x0 Church10_2 Church10_9.
Assume H39: x0 Church10_3 Church10_9.
Assume H40: x0 Church10_4 Church10_9.
Assume H41: x0 Church10_5 Church10_9.
Assume H42: x0 Church10_6 Church10_9.
Assume H43: x0 Church10_7 Church10_9.
Assume H44: x0 Church10_8 Church10_9.
Apply unknownprop_11278145386dd85f714f31121ec2805e154e2e3ecae4d7cd701d70d0cf5007ab with x0 Church10_0 Church10_1, and (x0 Church10_0 Church10_2) (x0 Church10_1 Church10_2), and (and (x0 Church10_0 Church10_3) (x0 Church10_1 Church10_3)) (x0 Church10_2 Church10_3), and (and (and (x0 Church10_0 Church10_4) (x0 Church10_1 Church10_4)) (x0 Church10_2 Church10_4)) (x0 Church10_3 Church10_4), and (and (and (and (x0 Church10_0 Church10_5) (x0 Church10_1 Church10_5)) (x0 Church10_2 Church10_5)) (x0 Church10_3 Church10_5)) (x0 Church10_4 Church10_5), and (and (and (and (and (x0 Church10_0 Church10_6) (x0 Church10_1 Church10_6)) (x0 Church10_2 Church10_6)) (x0 Church10_3 Church10_6)) (x0 Church10_4 Church10_6)) (x0 Church10_5 Church10_6), and (and (and (and (and (and (x0 Church10_0 Church10_7) (x0 Church10_1 Church10_7)) (x0 Church10_2 Church10_7)) (x0 Church10_3 ...)) ...) ...) ..., ..., ... leaving 9 subgoals.
...
...
...
...
...
...
...
...
...
■