I have found a nice set of lecture on software verification:
The course introduces the theory and practice of formal methods for the design and analysis of software systems. The course will cover the underlying logical and theoretical concepts, with focus on the algorithmic solutions, and heuristics to cope with the high computational complexity.
Polynomial , where each is divisible by some number , is irreducible in when does not divide .
If A is not irreducible then there are some and such as .
But that means that , which means that XOR (since does not divide ).
Let’s assume that . Now let’s take a map (I believe this method is called homomorphism-reduction).
, but , where .
That is possible only when is constant and . Which means that is irreducible.
Note: here denotes where is a homomorphism .
Let’s say we have a possibly infinite collection of countable sets , prove that is countable too. We are going to do this using Axiom of Choice.
Since every set is countable, there is a set of injections from to , let’s call it . Using the axiom of choice we can create a set of maps from to . Now, we are going to create an injection from to . If is an element of then it’s also an element of some set . Therefore we can construct where . And since we know that is countable, we can map to . QED.