proposition: Theorem eval_nfa e: eval (nfa e) ≡ e.
proof: Proof. rewrite <- (Thompson.correct e) at 2. unfold nfa. change (mx_scal ((Thompson.enfa e)^u ⋅ ((epsilon_mx (Thompson.enfa e)^M)^* ⋅ pure_part_mx (Thompson.enfa e) ^M) ^* ⋅ ((epsilon_mx (Thompson.enfa e)^M)^* ⋅ (Thompson.enfa e) ^v)) ≡ eval (Thompson.enfa e)). set (f := Thompson.enfa e). set (J := epsilon_mx f^M). apply mx_scal_weq. rewrite (@expand_simple_mx _ _ f^M) at 2 by apply Thompson.is_enfa. rewrite str_pls. rewrite <-dotA, (dotA _ (J^*)). rewrite <-str_dot. apply dotA. Qed.
imports: kleene sums matrix_ext lset boolean lang nfa regex bmx rmx normalisation