1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
16 include "Q/fraction/fraction.ma".
20 [ (pp n) \Rightarrow (nn n)
21 | (nn n) \Rightarrow (pp n)
22 | (cons x g) \Rightarrow (cons (Zopp x) (finv g))].
24 theorem finv_finv: ∀f. finv (finv f) = f.
35 theorem or_numerator_nfa_one_nfa_proper:
37 (numerator f = nfa_one ∧ ∃g.numerator (finv f) = nfa_proper g) ∨
38 ∃g.numerator f = nfa_proper g.
41 apply (ex_intro ? ? (nf_last n)).reflexivity
44 |apply (ex_intro ? ? (nf_last n)).reflexivity
51 rewrite > H.rewrite > H1.simplify.
54 |apply (ex_intro ? ? (nf_cons O a)).reflexivity
57 rewrite > H.rewrite > H1.simplify.
58 right.apply (ex_intro ? ? (nf_last n)).reflexivity
60 rewrite > H.rewrite > H1.simplify.
63 |apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity
71 apply (ex_intro ? ? (nf_cons O a)).reflexivity
74 right.apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity
78 apply (ex_intro ? ? (nf_cons O a)).reflexivity
84 theorem eq_nfa_one_to_eq_finv_nfa_proper:
85 ∀f.numerator f = nfa_one → ∃h.numerator (finv f) = nfa_proper h.
87 elim (or_numerator_nfa_one_nfa_proper f); cases H1;