DFSA

I have wrote about NFSA, Cartesian Product stuff already. Since DFSA is the basis of all the automaton machines, I need to show some understanding in DFSA.
Here I wrote the proof of state invariants, for question 4 in A3:

The state invariants of the DFSA are:
\delta(s,x) = (q(\epsilon), q(0)') if x = \epsilon
(q(0), q(0)') if x = 0 mod 5, the length of x is even
(q(0), q(1)') if x = 0 mod 5, the length of x is odd
(q(1), q(0)') if x = 1 mod 5, the length of x is even
(q(1), q(1)') if x = 1 mod 5, the length of x is odd
(q(2), q(0)') if x = 2 mod 5, the length of x is even
(q(2), q(1)') if x = 2 mod 5, the length of x is odd
(q(3), q(0)') if x = 3 mod 5, the length of x is even
(q(3), q(1)') if x = 3 mod 5, the length of x is odd
(q(4), q(0)') if x = 4 mod 5, the length of x is even
(q(4), q(1)') if x = 4 mod 5, the length of x is odd

Proof:
Base case: x = \epsilon. In this case, \delta(q(\epsilon),x) = (q(\epsilon), q(0)'). All other states are vacuously true.
Induction Step: Assume P(x'), x' being some string of {0,1}*. And let x = x'a. Then either a = 0 or a = 1.
Case a = 0: Then \delta*(s,x) = \delta*((q(\epsilon), q(0)'), x'0) = \delta((\delta*(q(\epsilon), q(0)'), x')), 0)
= \delta(q(\epsilon), q(0)'), 0) if x' = \epsilon # By IH, P(x')
\delta((q(0), q(0)'), 0) if x' = 0 mod 5, the length of x is even
\delta((q(0), q(1)'), 0) if x' = 0 mod 5, the length of x is odd
\delta((q(1), q(0)'), 0) if x' = 1 mod 5, the length of x is even
\delta((q(1), q(1)'), 0) if x' = 1 mod 5, the length of x is odd
\delta((q(2), q(0)'), 0) if x' = 2 mod 5, the length of x is even
\delta((q(2), q(1)'), 0) if x' = 2 mod 5, the length of x is odd
\delta((q(3), q(0)'), 0) if x' = 3 mod 5, the length of x is even
\delta((q(3), q(1)'), 0) if x' = 3 mod 5, the length of x is odd
\delta((q(4), q(0)'), 0) if x' = 4 mod 5, the length of x is even
\delta((q(4), q(1)'), 0) if x' = 4 mod 5, the length of x is odd
= (q(\epsilon), q(0)') if x = \epsilon
(q(0), q(0)') if x = 0 mod 5, the length of x is even
(q(0), q(1)') if x = 0 mod 5, the length of x is odd
(q(1), q(0)') if x = 1 mod 5, the length of x is even
(q(1), q(1)') if x = 1 mod 5, the length of x is odd
(q(2), q(0)') if x = 2 mod 5, the length of x is even
(q(2), q(1)') if x = 2 mod 5, the length of x is odd
(q(3), q(0)') if x = 3 mod 5, the length of x is even
(q(3), q(1)') if x = 3 mod 5, the length of x is odd
(q(4), q(0)') if x = 4 mod 5, the length of x is even
(q(4), q(1)') if x = 4 mod 5, the length of x is odd .

Case a = 1: Then \delta*(s,x) = \delta*((q(\epsilon), q(0)'), x'1) = \delta((\delta*(q(\epsilon), q(0)'), x')), 1)
= \delta(q(\epsilon), q(0)'), 1) if x' = \epsilon # By IH, P(x')
\delta((q(0), q(0)'), 1) if x' = 0 mod 5, the length of x is even
\delta((q(0), q(1)'), 1) if x' = 0 mod 5, the length of x is odd
\delta((q(1), q(0)'), 1) if x' = 1 mod 5, the length of x is even
\delta((q(1), q(1)'), 1) if x' = 1 mod 5, the length of x is odd
\delta((q(2), q(0)'), 1) if x' = 2 mod 5, the length of x is even
\delta((q(2), q(1)'), 1) if x' = 2 mod 5, the length of x is odd
\delta((q(3), q(0)'), 1) if x' = 3 mod 5, the length of x is even
\delta((q(3), q(1)'), 1) if x' = 3 mod 5, the length of x is odd
\delta((q(4), q(0)'), 1) if x' = 4 mod 5, the length of x is even
\delta((q(4), q(1)'), 1) if x' = 4 mod 5, the length of x is odd
= (q(\epsilon), q(0)') if x = \epsilon
(q(0), q(0)') if x = 0 mod 5, the length of x is even
(q(0), q(1)') if x = 0 mod 5, the length of x is odd
(q(1), q(0)') if x = 1 mod 5, the length of x is even
(q(1), q(1)') if x = 1 mod 5, the length of x is odd
(q(2), q(0)') if x = 2 mod 5, the length of x is even
(q(2), q(1)') if x = 2 mod 5, the length of x is odd
(q(3), q(0)') if x = 3 mod 5, the length of x is even
(q(3), q(1)') if x = 3 mod 5, the length of x is odd
(q(4), q(0)') if x = 4 mod 5, the length of x is even
(q(4), q(1)') if x = 4 mod 5, the length of x is odd
So forall string x', forall a \in {0,1}, x = x'a, P(x') -> P(x).

Therefore \forall x \in {0,1}*, P(x).