Hi Jon, Here's a proof <https://mmproofassistant.azurewebsites.net/#eJzVXeuS4riSfpWK+lUd3dVrS7YuHdEnoqsmJmI34jzBnPlhjMEYYxtsA2a2331lLlZaiART9Nk5MzE1QFGZX16USqVS8l/PsypalM/f/nom0yYnC1YE7ZuqKaLnb89pMIrS5y/PRbCKsur5W1an6ZfnsgrUH+0/eJ7M0lnhjdV3ZmP1VhP58pzmwXiWTZ+/TYK0jH5+ed41WbgppjIBHMZRGa5mRTXLM5TPy3ueVavZqK6i8dOoefry5MrX/6nTV+IQ5+unE3/NQvFb1NUyyhcbD/CLmyKv4qiclTi7pyJ+ev3H04+n6OvT+/tTx0DTPPxBrXT3nBdR1jKcTDeKelCOAMNpHuAaPLF6Ucy+P7lP//Wvfz29qVfk6dOebV+NX57DPE2DoozG3Sd7YJq3BVgUNtnaI159vybeTE1omhaGdOM1oROv+f0MW318Vmw/KV1QzVZTtrAt43Ds8XDrfITti2K3/aq4f1L8X5Qd1JsWRguEayCalwWIt0m4K0bVBgCpgrCahQDEmc1OWP744+l/X59OiIpSsQbvw1i9//NP+NFL+6XWcfa/+/T011/tq29HP/r5s/2gaD9QP47vSvXu4HA/f7Zeth/p356TMDgJqGUwBfzyvA7SWsnkfHU8KiilQgjCuZBCKOHzJi4mvmCTy8PgjPj5wGuhDfB/zdRijnGcRv6u9uIPIDqOydsRaaYWRKNtTn2eTBPUQUyh7A7S6uqt7yMt2PczN/lx/FTZ/8fe/AdfeFevXauXvKk3L8rpX0/jQA/K9t+e50TLatXNA1o8zHcIcRzPZZ7j+tzhjs+VYmaV3BWzKNkhpjKp25wHgT3AhhqNxYbppgiXspmnH4CKwBw4ADQaWzyaNl7kzYMp6m4mice6G+pIA/2QXvE/LS/mfz5xXUaYw1yH+q5kSlFzj85JHC5zLFIYxAfZ1CLGACNreBYjZyKcz0nSbB6Fnd7jhxqFBWLT0GI2mjoZ6oemlLgfmlPh+9Pv+8n7+/H122lKPDjhmVWgi3Via4/kx9e/q9evZ94JHDBfR0vSeaCWFPFA6UghJfHVD9/j3FMamvpBniW+SxEjmrTPjXgm5PeeTW+3poZjsWbgZWtCa79ErWmSeKg1TxJqI1JgOwJsp2S/2XhaMMx40icekVyq4EE94rYrHObOwjTb4mmfOUKuhtlDeL09uNIzv25/ya4EWqCNsklZtOwWVZ1UiDaISgSJ9H1CHeKrXFC266FJso6TKCkQXzaJ3xSQtEBDVkgdGosrF0mcrEUswrugntCoUHk7Hs3SgmdW7PLRnIUTfAFhiPT4QEl7jsQ+Hhe1YIgzMcodyqgriO8wLtq4OKmdLY02hCMGMmlfiIt0LzMb5Dsdd5utxnXjxzMSoLYyzd231anQsB/t3ct3/fJFff55P+K/qy+fTPnj6fW4RH4/GY5fsJex0CvrUTAer2azzjCdFFjK1P5DGZfSY4xR4TuCOlTpoCL5pFqtdjPMPAaHkwb4QcrbraGZ2WodchQ3q9kSm0AvIWFDkWhmFiRzyZbeyCuqO5C4Q5FoZra6SL4K6rrysUXVJSQvyos+tylgW/64HY9macGzKsdORquK4NHNGHT9EaOGdBfQyn2dJD5Er30QMoY6KHqY4SlwuyGgYSFDgBJHECKIJ4grmOO33r9OxtvFmiUBol+TuNYvRHq7gjVPm8FFlsjcr7eogk0St4SkNuYcC2IwKXk7lcxAJKIgEhEQiVjfAIs6DfNF2llBY8fSDcocThyHUJdIyhhRQm+SIG0kybC1m0n8JDIdOt40M4v62WgaSiIoVm+6hIQMRaKZWZAkjlitco9gtbhLSI6FUDLUMzVPm2f6YbolLMCHvkkCeObJ40xsR2+iFYlY50ods4uu1Kbt00W2m4sZnaGYTD2fYQKWO4IhYXaConmgUDbhJmVSjHH1mM53BoWeQaEaiuaBQmH+yNmKuMYXM+ZcfAaFn0HhGormgWuFF81uQ9MchWJOxmdQ2BkUBrTS8UChNN6cx76/YXgFw5iNz6C4Z1CCravBaC64iVIRbOpm6qBgzKnYMpiMKf6kncKNeGeqjhcKyWPBphk5ywqFZNZVb640npa9RvHxt7PlzW/m+riNGK/7gHGcqeD62O1/+H5LufI3UEK3LnxoW5KkoCjZqQbdUFFLH0etfFyu8msh3XbxU07m5bbYlkussmdQt29s9TTwHUo+YDWk4VgCvLNYOBNns/Mej/URFX0NzzZvz1c5iWYOtsi8jt3VmH8Mgaa52zYbGlqPxEYu8DnKIHFpXB33cs9KAn3o5kaR1ctV+jYb6/W9xomWzoTrqDzac4nnOW3uJrcbZ+clDh42TMcbVu/48fT7cQHd5quH1yBAnBxOxwUXhIMfg0qJbqcPLRimD6UHSl3K1aKa++0eahiMmlxlCxHiiSbpc088iTSwhK+Z29bX85E/9WqKbyWZJIat3SDu25ZuGhWiZuH50iO+5K5LlJr3241yFEXeTGLVApM2zI87nLdrV7O0RU+xa+iuDPEZ3STxq2pJl1Zw12pJWgrEGj5jjpRMKsfn0t3Pc/l8HdfU3WDx16R99wpOM7PV9KZyFhVBsr0DyeAVnGZmQcI9f5d7Gb0HyeAqkmZmQbIr50FES4qtJS8haaftU4pJb8ejWVrwLJwwmoVbDy9ymCQs2a8B7bR4U9kvPXm05oVmv+tJxXdeVuJrJjMHuTZL95Jdy4ewVep8Vn87FvhfD2nejTuhF9JlWPm3pwNrZcjxuJv/tEaQUOC6VBAhfc6p+kmF3/r9ZhXkBSNTxNtM4jdshOoutluHRIfDFq7jjDQrb5F9COSZrgeD1Dhs3U/ZZqKW2OnigyDPdPnZhl23yd3aJ9XBs9XQa+URMhzv0AFlknh048rtsmOjpD+47C2Gl1tatCbQlhbBPZf51JeCMbJvx/MYn46cIFoj5jeJf8z8mIADHEMDt01GKoLu6mizRh3DHLxGGlqe9VXu3/fbKdWvqvOWy+qYsYZxrw/hMHIvdlyS3heq2B6HT9+BKVaTBlm4OjmDlh5bVXCPUJ95whfCYfvuEm822TiOyx3EF0zad6c1mpltqc2n4yrlDbbAuYTkfN4bHDA1e1tUn8bjYCfX5V3YXjorty50hvFR85IGaZHAj2g8KuM5XjA1lXBXHnK+yu6La9QQ3vZtyUgCoZKHMO2inhYELSdwIjgjDmcqhWiTh2ruemUpRhLPwwwVWlLDl078Q19+z4jdTpghK+kFe92iBKXcttte6UlMjRdNL2VURIs6kningZkMPMisdlltdZNr9SJgXy0RZl9GHdcXjDLXI4zSfZVRJvFoTLEhatK+XB8ZPvg69rYmR8EmzWyeeVcWAX0S91VIevPNlRqJxoXrmrSpuPCkq1Lxtic2GclguVgsGKJrk/Z5jWTg5KGZ2jLaxXRWSObjmzAmiatVErMScvj0Qi2kX/8I9f61BoepWTAimZTUlUrd+wXPYlH7DV/sXETNJu27ix+amUW9hAfJtHJG2NLrEpLBWYJmZit+sHG0ZCsX35k1E8W/Q/qPJ/mXFwZWTi7kcGmBoHWFLRAoJcxxhCN8lxLh7JveN95ovi4XAba9ZFL/+ArhmqRXwnG1qrtejA6/LZmr55UcZwnmzHcL5/6CZY8GbGu5TkSVeIXE68OmQh7aFzp8I/VCoandSvk8oCm7Ex3xby4I8z3mCkkFZaT17jiVMtkUuUAcwKT9CzdPNRyLeaebZCHLVTpHzWuS+A/YBtOCDdoGm06mPveaMkFsZ5J+2DaYZm5L8nK64qyS+ArLJPGrt8E0qmvbYK7vt5uwvthvg20SGVS5mM2xFM+g/cFtMM3SVtpPi5hvIo6X9k0Sf7dtMC3FtW0wzjnzGKO8NUYdeBGLV0tsn8UkfXciqJlZzJCHoqm81ULegWRwIqiZWZDIcL5erBYq2xmOZPAumGZmQSLywp861Qbrpb6E5M5dMM3SppkoCtLFPB3jq00jqfg3pcjuI1Pj4xctf3VzjqyVheXIruNK9V/bhLU/0dQWHHabfJSMkxJLI03q96eRN4s6YDrTEti8KInqeZ4IbKTfIt7NwB+WLmvktm7jsJmyup6O0MFhauah+dSVXdZL6oLDxUiqb8qbdeqldYClXlS4xCHCFY7DPdbuFZBtVnhzB7vN5Iz2jSdRL4s9wPAan61LaTKNi9F0laKGN0l8dCP+HS+f6oTjpIauqvr59ObwW2spGd7XcK2EPp519teqQEvozONUEKJCnyNEW2yu06zxJ1WDHWIwaZv2J8NLq5qtbfINdqttPqnx9niThKWub8C7qEoSZp0iNXO8KXtD59Nd3FAUoxm2bp6Q361hyDIhD5guTx7G75yljelW3weldYHNt1Iw4brcdRzmKRdsjw4X8TStqk2IlaRM4h+cjwY1LWh8tvJ0km+iypvj5WmTxONTsjs84LrVr3YA9RIurQq0KMl9SVxfSqmSLS7ctmwjJutczEOC9b2Z1P8eGYlGbvGNrEjniRf4ePusSeL/3TcemLcD2jc3v2itYStpV1IVSih1BeeOaJ2IluswcXcVdjDTpP0AJ7pZ4gFepUWx1UvW/nTRBHP/sXJeBv6wwaKRW8SqJ3Qb1zHHd1JNEg9N3y9rBDp5p4izsre+nGRg2q5lx1xeEsbaQxSc+NzbX6A13szjySqqsJP4Ju2LC1WL2N+huEPa/DpctkLTjqZJHMR436xJ4vE50y227n3LtLnhCDekSFp0xM6Mey4RTKq50fXJ/saFJElJOC4Z1npq0h5q5zNRB9hb47Otywsyl9O0xq6qug6+U/ZHsWo4FqzLyZLnxW4Wor5pivvQLTejAGAuBoHod+2saQnRbkJX+Z7yPp8R6sj20JY7qkOHNBQrhZq0H3dcTnO3bc9ErCR0uV6iRjPt/ug0i57b7eCohyKwZc64EFyuJ9paYGy68DzqUul5vqP+57erVTfPdqtoO0J3fgzaN4zEnoBDjNrBsaUD291snvnr+kNYz+B9NHpoWLYNe5Hm42wX+qgjmr787z+3qXGiVSLz3OZqvp2vmipxcfEMqz4wQ6O9sXWy7Mc3rLVg2E6qpGSvE8F8T7qtQpKFu1hWQYHNbCZt00fp8bq+gyxD5tyOucUT49F00uReceXmDYPEkB3rPu7bdqw1KrQpUVAufcJdSQRhbWeAM55wwuYppmeTtt4kBThv165maatMNnHjlW6KX+hrkrBc3GFAO2psPHntzqJpVmgdslAxPvOjER55zOD1kGbhQ73/GGLfnizV7l6CYytyXy5srwo9SrWMaK8lpypq8TZzJq7XjtJZthAFcybYkSiT9gNq25qtxYOomGThIhiv8KO/BokH1bY1c9SnGj8SzqKp8L56s1Tx67ZV9MbS526KOHz2fu5mZ2nym22Zbt1yu+SNFFz42qkG3WZri92MU08w4TitSpOx3NWTVYjdIm3SvrDNdtfRQc3fVskueRbO0q33cXB3HdPR/G1Fr2gkC7lm2AbVdXDu3ZrT/G15X54UNZMJx2dbQ/m/6Hzaj/45gSHn0rRmsPNoWlrM+X3pMacNxpJ4h7OJxdLPZguaYqfATNp3NxhpZrZO8822jAWtMU+/hMQ886Uj2wfHpgZlQbzbNLFIK1LhNTNjBP3Sw0BwIkd3qPuHgLQk6CyuckCikj+fuJx73j50zlajSTjCDqaYtB8wi2u2tg7eadwU1TrGq0Vm6BhQeIi+WisPx49vLRlZgkGvshCloLagZUJzdEk4cXzOpDLT/hTeal1yfxnvsKnNpP24+pDmbgvPQbRtxqzEk2Nz/P2KA4I/0IOBGieSl7XXQwVNXitof/QewaQfh/Sl9+Qi+Oye3gN1wDNt4MNp4LNR4DNJ4NMt4JVuvTuywJ1N8MYieEMQvGEH3m0DbxOB17XAC1PglSXwrg94Ywe8cAPedACPh8MDvfDkMjwkC0+jwsOj8PgmPH0JTyDC837wtBw8pQYPVcETWvCMFLzrAB7bh4eg4HkWeBYEHnOAhwhgCz1sWYct37DZGva3wgZi2MILm2hhAyvsRIUdhb0mPNBWBnu0YLsRbPKBnTmwsQZ2iMB2C9g3ALfa4RYpXMTALBKmbDAhgNkFjBtwBMPJGE5McEaBUwMMjjCcwR1PuJcHN8jg9gncnIAFeVh27BUAQV0cFlRhHQ8WsWDRCBZdYLkDVi1g0QEus+HiFq5I4bV28II5+MAa+GQT+AAR+LAM+CgK+IwH+EQGeMs/vF8fXi4Pb6aG9zr3LlQGt+rC+1rh7avwSll4QWzv+ltwhy28Qx7e1w0vYYVXqsIbUeH9pvB60t5Vo+CmUHjfp36U1Z9fjtPkf2dFO98cHqRWrPJ88s9/Ht7+/D+830pB> for the A=1 part. The other part should be similar. It's a bit tedious and you need to hint the model on a few eqtrd. I also had to hint `mvlladdd` to it by doing a search for it.
Hope it helps! -stan On Sun, Jul 19, 2020 at 10:57 AM Stanislas Polu <[email protected]> wrote: > Hi Jon! > > I think eqtri is at least a plausible way to go here. > > I think something along these lines could get you there? I entered the > first eqtri manually here as the model fails to make useful progress early > on. > > > https://mmproofassistant.azurewebsites.net/#eJydV9uSojAQ/ZUUT1qDbiDIxap9UJ92q+YLZueB6xjuEmBE13/fgEIiIqvWVE2FDNPndJ/TnXAUcO5GRFgehX1i+Dqy8rB+yKvUFZZCaFpuKIhCamZunAvLuAhDUSC5Sf+p2RCiapZmSeLRl7BDn1kUUQgT08Hxl7D0zJC4J1EIHB8rhl6WHITjEjvDaY6TeBRoskniPMNWkbsOsCoggsXsdxHOZCjD+bSFZwgUjqQoN5xQ5eG2VZrkW5dgMoq2Au4cbDZtWBbp/FpBKyYkqRvXMKUXbO1gGzsczFdijtdtAlbgJ5DAjz9/wJquZDC9qZgo2EkYmilxnW6nocMQB+iQnSWnplkYz2e97mXdRRqAcQ0j0mB2cJ+HqXN/o1lPad6oBWPxBsB2FQmlg6fkr4BNAAL7OcWcUtQJrTR9qMFreK2FZwgD8FIi6Xak7hEHn5t2jm0O+kaVlsHHB/g7A+m2+U3A52e9mNQbtfh0ZwqOx/pxefHE6dRsELpxtsbpVHuj6cWlkEZoLuOWN6PW502NaYYFpQrnECqqApGsaCoyVGUBNZpUluulISsL/b5tb6Kz9qA8H/crgxooLgpI6GF5O9I+d3k05XmcB4Ma4CFj0yPld/Q1KnI/lWuR67qs60VNbHORetWsqaKrRuGzuhu6bpVe0/UEaGDWupM1SP1zpb67o0OwFZ9RHhNfliUVSoZiIEPXDaggmqznB3YWBAtppOj96Lz49+k+rgbjMKCGgwMf+gmBLxAcqeVTtmUcBgjGBYx3qPTgqF36Ifp2aebt2TDdcsOWE7r/Rjdq4qtucqzA7DI9O1tpV1a6Sfzac5ydSGGZjpPhzlIsrRFLIU2XEISSpC00SUe6Suth+8VeSv1oNyJYP3hbDa07dx5UhoENWWcfJS4OUvUFJgO1e5IaQx90tR99RxgaL1CTnmbSgQ0w0SzV+TYNXL1UpIEyvVFrtSfqgwQZhwGCpozzA4qxNdpf/RDPjuORVPiGuryEen/cXDrv3nxmOYw0k6Ip9FyWJWgodE7LqkKTVzwjLHFcpiPq9IM/pM5tKo/LxUgNyAUr4oXlYT82r//LGL3mI4Z9Q+xUK1MlBYX5uPo2YR8K4vXtnrvz8ldS/n7IX/T4mwl/N+DPJv6g4w8Evr/4icaPEL6JebPzteSF4WvBrjuf4qV3fsVp0V2Tmw+39/fz4+kfOGw5mQ== > > > On Sun, Jul 19, 2020 at 10:28 AM Jon P <[email protected]> wrote: > >> Hi Thierry, >> >> That's is very nice progress! I have been playing around with the tool >> and I like it, it seems to have an obsession with eqtri however that also >> seems to work out quite often so it's probably right to think highly of it. >> I have done all the practice problems and I'm searching for some theorems I >> might be able to prove with it. >> >> One thing I noticed doing Filip's practice problems is that the 4th >> problem of his is much more difficult than the others and I have not yet >> been able to solve it using suggestions from the tool. I found this a bit >> surprising. My solutions are here >> <https://docs.google.com/document/d/1cpbz2ZJ60qR0220fUTvCWAv4NYX4y8JTClCwGnzryXc/edit?usp=sharing>if >> anyone is also trying the practice problems. I don't know if anyone else >> has found anything similar. >> >> -- >> You received this message because you are subscribed to the Google Groups >> "Metamath" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/metamath/50a189c7-3f29-40ef-bd32-ee6246c2eceeo%40googlegroups.com >> <https://groups.google.com/d/msgid/metamath/50a189c7-3f29-40ef-bd32-ee6246c2eceeo%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACZd_0yUGVS_Pr-b3aNq17LnqSP6Dg%2BP6_KRD08Q59aPvJue3w%40mail.gmail.com.
