This is a cleaned up copy of the PrBoom+ SVN repository as a courtesy for those interested in forking that port - GitHub - coelckers/prboom-plus: This is a cleaned up copy of the PrBoom+ SVN reposi...
A source port for Doom that supports vanilla and Boom formats. Fast and highly-configurable, my Doom source port of preference.
Has anyone here read the Katz translation? How does it compare to the other two?
How’s the Katz translation?
(a OR b) -> c
= ~(a OR b) OR c
= (~a AND ~b) OR c
= (~a OR c) AND (~b OR c)
= (a -> c) AND (b -> c) as required
I haven’t formally learnt logic so I’m not sure if my proof is what you’d call rigorous, but the result is pretty useful for splitting up conditionals in proofs like some of the number theory proofs I’ve been trying. E.g.
> Show that if a is greater than 2 and a^m + 1 is prime, then a is even and m is a power of 2
In symbolic form this is:
∀a >= 2 ( a^m + 1 is prime -> a is even AND m is a power of 2 )
The contrapositive is:
∀a >= 2 ( a is odd OR m is NOT a power of 2 -> a^m + 1 is composite )
and due to the result above, this becomes
∀a >= 2 ( a is odd -> a^m + 1 is composite ) AND ( m is NOT a power of 2 -> a^m + 1 is composite )
so you can just prove two simpler conditionals instead of one more complicated one.
Is guix pull still slow? That was a problem I and a few others had a while back.