| pf |
|---|
Apply add_nat_SR with u51, u26, λ x0 x1 . atleastp (ordsucc (ordsucc (add_nat (ordsucc (add_nat x0 u34)) u43))) (prim4 u8) leaving 2 subgoals.
The subproof is completed by applying unknownprop_289054093170089dbe39b1d15aa65cd476b1f9d33d6fb8e39a1c75742ce9ba86.
Apply add_nat_asso with u51, u27, u34, λ x0 x1 . atleastp (ordsucc (ordsucc (add_nat (ordsucc x1) u43))) (prim4 u8) 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 (ordsucc (add_nat u51 x1)) u43))) (prim4 u8) 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 (ordsucc (add_nat u51 (ordsucc x1))) u43))) (prim4 u8) 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 (ordsucc (add_nat u51 (ordsucc (ordsucc x1)))) u43))) (prim4 u8) 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 (ordsucc (add_nat u51 (ordsucc (ordsucc (ordsucc x1))))) u43))) (prim4 u8) 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 (ordsucc (add_nat u51 (ordsucc (ordsucc (ordsucc x1))))) u43))) (prim4 u8).
Apply add_nat_SR with u51, u61, λ x0 x1 . atleastp (ordsucc (ordsucc (add_nat x0 u43))) (prim4 u8) leaving 2 subgoals.
The subproof is completed by applying unknownprop_fcd025a00bb7da23d97680c00d0033d2906ef1fea03d4d71234a6087585458e3.
Apply add_nat_SL with add_nat u51 u62, u43, λ x0 x1 . atleastp (ordsucc x0) (prim4 u8) leaving 3 subgoals.
Apply add_nat_p with u51, u62 leaving 2 subgoals.
The subproof is completed by applying unknownprop_0e4f7f5019dd72cad77d235851aaa5f40639940cef2c896847b5850af4193769.
The subproof is completed by applying unknownprop_dd71b54e44a69b22b3c4f0693e5dd13038fd58ca7849918338011816a552e7ad.
The subproof is completed by applying unknownprop_d01ba0648b928568932ea85770d1b477f11e878008abbd9eb9f158692f5b4774.
Apply add_nat_SR with u51, u62, λ x0 x1 . atleastp (ordsucc (add_nat x0 u43)) (prim4 u8) leaving 2 subgoals.
The subproof is completed by applying unknownprop_dd71b54e44a69b22b3c4f0693e5dd13038fd58ca7849918338011816a552e7ad.
Apply add_nat_SR with add_nat u51 u63, u43, λ x0 x1 . atleastp x0 (prim4 u8) leaving 2 subgoals.
The subproof is completed by applying unknownprop_d01ba0648b928568932ea85770d1b477f11e878008abbd9eb9f158692f5b4774.
Apply atleastp_tra with add_nat (add_nat u51 u63) u44, exp_nat u2 u8, prim4 u8 leaving 2 subgoals.
Apply Subq_atleastp with add_nat (add_nat u51 u63) u44, exp_nat u2 u8.
Apply unknownprop_e9c4cec7fb327dcb17b88acdaf76daee024e49fa71834a13065f86e12e958609 with u2, u7, λ x0 x1 . add_nat (add_nat u51 u63) u44 ⊆ x1 leaving 2 subgoals.
The subproof is completed by applying nat_7.
Apply unknownprop_463ff37e0f5b1f0c9f9e5bd24ebf02eb01188a79277f3c1f714af19504beaaf2 with exp_nat u2 u7, λ x0 x1 . add_nat (add_nat u51 u63) u44 ⊆ x1 leaving 2 subgoals.
Apply unknownprop_1b73e01bc234ba0e318bc9baf16604d4f0fc12bea57885439d70438de4eb7174 with u2, u7 leaving 2 subgoals.
The subproof is completed by applying nat_2.
The subproof is completed by applying nat_7.
Apply unknownprop_f15668f9dd126ccb5aaf8475e840ca53cc6e13458c80098a365679d1ec8b61cb with add_nat u51 u63, u44, exp_nat u2 u7, exp_nat u2 u7 leaving 6 subgoals.
Apply add_nat_p with u51, u63 leaving 2 subgoals.
The subproof is completed by applying unknownprop_0e4f7f5019dd72cad77d235851aaa5f40639940cef2c896847b5850af4193769.
The subproof is completed by applying unknownprop_1bb5d644e46edf4d7f31f818c9ba84409d227e8fe01f3cebddc2e7a46ab7177a.
The subproof is completed by applying unknownprop_a7846785c80d257e26f332679b1749824b21b7b8082e0deabed938cf8bd1a141.
Apply unknownprop_1b73e01bc234ba0e318bc9baf16604d4f0fc12bea57885439d70438de4eb7174 with u2, u7 leaving 2 subgoals.
The subproof is completed by applying nat_2.
The subproof is completed by applying nat_7.
Apply unknownprop_1b73e01bc234ba0e318bc9baf16604d4f0fc12bea57885439d70438de4eb7174 with u2, u7 leaving 2 subgoals.
The subproof is completed by applying nat_2.
The subproof is completed by applying nat_7.
The subproof is completed by applying unknownprop_8d767625c7188cac3f67da81f68e6dc32bb0713dfc32b751af8be4b3bff7bce3.
Apply unknownprop_e9c4cec7fb327dcb17b88acdaf76daee024e49fa71834a13065f86e12e958609 with u2, u6, λ x0 x1 . u44 ⊆ x1 leaving 2 subgoals.
The subproof is completed by applying nat_6.
Apply unknownprop_4d619f8c0c4edc98bd8e6be92366236784a59ad7862cae98bda091f9d44c9792 with λ x0 x1 . u44 ⊆ mul_nat u2 x1.
Apply unknownprop_463ff37e0f5b1f0c9f9e5bd24ebf02eb01188a79277f3c1f714af19504beaaf2 with u64, λ x0 x1 . u44 ⊆ x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_c00f2f77a9de84adbe221e2db786f0dbccd295ee08ec6eb8eaaf0b0a862ad5bd.
Apply add_nat_0R with u44, λ x0 x1 . x0 ⊆ add_nat u64 u64.
Apply unknownprop_f15668f9dd126ccb5aaf8475e840ca53cc6e13458c80098a365679d1ec8b61cb with u44, 0, u64, u64 leaving 6 subgoals.
■ |
|