-
-
-theorem or_numerator_nfa_one_nfa_proper:
-∀f.
- (numerator f = nfa_one ∧ ∃g.numerator (finv f) = nfa_proper g) ∨
- ∃g.numerator f = nfa_proper g.
-intro.elim f
- [simplify.right.
- apply (ex_intro ? ? (nf_last n)).reflexivity
- |simplify.left.split
- [reflexivity
- |apply (ex_intro ? ? (nf_last n)).reflexivity
- ]
- |elim H;clear H
- [elim H1.clear H1.
- elim H2.clear H2.
- elim z
- [simplify.
- rewrite > H.rewrite > H1.simplify.
- left.split
- [reflexivity
- |apply (ex_intro ? ? (nf_cons O a)).reflexivity
- ]
- |simplify.
- rewrite > H.rewrite > H1.simplify.
- right.apply (ex_intro ? ? (nf_last n)).reflexivity
- |simplify.
- rewrite > H.rewrite > H1.simplify.
- left.split
- [reflexivity
- |apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity
- ]
- ]
- |elim H1.clear H1.
- elim z
- [simplify.
- rewrite > H.simplify.
- right.
- apply (ex_intro ? ? (nf_cons O a)).reflexivity
- |simplify.
- rewrite > H.simplify.
- right.apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity
- |simplify.
- rewrite > H.simplify.
- right.
- apply (ex_intro ? ? (nf_cons O a)).reflexivity
- ]
- ]
- ]
-qed.
-
-theorem eq_nfa_one_to_eq_finv_nfa_proper:
-∀f.numerator f = nfa_one → ∃h.numerator (finv f) = nfa_proper h.
- intros;
- elim (or_numerator_nfa_one_nfa_proper f); cases H1;
- [ assumption
- | rewrite > H in H2;
- destruct
- ]
-qed.