Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: ...
...
Claim L1: ...
...
Claim L2: ...
...
Claim L3: ...
...
Claim L4: ...
...
Claim L5: ...
...
Claim L6: ...
...
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Claim L12: ...
...
Let x0 of type ι be given.
Assume H13: x0 ∈ u6.
Let x1 of type ι be given.
Assume H14: x1 ∈ u6.
Let x2 of type ι be given.
Assume H15: x2 ∈ u6.
Let x3 of type ι be given.
Assume H16: x3 ∈ u6.
Let x4 of type ι be given.
Assume H17: x4 ∈ u6.
Let x5 of type ι be given.
Assume H18: x5 ∈ u6.
Let x6 of type ι be given.
Assume H19: x6 ∈ u6.
Let x7 of type ι be given.
Assume H20: x7 ∈ u6.
Claim L21: ...
...
Claim L22: ...
...
Claim L23: ...
...
Claim L24: ...
...
Claim L25: ...
...
Claim L26: ...
...
Claim L27: ...
...
Claim L28: ...
...
Claim L29: ...
...
Claim L30: ...
...
Claim L31: ...
...
Claim L32: ...
...
Claim L33: ...
...
Claim L34: ...
...
Claim L35: ...
...
Claim L36: ...
...
Claim L37: ...
...
Claim L38: ...
...
Claim L39: ...
...
Claim L40: ...
...
Claim L41: ...
...
Claim L42: ...
...
Claim L43: ...
...
Claim L44: ...
...
Claim L45: ...
...
Claim L46: ...
...
Claim L47: ...
...
Claim L48: ...
...
Claim L49: ...
...
Claim L50: ...
...
Claim L51: ...
...
Claim L52: ...
...
Claim L53: ...
...
Claim L54: ...
...
Claim L55: ...
...
Claim L56: ...
...
Claim L57: ...
...
Claim L58: ...
...
Claim L59: ...
...
Claim L60: ...
...
Claim L61: ...
...
Claim L62: ...
...
Claim L63: ...
...
Claim L64: ...
...
Claim L65: ...
...
Claim L66: ...
...
Claim L67: ...
...
Claim L68: ...
...
Claim L69: ...
...
Claim L70: ...
...
Claim L71: ...
...
Claim L72: ...
...
Claim L73: ...
...
Claim L74: ...
...
Claim L75: ...
...
Claim L76: ...
...
Claim L77: ...
...
Claim L78: ...
...
Claim L79: ...
...
Claim L80: ...
...
Claim L81: ...
...
Claim L82: ...
...
Claim L83: ...
...
Claim L84: ...
...
Claim L85: ...
...
Claim L86: ...
...
Claim L87: ...
...
Claim L88: ...
...
Claim L89: ...
...
Claim L90: ...
...
Claim L91: ...
...
Claim L92: ...
...
Claim L93: ...
...
Claim L94: ...
...
Claim L95: ...
...
Claim L96: ...
...
Claim L97: ...
...
Claim L98: ...
...
Claim L99: ...
...
Claim L100: ...
...
Claim L101: ...
...
Claim L102: ...
...
Claim L103: ...
...
Claim L104: ...
...
Claim L105: ...
...
Claim L106: ...
...
Claim L107: ...
...
Claim L108: ...
...
Claim L109: ...
...
Claim L110: ...
...
Claim L111: ...
...
Claim L112: ...
...
Claim L113: ...
...
Claim L114: ...
...
Claim L115: ...
...
Claim L116: ...
...
Claim L117: ...
...
Claim L118: ...
...
Claim L119: ...
...
Claim L120: ...
...
Claim L121: ...
...
Claim L122: ...
...
Claim L123: ...
...
Claim L124: ...
...
Claim L125: ...
...
Claim L126: ...
...
Claim L127: ...
...
Claim L128: ...
...
Claim L129: ...
...
Claim L130: ...
...
Claim L131: ...
...
Claim L132: ...
...
Claim L133: ...
...
Claim L134: ...
...
Claim L135: ...
...
Claim L136: ...
...
Claim L137: ...
...
Claim L138: ...
...
Claim L139: ...
...
Claim L140: ...
...
Claim L141: ...
...
Claim L142: ...
...
Claim L143: ...
...
Claim L144: ...
...
Claim L145: ...
...
Claim L146: ...
...
Claim L147: ...
...
Claim L148: ...
...
Claim L149: ...
...
Claim L150: ...
...
Claim L151: ...
...
Claim L152: ...
...
Claim L153: ...
...
Claim L154: ...
...
Claim L155: ...
...
Claim L156: ...
...
Claim L157: ...
...
Claim L158: ...
...
Claim L159: ...
...
Claim L160: ...
...
Claim L161: ...
...
Claim L162: ...
...
Claim L163: ...
...
Claim L164: ...
...
Claim L165: ...
...
Claim L166: ...
...
Claim L167: ...
...
Claim L168: ...
...
Claim L169: ...
...
Claim L170: ...
...
Claim L171: ...
...
Claim L172: ...
...
Claim L173: ...
...
Claim L174: ...
...
Claim L175: ...
...
Claim L176: ...
...
Claim L177: ...
...
Claim L178: ...
...
Claim L179: ...
...
Claim L180: ...
...
Claim L181: ...
...
Claim L182: ...
...
Claim L183: ...
...
Claim L184: ...
...
Claim L185: ...
...
Claim L186: ...
...
Claim L187: ...
...
Claim L188: ...
...
Claim L189: ...
...
Claim L190: ...
...
Claim L191: ...
...
Claim L192: ...
...
Claim L193: ...
...
Claim L194: ...
...
Claim L195: ...
...
Claim L196: ...
...
Claim L197: ...
...
Claim L198: ...
...
Claim L199: ...
...
Claim L200: ...
...
Claim L201: ...
...
Claim L202: ...
...
Claim L203: ...
...
Claim L204: ...
...
Claim L205: ...
...
Claim L206: ...
...
Claim L207: ...
...
Claim L208: ...
...
Claim L209: ...
...
Claim L210: ...
...
Claim L211: ...
...
Claim L212: ...
...
Claim L213: ...
...
Claim L214: ...
...
Claim L215: ...
...
Claim L216: ...
...
Claim L217: ...
...
Claim L218: ...
...
Claim L219: ...
...
Claim L220: ...
...
Claim L221: ...
...
Claim L222: ...
...
Claim L223: ...
...
Claim L224: ...
...
Claim L225: ...
...
Claim L226: ...
...
Claim L227: not (TwoRamseyGraph_4_6_35_b u5 0 u5 u1)
Assume H227: TwoRamseyGraph_4_6_35_b u5 0 u5 u1.
Claim L228: TwoRamseyGraph_4_6_Church6_squared_b (λ x8 x9 x10 x11 x12 x13 . x13) (λ x8 x9 x10 x11 x12 x13 . x8) (λ x8 x9 x10 x11 x12 x13 . x13) (λ x8 x9 x10 x11 x12 x13 . x9) = λ x8 x9 . x8
Apply L7 with λ x8 x9 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_b (λ x10 x11 x12 x13 x14 x15 . x15) ... ... ... = ....
...
Apply L0.
The subproof is completed by applying L228.
Claim L228: not (TwoRamseyGraph_4_6_35_b u5 0 u5 u2)
Assume H228: TwoRamseyGraph_4_6_35_b u5 0 u5 u2.
Claim L229: TwoRamseyGraph_4_6_Church6_squared_b (λ x8 x9 x10 x11 x12 x13 . x13) (λ x8 x9 x10 x11 x12 x13 . x8) (λ x8 x9 x10 x11 x12 x13 . x13) (λ x8 x9 x10 x11 x12 x13 . x10) = λ x8 x9 . x8
Apply L7 with λ x8 x9 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_b (λ x10 x11 x12 x13 x14 x15 . x15) x8 (λ x10 x11 x12 x13 x14 x15 . x15) (λ x10 x11 x12 x13 x14 x15 . x12) = λ x10 x11 . x10.
Apply L12 with λ x8 x9 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_b x8 (nth_6_tuple 0) x8 (λ x10 x11 x12 x13 x14 x15 . x12) = λ x10 x11 . x10.
Apply L9 with λ x8 x9 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple u5) (nth_6_tuple 0) (nth_6_tuple u5) x8 = λ x10 x11 . x10.
Apply H228 leaving 4 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L1.
The subproof is completed by applying L6.
The subproof is completed by applying L3.
Apply L0.
The subproof is completed by applying L229.
Apply unknownprop_28d4afbfac484e2ed1baefa26bdba576308a319cae01b5e1fccec39c96be2681 with λ x8 . x8 ∈ u6, λ x8 . x8 ∈ u4, 0, u1, u2, u3, u4, u5, 9defa.., 247c9.., 3ffd5.., TwoRamseyGraph_4_6_35_b, x0, x1, x2, x3, x4, x5, x6, x7 leaving 231 subgoals.
The subproof is completed by applying L21.
The subproof is completed by applying In_0_6.
The subproof is completed by applying In_1_6.
The subproof is completed by applying In_2_6.
The subproof is completed by applying In_3_6.
The subproof is completed by applying In_4_6.
The subproof is completed by applying In_5_6.
The subproof is completed by applying In_0_4.
The subproof is completed by applying In_1_4.
The subproof is completed by applying In_2_4.
The subproof is completed by applying In_3_4.
The subproof is completed by applying L37.
The subproof is completed by applying L38.
The subproof is completed by applying L39.
The subproof is completed by applying L40.
The subproof is completed by applying L41.
The subproof is completed by applying L42.
The subproof is completed by applying L43.
The subproof is completed by applying L44.
The subproof is completed by applying L45.
The subproof is completed by applying L46.
The subproof is completed by applying L47.
The subproof is completed by applying L48.
The subproof is completed by applying L22.
The subproof is completed by applying L23.
The subproof is completed by applying L24.
The subproof is completed by applying L49.
The subproof is completed by applying L50.
The subproof is completed by applying L51.
The subproof is completed by applying unknownprop_50a8b7acb55ee7b60f2f005d925ff99b8fd7b14f24b56c6ce89157753015ec38.
The subproof is completed by applying unknownprop_036a822ac8f1a54700a58d95cdf87b77e4b11f25d54b16c95bd9551c21983920.
The subproof is completed by applying unknownprop_15732df45e168263b206e7a469ebd6fcac415981f88ad22f3c7d7f8e84a394f1.
The subproof is completed by applying unknownprop_a95c9e5f054be0de14ccc0ecef4dcac714fd92f9912712e6bb326c577d24c2b6.
The subproof is completed by applying unknownprop_10dc0bc1ebf9e7e58513344ad212af0379023035fe72a6868931ef03b8c907e6.
The subproof is completed by applying unknownprop_2aa9031b1e3b720d7641f55215d16d186362003042648ba71edb184f05901aa4.
The subproof is completed by applying unknownprop_ba6fefc3f771b5f91b58642a5f9ed93ca0b6a38aadb804ead9894da34e18c907.
The subproof is completed by applying unknownprop_a21fb392c034d21b64b1873cc259f0d1ef3f10bd0d1b4bb59f789f95cd63dbeb.
The subproof is completed by applying unknownprop_243a442c5e5863ccc918753807b1df3c8f09468de5b17fc1eb5ee94ffe009d6c.
The subproof is completed by applying unknownprop_2e96b86dfd897f1a18f1cbc67376985e9d9fe8658eb41e1e49e898c8eb88b7aa.
The subproof is completed by applying unknownprop_7152a75d0e9ce13cebedada570eeeb3defe2edf853c791c09a1b5910352b70fd.
The subproof is completed by applying unknownprop_535883424a9bcfdc4434b2918e57d79a585042b7e5b4d63379ab10876dae9dbe.
The subproof is completed by applying unknownprop_51b70d1c68a113e0fd13694548f2f36529dd299016e12694897ae861c30d4d24.
The subproof is completed by applying unknownprop_7291cb3ddfed5149e9fa3c9f69779e35ebc4b777f75c916d4359688142ae35c4.
The subproof is completed by applying unknownprop_9c8fe8f9fafda21f09bae1c2c95d40d01792e29b6a931d67569a1850a8f84915.
The subproof is completed by applying unknownprop_f1ebcb50105961924c6bcaded33bfbe7a175c59bafba670fe61ed3e2c8354dd7.
The subproof is completed by applying unknownprop_a1a4d376f704b11a42eebde0d2909eb2bce63b62a6be94a7d3f4f56805274c22.
The subproof is completed by applying L52.
The subproof is completed by applying L53.
The subproof is completed by applying L54.
The subproof is completed by applying L55.
The subproof is completed by applying L56.
The subproof is completed by applying L57.
The subproof is completed by applying L58.
The subproof is completed by applying L59.
The subproof is completed by applying L60.
The subproof is completed by applying L61.
The subproof is completed by applying L62.
The subproof is completed by applying L63.
The subproof is completed by applying L64.
The subproof is completed by applying L65.
The subproof is completed by applying L66.
The subproof is completed by applying L67.
The subproof is completed by applying L68.
The subproof is completed by applying L69.
The subproof is completed by applying L70.
The subproof is completed by applying L71.
The subproof is completed by applying L72.
The subproof is completed by applying L73.
The subproof is completed by applying L74.
The subproof is completed by applying L75.
The subproof is completed by applying L76.
The subproof is completed by applying L77.
The subproof is completed by applying L78.
The subproof is completed by applying L79.
The subproof is completed by applying L80.
The subproof is completed by applying L81.
The subproof is completed by applying L82.
The subproof is completed by applying L83.
The subproof is completed by applying L84.
The subproof is completed by applying L85.
The subproof is completed by applying L86.
The subproof is completed by applying L87.
The subproof is completed by applying L88.
The subproof is completed by applying L89.
The subproof is completed by applying L90.
The subproof is completed by applying L91.
The subproof is completed by applying L92.
The subproof is completed by applying L93.
The subproof is completed by applying L94.
The subproof is completed by applying L95.
The subproof is completed by applying L96.
The subproof is completed by applying L97.
The subproof is completed by applying L98.
The subproof is completed by applying L99.
The subproof is completed by applying L100.
The subproof is completed by applying L101.
The subproof is completed by applying L102.
The subproof is completed by applying L103.
The subproof is completed by applying L104.
The subproof is completed by applying L105.
The subproof is completed by applying L106.
The subproof is completed by applying L107.
The subproof is completed by applying L108.
The subproof is completed by applying L109.
The subproof is completed by applying L110.
The subproof is completed by applying L111.
The subproof is completed by applying L112.
The subproof is completed by applying L113.
The subproof is completed by applying L114.
The subproof is completed by applying L115.
The subproof is completed by applying L116.
The subproof is completed by applying L117.
The subproof is completed by applying L118.
The subproof is completed by applying L119.
The subproof is completed by applying L120.
The subproof is completed by applying L121.
The subproof is completed by applying L122.
The subproof is completed by applying L123.
The subproof is completed by applying L124.
The subproof is completed by applying L125.
The subproof is completed by applying L126.
The subproof is completed by applying L127.
The subproof is completed by applying L128.
The subproof is completed by applying L129.
The subproof is completed by applying L130.
The subproof is completed by applying L131.
The subproof is completed by applying L132.
The subproof is completed by applying L133.
The subproof is completed by applying L134.
The subproof is completed by applying L135.
The subproof is completed by applying L136.
The subproof is completed by applying L137.
The subproof is completed by applying L138.
The subproof is completed by applying L139.
The subproof is completed by applying L140.
The subproof is completed by applying L141.
The subproof is completed by applying L142.
The subproof is completed by applying L143.
The subproof is completed by applying L144.
The subproof is completed by applying L145.
The subproof is completed by applying L146.
The subproof is completed by applying L147.
The subproof is completed by applying L148.
The subproof is completed by applying L149.
The subproof is completed by applying L150.
The subproof is completed by applying L151.
The subproof is completed by applying L152.
The subproof is completed by applying L153.
The subproof is completed by applying L154.
The subproof is completed by applying L155.
The subproof is completed by applying L156.
The subproof is completed by applying L157.
The subproof is completed by applying L158.
The subproof is completed by applying L159.
The subproof is completed by applying L160.
The subproof is completed by applying L161.
The subproof is completed by applying L162.
The subproof is completed by applying L163.
The subproof is completed by applying L164.
The subproof is completed by applying L165.
The subproof is completed by applying L166.
The subproof is completed by applying L167.
The subproof is completed by applying L168.
The subproof is completed by applying L169.
The subproof is completed by applying L170.
The subproof is completed by applying L171.
The subproof is completed by applying L172.
The subproof is completed by applying L173.
The subproof is completed by applying L174.
The subproof is completed by applying L175.
The subproof is completed by applying L176.
The subproof is completed by applying L177.
The subproof is completed by applying L178.
The subproof is completed by applying L179.
The subproof is completed by applying L180.
The subproof is completed by applying L181.
The subproof is completed by applying L182.
The subproof is completed by applying L183.
The subproof is completed by applying L184.
The subproof is completed by applying L185.
The subproof is completed by applying L186.
The subproof is completed by applying L187.
The subproof is completed by applying L188.
The subproof is completed by applying L189.
The subproof is completed by applying L190.
The subproof is completed by applying L191.
The subproof is completed by applying L192.
The subproof is completed by applying L193.
The subproof is completed by applying L194.
The subproof is completed by applying L195.
The subproof is completed by applying L196.
The subproof is completed by applying L197.
The subproof is completed by applying L198.
The subproof is completed by applying L199.
The subproof is completed by applying L200.
The subproof is completed by applying L201.
The subproof is completed by applying L202.
The subproof is completed by applying L203.
The subproof is completed by applying L204.
The subproof is completed by applying L205.
The subproof is completed by applying L206.
The subproof is completed by applying L207.
The subproof is completed by applying L208.
The subproof is completed by applying L209.
The subproof is completed by applying L210.
The subproof is completed by applying L211.
The subproof is completed by applying L212.
The subproof is completed by applying L213.
The subproof is completed by applying L214.
The subproof is completed by applying L215.
The subproof is completed by applying L216.
The subproof is completed by applying L217.
The subproof is completed by applying L218.
The subproof is completed by applying L219.
The subproof is completed by applying L220.
The subproof is completed by applying L221.
The subproof is completed by applying L222.
The subproof is completed by applying L223.
The subproof is completed by applying L224.
The subproof is completed by applying L225.
The subproof is completed by applying L226.
The subproof is completed by applying L227.
The subproof is completed by applying L228.
The subproof is completed by applying H13.
The subproof is completed by applying H14.
The subproof is completed by applying H15.
The subproof is completed by applying H16.
The subproof is completed by applying H17.
The subproof is completed by applying H18.
The subproof is completed by applying H19.
The subproof is completed by applying H20.
■