Last active
May 4, 2026 19:55
-
-
Save lovely-error/7f2050f365645f95a8853bf1320664fe to your computer and use it in GitHub Desktop.
Domino AND, OR, NOT fns from NOR fn
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -- https://www.falstad.com/circuit/circuitjs.html?ctz=DwYwlgTgBAZgvAIgIwKgFwM6IAwDpsEECsqYIiSeATAVQOx0DM2AHFQGwCcndqIARoiLZUAB0EIALI1QA3CENQBbTEICmAWiQoAfACgoUYAHcoAD0R0WkqEU5UoVm5MktU8BCID0+w8DTmluwstlQhLEjsoW6wOGIAdohaqPxqFATKAPaIACZqMACGAK4ANmhyqUl47JRWdJxEHHQcSES8ULL85Aga1WF0kTT0LCzY7IwkPgZGAEqBCBFRkuw2LCtQy5LucVDGHiJQSgVmsopTfnMWCCvY0bZ0UY0x+6h7iFTuCtcHRydnvkYAlcnLZ7FBFqCPrFPAkKCk0sgModsgg8oVSuUOpVPLgaJErCtGJIxs1lhVutRsFQkCxOBE6NhGMFGBwEOcjKYrpwkA4iC5wZFbC5tjD2cBLoh2EQliyoOxWBsWSKDm8YYdjqcEJMAcBoMDrBtXI4aIbnjsvpQMmKAMrzZq3FwhKVLVzKsRwqAlMA7NAAC3ebJ1AHN5s6Nut2FRnCs3WLOZLiXcbnLibGdfHrom1jZkzx2Gnprq7cEoHnjbc826oF9hFbg-MnuCCBtOFFRgcXjaG2CQY2nFXRB6vT7-QgPmK9ZYDSD7Y5rFWLYRA4WJVqwo4S65bg8zWrVT8Nf9CxnuQ4RrcIeeC34gVObPZwoKHwPEsh4ekfii0cUyhUEZT8WzIkSSoPkYk6ClcSpGk6SQBkmRYRgiV4ONQ0TMtZ0raFvB1VdL2bbMmw7HZ92UQ8tWXG9ixCMsISwl4oFEV8UCgbFLSyXJ8h-TFOgRDROFweorGwOkWGaODxnJJJJFwbg5O4YRQLsIgUDFW8EB3cF1kvGNsNhHoWLYpElC-LiMT-KpcBqbA6gaJoWjaKSej6MTBipKxRhWLYxRDK46LBCFLV3HDj3mS9RgFKJT2vDk7QNB85xsfs9NQq4eW0wUeVlRYYpMeYkBZEI6EaKAsocYqoU7dN8qoVsiNK2rHmFFKdXUnk6vbBrtKRDwWKYj0jM-Tj0V-LF-3wYhtDgplmFqbhmicqhcGEepuTsak2DgzhJE0Nw1JqgjmzKoiRT65j30RIbUTM0beJwCbsBU7QmHGbA5p4KEIPeZabO4Vp7Bpal6h2jQ9twmrZXlEIeQiqGq1I9U-go-a0ppJKmQa2UXpfJJDIRdjkWG7iLOcqzajEuzpTE1gSCxbpeis-o3OkHhlm1UK0qoLGDXSpL5xajmKA4VZMuF0t5VyjNjoqzHyv5qrC0nZA0ccDHKGlVX8z06shCXCdqKTRMngXXW60Vg3COTbMTa1PXqs5yHmll8tJYOi8jpoC9RldtLHqiF6U23JkfYTW5k2TbGBb8DNZ17Ht5biVLQ81wOtK2KPYr8wU+RFx4HhD5BHnlUrHnsXKlY0WUc6gLRi5zm3axC6P5lr25q9buVpVy3zcf5Lca4kjZvYz4BbSuUGHXWLQ+90hjhzVP0A318fBU2GuIs2G3LSb2YW6QPujS0MFHXhhjfk1dnm6uI1IxsQVb4L-ebGlW5s4lkeM1hhUN9nxPWrCsOCob6sBxm+Vi+NjKmRGjxbEGgZL1EQtSGyFNaRhCcloXA2hRgMiQJwRgER954MooCPeUQoYlzlCA7W-UwGDQ4tdaBJM4GCTpCycmCDnx01xpgmkNk3p4IIZIIhScDLFzDBPTuWsFYXFIW3fkGgqBRiFOnBiqpKpfHfufI8Mi0pLFhs4Yeqiz7kUviQ8ekMNb3y7tQ864CPz0O-OZMaSR2A8OwW9dgTAHiEi1l9HoMl5JyWCFKTYnBiH+BblXfk2dmoMRockOxl0HE3RgXxao7DKY1C5twdBLkBiRmwJIFSjAYZhJ8vlMhTt74jEfqXBwRp1q1NTjfVMH95g3yUS04iop7a4zIQqWu4YVF-0LGYFuJViSvw2IyEU6cMDejHOnNACIAByAB5GY4SlZPyGU2IZW87aFjHhQGeNhFHRmGWqQcYD54HEXmOcJq5zmmigPQeprptYIy0cjesVxnn91Ano7pO9gA92QPydapV+Q3FymM32kh6l2FKiJepkZZmoHme8JZCIACCKyAAi4SwUFXXJ1El4QlQj2JTyZFSjtAOFqJVEZfg4VJANBCSuIswnQjmQsqMqBlmIHWQAFXCRmOB0MqQ2AleCQxzKjBgsGZQEYA8ojaEKbldSGh1itluIM3VoCEl0MJgw4mzjSbWVso0aU0gHjcr8QzSMrkCkuBWHyJg4StXrEZaq5FC0bEDQgVdRxt1YEBIYNwRCKkBhIWkOggJgTWYTFrGDFcpDZW3GynKvcxikamPFHvMEuqa6AvFsC14Hh1GSgPHmsVhaGU2QcFoGljLNUtyNJQJRSqpWgLxvYk1IbUnSRYYgua0oeBEBkFwnEVJPaDGKvghFLg+R1tRg4Ms+r84j1XFoB4acS1KOtp83NF8tntvCBFZtZ5s0HEXGbPwxyDI0vPAPPdV5ta3IFaOccvzcZvrqgo7+rZy4t29Y2geLbG0N0OVfXGRbi5Hwbf66RRgK46oQ7g9d78GI1hg5nPppY93dqoShvKK81WFL1ZlP2IHzEOHEbDaxOHTYgqVrSNVRS2wds49B+9Cr8qtAZWEV+KsYblrFKubQJUeQds9g1D5RidjfPzY+n1vNSqCa6pcg41yWKfvQN+s9vsqliyClpg5fHgCsoWHunkzZTwNRmTyjFfLsWIA2auxADn94Km88LAuZZ95KMCy4cTvSEDbTvqFwjHHWmkZPNExgRbbNJaZT0wsYLItQqdll-eNSR7qXY6VIk95EuxJ2PEvtSSB0pKYek5B9RrWEh4FOh1eTmabC5pIFC-8-J1X3hrXLPGA20KDckxh5r+JWQZPSCYrRmj0Fpg6hNgThC0hEjyfNq5cvCdLGCMTp8lMmM8xpEsA2uPQ2G6R9S3niQ0WiXd3tF0CYmSJk4u6-iR1sN+taiYxV43TdYNNBoTBJ1IU9flAgl3fO2ceyNqrL2oFmo+8whB33GugT+0trow7PFA6YCDiYSEZAiLMz5yVCpeYBdh8Fh7-Lt1xTvlGIqatmeHbVMpozXmW1i2sNDfz2s70gsfXzrTiVzMfoWXcwz5T9RM4ijLA7bTgRnZKxuS7TH5VFj62qtXmkCrlbVLhyzCW75MgrIlsuyuhbes42LvLwUTvqYKrZ0zS7aNC0ytF5Vl24vmg-CCqWrBfev2D6VIgjRH6pahZYt3mv0tUQdgy4QTPvUp6e4kxHb3Q1pMwYhYqYw2jLAqtYvxeAeQF4QoweotAik-rTZzb11fdctub+zmtp6Uae9i6-N3furmviNWNmrE2UfVCeHZ9WCkiTY-ptUBkdBiQcDWPKSM1Indc2T4U52BVsNa8-k+fkdE98J-wwse+39770-i5DlVrQSr64j2lkFxLo8O+K-tydUj981TTyaZ3X+uUq4+ueu2+Bu2mFaAYsAGiHeigjEvoBQGAag1ovoYAMAaA90Vgk6sE4wSWi+rgJOOoIA+Ub+rg0MpB8e6c3QSAu0pAmoeABALEGAXwBwsgOQw6dINAAwi+uC+Cp43k4WuW5ufqDK5uj84Gu+vesokhuUxBaUhUjg0mCh7Y6KUA1BtBUAYA9BE0TBLBcg7BUgX2SCLAEeWCAw4SchJyz8+2EKJ+VBFAGhWh90jBGKehHQBhqOrCxh1eIkCKZSRBAm66tmkG1+iA9hyAjh2hLhUAzBOwbBYRRhyqrqUoBUFhkOVSwhamqWqh6hoMdBzhb0rhcRBh8CXhSR3WBUYkRK6Roh+2EhcOpGFcgoL6+qhut69iIij+D+Z2V2WulhEWNK1cDmbQ3+aouRMQThM6hRMRbh8RhhaO1I6qdgcEVRsu3OvIe6wxVuN+XIgx0SjUyish8wDmL6Dm0U2s4x+RUxuhxRCRCxU0j03IdQ1Rux66NKZxaC1uAx16veBEN6XOyAm+lC-Ojsz+qAd6AJq8EU2cnxzGSSy8iAEIa8EIKkYJOs8JOobGzRBEzRCm-uGJ5sXI+xEUQhsJ+J7EIipxxc6mBqXxEIt8GacooRp+ZGiJsMh6JJJ+geYUnJF4T4XJG+aeGMgWgBXxIW6EtmoppGmQUAagr49AGK1yv8CAZgnsTm1yIgAIfgogHQOwGA1BO82pupCAU6+pzhoExCRpCIrWepBplpRgOp1pcgiAppkEVI+aXgmQOoMpcpFA1eipCYIoZgU6umCAWpDpxpBwZpiI9pwAOpmorpzhpiVpQs7Q9BGKdp7IKZgJaZLpGZSZ4Snp+gwAXg4AEA+gQAA | |
| def Bool.nor a b := Bool.not (.or a b) | |
| example : Bool.or a b = .not (.nor a b) := by | |
| decide +revert | |
| example : Bool.and a b = .nor (.not a) (.not b) := by | |
| decide +revert | |
| example : Bool.not a = .nor a a := by | |
| decide +revert | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment