equal
deleted
inserted
replaced
463 \end{center} |
463 \end{center} |
464 |
464 |
465 \noindent |
465 \noindent |
466 where the terms @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} |
466 where the terms @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} |
467 stand for all transitions @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow> |
467 stand for all transitions @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow> |
468 X\<^isub>i"}. In terms of finite automata, every equation @{text "X\<^isub>i = rhs\<^isub>i"} in this system |
468 X\<^isub>i"}. If viewed as an automaton, then every equation @{text "X\<^isub>i = rhs\<^isub>i"} in this system |
469 corresponds very roughly to a state whose name is @{text X\<^isub>i} and its predecessor states |
469 corresponds roughly to a state whose name is @{text X\<^isub>i} and its predecessor states |
470 are the @{text "Y\<^isub>i\<^isub>j"}; the @{text "c\<^isub>i\<^isub>j"} are the labels of the transitions from these |
470 are the @{text "Y\<^isub>i\<^isub>j"}; the @{text "c\<^isub>i\<^isub>j"} are the labels of the transitions from these |
471 predecessor states to @{text X\<^isub>i}. In our initial equation system there can only be |
471 predecessor states to @{text X\<^isub>i}. In our initial equation system there can only be |
472 finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} in a right-hand side |
472 finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} in a right-hand side |
473 since by assumption there are only finitely many |
473 since by assumption there are only finitely many |
474 equivalence classes and only finitely many characters. The term @{text |
474 equivalence classes and only finitely many characters. The term @{text |