\ 5a href="cic:/matita/tutorial/chapter7/beqitem.fix(0,1,4)"\ 6beqitem\ 5/a\ 6 S i1 i2 ≡ \ 5a href="cic:/matita/tutorial/chapter4/eqb.fix(0,0,3)"\ 6eqb\ 5/a\ 6 X i1 i2.
(*
\ 5a href="cic:/matita/tutorial/chapter7/beqitem.fix(0,1,4)"\ 6beqitem\ 5/a\ 6 S i1 i2 ≡ \ 5a href="cic:/matita/tutorial/chapter4/eqb.fix(0,0,3)"\ 6eqb\ 5/a\ 6 X i1 i2.
(*
The intuitive semantic of a point is to mark the position where
we should start reading the regular expression. The language associated
to a pre is the union of the languages associated with its points. *)
The intuitive semantic of a point is to mark the position where
we should start reading the regular expression. The language associated
to a pre is the union of the languages associated with its points. *)