1021   is to find out what the possible splits of @{text "x @ z"} are to be in @{term "A ;; B"}.

  1021   is to find out what the possible splits of @{text "x @ z"} are to be in @{term "A ;; B"}

  1022 

  1022   (this was easy in case of @{term "A \<union> B"}). For this we define the

  1023   notions of \emph{string prefixes} 

  1024 

  1025   \begin{center}

  1026   @{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\hspace{10mm}

  1027   @{text "x < y \<equiv> x \<le> y \<and> x \<noteq> y"}

  1028   \end{center}

  1029 

  1030   \noindent

  1031   and \emph{string subtraction}:

  1032 

  1033   \begin{center}

  1034   \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

  1035   @{text "[] - y"} & @{text "\<equiv>"} & @{text "[]"}\\

  1036   @{text "x - []"} & @{text "\<equiv>"} & @{text x}\\

  1037   @{text "cx - dy"} & @{text "\<equiv>"} & @{text "if c = d then x - y else cx"}\\

  1038   \end{tabular}

  1039   \end{center}

  1040 

  1041   \noindent

  1042   where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings.