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: ...
...
Claim L13: ...
...
Claim L14: ...
...
Claim L15: ...
...
Claim L16: ...
...
Claim L17: ...
...
Claim L18: ...
...
Claim L19: ...
...
Claim L20: ...
...
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: ...
...
Claim L228: ...
...
Claim L229: ...
...
Claim L230: ...
...
Claim L231: ...
...
Claim L232: ...
...
Claim L233: ...
...
Claim L234: ...
...
Claim L235: ...
...
Claim L236: ...
...
Claim L237: ...
...
Claim L238: ...
...
Claim L239: ...
...
Claim L240: ...
...
Claim L241: ...
...
Claim L242: ...
...
Claim L243: ...
...
Claim L244: ...
...
Claim L245: ...
...
Claim L246: ...
...
Claim L247: ...
...
Claim L248: ...
...
Claim L249: ...
...
Claim L250: ...
...
Claim L251: ...
...
Claim L252: ...
...
Claim L253: ...
...
Claim L254: ...
...
Claim L255: ...
...
Claim L256: ...
...
Claim L257: ...
...
Claim L258: ...
...
Claim L259: ...
...
Claim L260: ...
...
Claim L261: ...
...
Claim L262: ...
...
Claim L263: ...
...
Claim L264: ...
...
Claim L265: ...
...
Claim L266: ...
...
Claim L267: ...
...
Claim L268: ...
...
Claim L269: ...
...
Claim L270: ...
...
Claim L271: ...
...
Claim L272: ...
...
Claim L273: ...
...
Claim L274: ...
...
Claim L275: ...
...
Claim L276: ...
...
Claim L277: TwoRamseyGraph_4_6_35_a u5 u4 u1 ...
...
Claim L278: TwoRamseyGraph_4_6_35_a u5 u4 u4 u5
Apply unknownprop_d3b792af1adffec16ce4fc340f1433694e312f9a299dc66e7bdd660386d0095e with λ x0 x1 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_a (nth_6_tuple u5) x1 x1 (nth_6_tuple u5) = λ x2 x3 . x2.
Apply unknownprop_d1ab6c05d827ab2f0497648eeb2e74b0b0260f4e004a74cbc06a5c0a175e4a2a with λ x0 x1 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_a x1 (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x6) x1 = λ x2 x3 . x2.
Let x0 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H278: x0 (TwoRamseyGraph_4_6_Church6_squared_a (λ x1 x2 x3 x4 x5 x6 . x6) (λ x1 x2 x3 x4 x5 x6 . x5) (λ x1 x2 x3 x4 x5 x6 . x5) (λ x1 x2 x3 x4 x5 x6 . x6)) (λ x1 x2 . x1).
The subproof is completed by applying H278.
Apply unknownprop_f27937bf94bfaa4b78a4045d5ca59fff96ebce7f0748a28a6dc13e15a688b220 with λ x0 . x0 ∈ u6, λ x0 . x0 ∈ u4, 0, u1, u2, u3, u4, u5, u6_squared_permutation__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5__1_0_3_2_4_5, u6_squared_permutation__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5__2_3_0_1_4_5, u6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5, In2_lexicographic, TwoRamseyGraph_4_6_35_a leaving 335 subgoals.
The subproof is completed by applying L13.
The subproof is completed by applying L14.
The subproof is completed by applying L15.
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 In_irref with u4.
Apply In_no2cycle with u4, u5.
The subproof is completed by applying In_4_5.
Apply neq_i_sym with u1, 0.
The subproof is completed by applying neq_1_0.
Apply neq_i_sym with u2, 0.
The subproof is completed by applying neq_2_0.
Apply neq_i_sym with u3, 0.
The subproof is completed by applying neq_3_0.
Apply neq_i_sym with u4, 0.
The subproof is completed by applying neq_4_0.
Apply neq_i_sym with u5, 0.
The subproof is completed by applying neq_5_0.
Apply neq_i_sym with u2, u1.
The subproof is completed by applying neq_2_1.
Apply neq_i_sym with u3, u1.
The subproof is completed by applying neq_3_1.
Apply neq_i_sym with u4, u1.
The subproof is completed by applying neq_4_1.
Apply neq_i_sym with u5, u1.
The subproof is completed by applying neq_5_1.
Apply neq_i_sym with u3, u2.
The subproof is completed by applying neq_3_2.
Apply neq_i_sym with u4, u2.
The subproof is completed by applying neq_4_2.
Apply neq_i_sym with u5, u2.
The subproof is completed by applying neq_5_2.
Apply neq_i_sym with u4, u3.
The subproof is completed by applying neq_4_3.
Apply neq_i_sym with u5, u3.
The subproof is completed by applying neq_5_3.
Apply neq_i_sym with u5, u4.
The subproof is completed by applying neq_5_4.
The subproof is completed by applying L17.
The subproof is completed by applying L18.
The subproof is completed by applying unknownprop_aa692ea1aa63eb15856af3e99748d802e7b0fa215a873b3d7a0eaf6c40dc14ee.
The subproof is completed by applying L19.
The subproof is completed by applying L20.
The subproof is completed by applying L21.
The subproof is completed by applying unknownprop_4d91bec054042bcdeefe33bb5a3d3611c13820c9f08314db2f8ef62923a83386.
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 unknownprop_1663e3943afde111e4661df41325166c466aef81ade0fce5108a3042fa43a66c.
The subproof is completed by applying L25.
The subproof is completed by applying unknownprop_6941479821a87bc0213525579f6079e2b0a19cf04ef701e5cf38bb698686b29c.
The subproof is completed by applying L27.
The subproof is completed by applying L16.
The subproof is completed by applying unknownprop_cdbc6277200ea99f7eefcbc0878b5c5c35ef86a6cae6f27f5a4a6562e338ad50.
The subproof is completed by applying unknownprop_c3b53ba05cb8a966e79bf7686d8a6d429b7a67f4133f758c77f7634030086a38.
The subproof is completed by applying unknownprop_daea222bde6599d08f3e1f080283f6d31c819e9d3fc672010019a0d512917af2.
The subproof is completed by applying unknownprop_3d8970394a902d267ed19d01ab818f977c770d7881a4d51a5d891efca480b273.
The subproof is completed by applying unknownprop_8a9776723da253f57832b2c3c265d876ce63c12fa6d67d3d8d5936dab1aab4e3.
The subproof is completed by applying unknownprop_45af0e5691a9cf52cd1ae085d0eece1b7e1ed1d45c8475957796d4d228b218ed.
The subproof is completed by applying unknownprop_8565bcc6d9a8ef91f6be6cf42caf6e272701035129050cd69fe5b21172dba186.
The subproof is completed by applying unknownprop_548e120db7c3ad799c85538d1da2c32a8b396a4e81330557d9fff3a0c19b04ef.
The subproof is completed by applying unknownprop_36c0d8bebb09370aca4fb2922f152f8cd3276f34e2b1edda8be238e293dea7fe.
The subproof is completed by applying unknownprop_4a4fca565643f72eb0ea67ce55df7321774bc922ef2062a3f305cdf2f3544b66.
The subproof is completed by applying unknownprop_d83ae45108d35e0fb327786fc6fe6f8e07c44e22d565943cac2638f55d6f5bd4.
The subproof is completed by applying unknownprop_a4165572a0e7f94ec68ad0de3bd2d67f3eda34597e66d4df7eb5bc04615eb969.
The subproof is completed by applying unknownprop_12c2d32d3b0a4d379bfd31bb4a06b3883d1dd755619c597c44c06bb975bd9467.
The subproof is completed by applying unknownprop_5053d8decba4824ece40f7eda6494874bc3aa6f8da6720b72135d5129b785480.
The subproof is completed by applying unknownprop_1345ff26ac618cf0478629cefa9923bbe00d06bb23ed2cb69ede78280057e4b6.
The subproof is completed by applying unknownprop_611dcd3b3d470e1006f1cce69705cb47963f241eef0bbee19351f9cc9ee88eca.
The subproof is completed by applying unknownprop_f04d41eb8e4f776924c78b479ba58135945070b176488f3e4fb4b1880369e3b9.
The subproof is completed by applying unknownprop_3f930481fcfac5229495a8bec7c52498133922a121da53552e66848c4086826d.
The subproof is completed by applying unknownprop_07322204153a256a98cb97a1e0c8f90b4215d6376cd0af872814e287dce96776.
The subproof is completed by applying unknownprop_33a6bc18cfd8d20cac3a782e72f02a1f3efbca4312e292180069e370e2ae77d7.
The subproof is completed by applying unknownprop_7abc2d954f30ac1710df169c03b40c811a40b48113e2a8b55f9d7198497f4c9f.
The subproof is completed by applying unknownprop_6ac6d7e93a50e964968a96f66a9aa9dc3778a58cb83309544cb39a85783128c4.
The subproof is completed by applying unknownprop_1c227da1eb8009dbe54d36a9388ac462e3233ad6cd6eda88206a777204ef6be9.
The subproof is completed by applying unknownprop_e76834dc137834cd33291ca0ba7620645922e4e84be041715b9165fc9f98ecec.
The subproof is completed by applying unknownprop_5eecaecea4203ee1bf240cb5f8d322e991cb60db8552b2499ebfec35cf4ee3c8.
The subproof is completed by applying unknownprop_12c43641953f27e0d07d13646ada34cbbe874fdf6c604d6f7022b856e5fc0bc2.
The subproof is completed by applying unknownprop_2a66f5e914e822d9f6f9be00d3f5d54d213d794d8fbbaf33681095fc49e1eadc.
The subproof is completed by applying unknownprop_1915c0dc993faeb7b859336416ffe186a7006116a2145adcee4874f59e0d51d7.
The subproof is completed by applying unknownprop_7ce91b6a4df38a83ada9bde6b949239d219d83702596c9d8033c185efc3692b8.
The subproof is completed by applying unknownprop_4a7a758742c7e66af2ccc47cd7d429a60bfbc2350bdfab3ca23160a2cf23b3ea.
The subproof is completed by applying unknownprop_8c0afb5e8c6029664390755a3ba7924a7cd35216a66abef2d1dd50cf115518a6.
The subproof is completed by applying unknownprop_4e1eedbd1c62a3475d65b5bd06b3af64f9b485605630aeab50afbee7f54f3d55.
The subproof is completed by applying unknownprop_d7d8ec59eecb06daee640d22d8b7e7d9116241b7a975bf6d1f70e8e7f75bb8ef.
The subproof is completed by applying unknownprop_816523af5b2f9c4a4dfbc601a160296b917c39869a3f5b34c23c007b5e7728f5.
The subproof is completed by applying unknownprop_7394a12a1d063faeceb656d0872dad1b273f4172b47c35b9985809b936edb369.
The subproof is completed by applying unknownprop_8901814c7f627f3098e85b81c2e8d38a1404335c801ee0854d6a9883502b02b1.
The subproof is completed by applying L26.
The subproof is completed by applying L31.
The subproof is completed by applying L32.
The subproof is completed by applying L33.
The subproof is completed by applying L28.
The subproof is completed by applying L29.
The subproof is completed by applying L30.
The subproof is completed by applying unknownprop_3977bf1090f933d3709f6b2041283bba6d87781a8eeab5f92047019ad110a939.
The subproof is completed by applying unknownprop_7cb93b98f252f18e4c77c51e548e5d9375b06b17a1739279bbecb77acb7c3a44.
The subproof is completed by applying L34.
The subproof is completed by applying L35.
The subproof is completed by applying L36.
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 L49.
The subproof is completed by applying L50.
The subproof is completed by applying L51.
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 L229.
The subproof is completed by applying L230.
The subproof is completed by applying L231.
The subproof is completed by applying L232.
The subproof is completed by applying L233.
The subproof is completed by applying L234.
The subproof is completed by applying L235.
The subproof is completed by applying L236.
The subproof is completed by applying L237.
The subproof is completed by applying L238.
The subproof is completed by applying L239.
The subproof is completed by applying L240.
The subproof is completed by applying L241.
The subproof is completed by applying L242.
The subproof is completed by applying L243.
The subproof is completed by applying L244.
The subproof is completed by applying L245.
The subproof is completed by applying L246.
The subproof is completed by applying L247.
The subproof is completed by applying L248.
The subproof is completed by applying L249.
The subproof is completed by applying L250.
The subproof is completed by applying L251.
The subproof is completed by applying L252.
The subproof is completed by applying L253.
The subproof is completed by applying L254.
The subproof is completed by applying L255.
The subproof is completed by applying L256.
The subproof is completed by applying L257.
The subproof is completed by applying L258.
The subproof is completed by applying L259.
The subproof is completed by applying L260.
The subproof is completed by applying L261.
The subproof is completed by applying L262.
The subproof is completed by applying L263.
The subproof is completed by applying L264.
The subproof is completed by applying L265.
The subproof is completed by applying L266.
The subproof is completed by applying L267.
The subproof is completed by applying L268.
The subproof is completed by applying L269.
The subproof is completed by applying L270.
The subproof is completed by applying L271.
The subproof is completed by applying L272.
The subproof is completed by applying L273.
The subproof is completed by applying L274.
The subproof is completed by applying L275.
The subproof is completed by applying L276.
The subproof is completed by applying L277.
The subproof is completed by applying L278.
■