Filip asked me to post this. Norm -------- Forwarded Message -------- Subject: New feature of proof assistant Date: Thu, 19 Nov 2020 13:35:16 +0000 (UTC) From: Cernatescu Filip To: Norman Megill
Hi Norman! I want to put a question on metamath forum: I was thinking about a new feature on milpgame proof assistant: If we have a complex metamath statement , we select only: ( ( ( A - 1 ) x. ( 2 x. C ) ) / ( ( A - 1) x. ( 3 x. B ) ) ) and we put milpgame to search on set.mm. Milpgame it will give us some choices: divcan1i, divcan2i ,bla bla , we select one and milpgame will generate for us new statements, first: ( ( A - 1 ) x. ( 2 x. C ) ) / ( ( A - 1 ) x. ( 3 x. B ) ) ) = ( ( 2 x. C ) / ( 3 x. B ) ) and the following statements to be proven : ( A - 1) e. CC , ( 2 x. C ) e. CC , ( 2 x. B ) e. CC. What do you say about that? It will be useful? Thank you very much! -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/b0401880-e4b8-4d09-a63a-b49b9116e301n%40googlegroups.com.
