| pf |
|---|
Apply unknownprop_4e9860e22f2ecdaba8646193805e60c1a038ee0d6cc9eed40f0f2599b16dfd4b with λ x0 x1 . TwoRamseyProp u3 u6 (ordsucc (ordsucc x0)).
Apply unknownprop_8dc90256cd485c4892a87cecdc3cbbfe0b65eb0964cbc26ac7da8ca72ab39534 with u2, u5, u13, ... leaving 4 subgoals.
Apply unknownprop_c8da84824b954785d0aad3ac1cab3ea408afb6900e8ea9f4397c25652192285c with λ x0 x1 . TwoRamseyProp u4 u6 (ordsucc (ordsucc x0)).
Apply unknownprop_8dc90256cd485c4892a87cecdc3cbbfe0b65eb0964cbc26ac7da8ca72ab39534 with u3, u5, u31, u19 leaving 4 subgoals.
The subproof is completed by applying unknownprop_723dd01f4e3b6ead0b114b6935717dcf3e97da79c873ecf977038ff266453fe1.
The subproof is completed by applying unknownprop_fac4bbb30ad81b6694b16257f5c78aca84fe44aabf82317cc19fcd45abcf1690.
The subproof is completed by applying TwoRamseyProp_u4_u5_u32.
The subproof is completed by applying L0.
Apply unknownprop_e48038bdec8e7884f08fd52a2588c05eed836ce7446f23174fba0b8b623ea2b3 with λ x0 x1 . TwoRamseyProp (ordsucc u2) (ordsucc u6) (ordsucc (ordsucc x0)).
Apply unknownprop_8dc90256cd485c4892a87cecdc3cbbfe0b65eb0964cbc26ac7da8ca72ab39534 with u2, u6, u19, u6 leaving 4 subgoals.
The subproof is completed by applying unknownprop_fac4bbb30ad81b6694b16257f5c78aca84fe44aabf82317cc19fcd45abcf1690.
The subproof is completed by applying nat_6.
The subproof is completed by applying L0.
The subproof is completed by applying unknownprop_0b333a54acf90ac2cb68915649df7a73a736b590f76b23b6e0e8b35fbb9faf0c with ordsucc u6.
Apply unknownprop_8dc90256cd485c4892a87cecdc3cbbfe0b65eb0964cbc26ac7da8ca72ab39534 with u3, u6, u51, u26 leaving 4 subgoals.
The subproof is completed by applying unknownprop_0e4f7f5019dd72cad77d235851aaa5f40639940cef2c896847b5850af4193769.
The subproof is completed by applying unknownprop_289054093170089dbe39b1d15aa65cd476b1f9d33d6fb8e39a1c75742ce9ba86.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
Apply unknownprop_7d33043cc623769ebdb44921901a824067184ba53aea51df2a9e6b184cd6f0a0 with λ x0 x1 . TwoRamseyProp (ordsucc u2) (ordsucc u7) (ordsucc (ordsucc x0)).
Apply unknownprop_8dc90256cd485c4892a87cecdc3cbbfe0b65eb0964cbc26ac7da8ca72ab39534 with u2, u7, u26, u7 leaving 4 subgoals.
The subproof is completed by applying unknownprop_289054093170089dbe39b1d15aa65cd476b1f9d33d6fb8e39a1c75742ce9ba86.
The subproof is completed by applying nat_7.
The subproof is completed by applying L2.
The subproof is completed by applying unknownprop_0b333a54acf90ac2cb68915649df7a73a736b590f76b23b6e0e8b35fbb9faf0c with u8.
Apply unknownprop_8dc90256cd485c4892a87cecdc3cbbfe0b65eb0964cbc26ac7da8ca72ab39534 with u3, u7, ordsucc (add_nat u51 u26), u34 leaving 4 subgoals.
Apply nat_ordsucc with add_nat u51 u26.
Apply add_nat_p with u51, u26 leaving 2 subgoals.
The subproof is completed by applying unknownprop_0e4f7f5019dd72cad77d235851aaa5f40639940cef2c896847b5850af4193769.
The subproof is completed by applying unknownprop_289054093170089dbe39b1d15aa65cd476b1f9d33d6fb8e39a1c75742ce9ba86.
The subproof is completed by applying unknownprop_3dad49cdb0b46d482652f9ab64d8695df650b7c7dfa1daf758686cc12275038b.
The subproof is completed by applying L3.
The subproof is completed by applying L4.
Apply add_nat_SR with u51, u26, λ x0 x1 . atleastp (ordsucc (ordsucc (add_nat x0 u34))) (prim4 u7) leaving 2 subgoals.
The subproof is completed by applying unknownprop_289054093170089dbe39b1d15aa65cd476b1f9d33d6fb8e39a1c75742ce9ba86.
Apply add_nat_asso with u51, u27, u34, λ x0 x1 . atleastp (ordsucc (ordsucc x1)) (prim4 u7) leaving 4 subgoals.
The subproof is completed by applying unknownprop_0e4f7f5019dd72cad77d235851aaa5f40639940cef2c896847b5850af4193769.
The subproof is completed by applying unknownprop_f5b8583d73a2efa339efab10375e1f72c07bd63d6625dbe8cc0533691448c99e.
The subproof is completed by applying unknownprop_3dad49cdb0b46d482652f9ab64d8695df650b7c7dfa1daf758686cc12275038b.
Apply add_nat_SR with u27, u33, λ x0 x1 . atleastp (ordsucc (ordsucc (add_nat u51 x1))) (prim4 u7) leaving 2 subgoals.
The subproof is completed by applying unknownprop_176b77e9dd5a04af2e6894f4be5e1bdf5368375bafa51d5f0b9802d23d85e4bf.
Apply add_nat_SR with u27, u32, λ x0 x1 . atleastp (ordsucc (ordsucc (add_nat u51 (ordsucc x1)))) (prim4 u7) leaving 2 subgoals.
The subproof is completed by applying unknownprop_e20297641bb65d9e51ebac2e053948365a3f53b65d223d41920ce90b2e26b533.
Apply add_nat_SR with u27, u31, λ x0 x1 . atleastp (ordsucc (ordsucc (add_nat u51 (ordsucc (ordsucc x1))))) (prim4 u7) leaving 2 subgoals.
The subproof is completed by applying unknownprop_723dd01f4e3b6ead0b114b6935717dcf3e97da79c873ecf977038ff266453fe1.
Apply add_nat_com with u27, u31, λ x0 x1 . atleastp (ordsucc (ordsucc (add_nat u51 (ordsucc (ordsucc (ordsucc x1)))))) (prim4 u7) leaving 3 subgoals.
The subproof is completed by applying unknownprop_f5b8583d73a2efa339efab10375e1f72c07bd63d6625dbe8cc0533691448c99e.
The subproof is completed by applying unknownprop_723dd01f4e3b6ead0b114b6935717dcf3e97da79c873ecf977038ff266453fe1.
Apply unknownprop_788bbe9828a92e5a00088dfb2b8bda376a1f0cc6f5af9d051630bf10267ff3d7 with λ x0 x1 . atleastp (ordsucc (ordsucc (add_nat u51 (ordsucc (ordsucc (ordsucc x1)))))) (prim4 u7).
Apply add_nat_SR with u51, u61, λ x0 x1 . atleastp (ordsucc x0) (prim4 u7) leaving 2 subgoals.
The subproof is completed by applying unknownprop_fcd025a00bb7da23d97680c00d0033d2906ef1fea03d4d71234a6087585458e3.
Apply add_nat_SR with u51, u62, λ x0 x1 . atleastp x0 (prim4 u7) leaving 2 subgoals.
The subproof is completed by applying unknownprop_dd71b54e44a69b22b3c4f0693e5dd13038fd58ca7849918338011816a552e7ad.
Apply atleastp_tra with add_nat u51 u63, exp_nat u2 u7, prim4 u7 leaving 2 subgoals.
Apply Subq_atleastp with add_nat u51 u63, exp_nat u2 (ordsucc u6).
The subproof is completed by applying unknownprop_8d767625c7188cac3f67da81f68e6dc32bb0713dfc32b751af8be4b3bff7bce3.
Apply equip_atleastp with exp_nat u2 u7, prim4 u7.
Apply equip_sym with prim4 u7, exp_nat u2 u7.
Apply unknownprop_f5822e9d5891900b4c653eab5e89c5bb71543e61fe2c332750489ecd340604eb with u7.
The subproof is completed by applying nat_7.
■ |
|