1155   \begin{proof} By induction on our POSIX rules. It is clear that

  1155   \begin{proof} By induction on our POSIX rules. By

  1156   @{text "v\<^sub>1"} and @{text "v\<^sub>2"} have the same underlying

  1156   Thm~\ref{posixdeterm} and the definition of @{const LV}, it is clear

  1157   string.

  1157   that @{text "v\<^sub>1"} and @{text "v\<^sub>2"} have the same

  1158 

  1158   underlying string @{term s}.  The three base cases are

  1159   The two base cases are straightforward: for example for @{term

  1159   straightforward: for example for @{term "v\<^sub>1 = Void"}, we have

  1160   "v\<^sub>1 = Void"}, we have that @{term "v\<^sub>2 \<in> LV ONE

  1160   that @{term "v\<^sub>2 \<in> LV ONE []"} must also be of the form

  1161   []"} must also be of the form \mbox{@{term "v\<^sub>2 =

  1161   \mbox{@{term "v\<^sub>2 = Void"}}. Therefore we have @{term

  1162   Void"}}. Therefore we have @{term "v\<^sub>1 :\<sqsubseteq>val

  1162   "v\<^sub>1 :\<sqsubseteq>val v\<^sub>2"}.  The inductive cases for

  1163   v\<^sub>2"}.  The inductive cases are as follows:

  1163   @{term "ALT r\<^sub>1 r\<^sub>2"} and @{term "SEQ r\<^sub>1

  1164 

  1164   r\<^sub>2"} are as follows:

  1165   \begin{itemize} \item[$\bullet$] Case @{term "s \<in> (ALT r\<^sub>1

  1165 

  1166   r\<^sub>2) \<rightarrow> (Left w\<^sub>1)"}: In this case @{term

  1166 

  1167   "v\<^sub>1 = Left w\<^sub>1"} and the value @{term "v\<^sub>2"} is

  1167   \begin{itemize} 

  1168   either of the form @{term "Left w\<^sub>2"} or @{term "Right

  1168 

  1169   w\<^sub>2"}. In the latter case we can immediately conclude with

  1169   \item[$\bullet$] Case @{term "s \<in> (ALT r\<^sub>1 r\<^sub>2)

  1170   @{term "v\<^sub>1 :\<sqsubseteq>val v\<^sub>2"} since a @{text

  1170   \<rightarrow> (Left w\<^sub>1)"}: In this case @{term "v\<^sub>1 =

  1171   Left}-value with the same underlying string @{text s} is always

  1171   Left w\<^sub>1"} and the value @{term "v\<^sub>2"} is either of the

  1172   smaller or equal than a @{text Right}-value.  In the former case we

  1172   form @{term "Left w\<^sub>2"} or @{term "Right w\<^sub>2"}. In the

  1173   have @{term "w\<^sub>2 \<in> LV r\<^sub>1 s"} and can use the

  1173   latter case we can immediately conclude with @{term "v\<^sub>1

  1174   induction hypothesis to infer @{term "w\<^sub>1 :\<sqsubseteq>val

  1174   :\<sqsubseteq>val v\<^sub>2"} since a @{text Left}-value with the

  1175   w\<^sub>2"}. Because @{term "w\<^sub>1"} and @{term "w\<^sub>2"}

  1175   same underlying string @{text s} is always smaller or equal than a

  1176   have the same underlying string @{text s}, we can conclude with

  1176   @{text Right}-value.  In the former case we have @{term "w\<^sub>2

  1177   @{term "Left w\<^sub>1 :\<sqsubseteq>val Left w\<^sub>2"}.\smallskip

  1177   \<in> LV r\<^sub>1 s"} and can use the induction hypothesis to infer

  1178   @{term "w\<^sub>1 :\<sqsubseteq>val w\<^sub>2"}. Because @{term

  1179   "w\<^sub>1"} and @{term "w\<^sub>2"} have the same underlying string

  1180   @{text s}, we can conclude with @{term "Left w\<^sub>1

  1181   :\<sqsubseteq>val Left w\<^sub>2"} by Prop ???.\smallskip

  1182   r\<^sub>1"}. This is needed when @{term "v\<^sub>2 = Left

  1186   r\<^sub>1"}. This is needed when @{term "v\<^sub>2"} is of the form

  1183   w\<^sub>2"}: since \mbox{@{term "flat v\<^sub>2 = flat w\<^sub>2"}

  1187   @{term "Left w\<^sub>2"}: since \mbox{@{term "flat v\<^sub>2 = flat

  1184   @{text "= s"}} and @{term "\<Turnstile> w\<^sub>2 : r\<^sub>1"}, we

  1188   w\<^sub>2"} @{text "= s"}} and @{term "\<Turnstile> w\<^sub>2 :

  1185   can derive a contradiction using Prop.~\ref{inhabs}. So also in this

  1189   r\<^sub>1"}, we can derive a contradiction using

  1186   case \mbox{@{term "v\<^sub>1 :\<sqsubseteq>val v\<^sub>2"}}.\smallskip

  1190   Prop.~\ref{inhabs}. So also in this case \mbox{@{term "v\<^sub>1

  1187 

  1191   :\<sqsubseteq>val v\<^sub>2"}}.\smallskip

  1188   \item[$\bullet$]  Case @{term "(s\<^sub>1 @ s\<^sub>2) \<in> (SEQ r\<^sub>1 r\<^sub>2)

  1192 

  1189   \<rightarrow> (Seq w\<^sub>1 w\<^sub>2)"}: Assume @{term "v\<^sub>2 =

  1193   \item[$\bullet$] Case @{term "(s\<^sub>1 @ s\<^sub>2) \<in> (SEQ

  1190   Seq (u\<^sub>1) (u\<^sub>2)"} with @{term "\<Turnstile> u\<^sub>1 : r\<^sub>1"}

  1194   r\<^sub>1 r\<^sub>2) \<rightarrow> (Seq w\<^sub>1 w\<^sub>2)"}: We

  1191   and \mbox{@{term "\<Turnstile> u\<^sub>2 : r\<^sub>2"}}. We have

  1195   can assume @{term "v\<^sub>2 = Seq (u\<^sub>1) (u\<^sub>2)"} with

  1192   

  1196   @{term "\<Turnstile> u\<^sub>1 : r\<^sub>1"} and \mbox{@{term

  1197   "\<Turnstile> u\<^sub>2 : r\<^sub>2"}}. We have @{term "s\<^sub>1 @

  1198   s\<^sub>2 = (flat u\<^sub>1) @ (flat u\<^sub>2)"}.  By the

  1199   side-condition on out @{text PS}-rule we know that either @{term

  1200   "s\<^sub>1 = flat u\<^sub>1"} or @{term "flat u\<^sub>1"} is a

  1201   strict prefix ??? of @{term "s\<^sub>1"}. In the latter case we can

  1202   infer @{term "w\<^sub>1 :\<sqsubset>val u\<^sub>1"} by ???  and from

  1203   this @{term "v\<^sub>1 :\<sqsubseteq>val v\<^sub>2"} by ???.  In the

  1204   former case we know @{term "u\<^sub>1 \<in> LV r\<^sub>1 s\<^sub>1"}

  1205   and @{term "u\<^sub>2 \<in> LV r\<^sub>2 s\<^sub>2"}. With this we

  1206   can use the induction hypotheses to infer @{term "w\<^sub>1

  1207   :\<sqsubseteq>val u\<^sub>1"} and @{term "w\<^sub>2

  1208   :\<sqsubseteq>val u\<^sub>2"}. By ??? we can again infer @{term

  1209   "v\<^sub>1 :\<sqsubseteq>val v\<^sub>2"} and are done.

  1210 

  1196   Given a lexical value @{text "v\<^sub>1"}, say, in @{term "LV r s"} for which there does 

  1216   \noindent This theorem shows that our posix value @{text

  1197   not exists any smaller value in @{term "LV r s"}, then this value is our POSIX value:

  1217   "v\<^sub>1"} with @{term "s \<in> r \<rightarrow> v\<^sub>1"} is a

  1218   minimal element for the values in @{text "LV r s"}. By ??? we also

  1219   know that any value in @{text "LV s' r"}, with @{term "s'"} being a

  1220   prefix, cannot be smaller than @{text "v\<^sub>1"}. The next theorem

  1221   shows the opposite---namely any minimal element must be a @{text

  1222   POSIX}-value.  Given a lexical value @{text "v\<^sub>1"}, say, in

  1223   @{term "LV r s"}, for which there does not exists any smaller value

  1224   in @{term "LV r s"}, then this value is our @{text POSIX}-value:

  1203   \begin{proof}

  1230   \begin{proof} By induction on @{text r}. The tree base cases are

  1204   By induction on @{text r}.

  1231   again straightforward.  For example if @{term "v\<^sub>1 \<in> LV

  1232   ONE s"} then @{term "v\<^sub>1 = Void"} and @{term "s = []"}. We

  1233   know that @{term "[] \<in> ONE \<rightarrow> Void"} holds.  In the

  1234   cases for @{term "ALT r\<^sub>1 r\<^sub>2"} and @{term "SEQ

  1235   r\<^sub>1 r\<^sub>2"} we reason as follows:

  1236 

  1237   \begin{itemize}

  1238 

  1239   \item[$\bullet$] Case @{term "v\<^sub>1 \<in> LV (ALT r\<^sub>1

  1240   r\<^sub>2) s"} with @{term "v\<^sub>1 = Left w\<^sub>1"} and @{term

  1241   "w\<^sub>1 \<in> LV r\<^sub>1 s"}: In order to use the induction

  1242   hypothesis we need to infer 

  1243 

  1244   \begin{center}

  1245   @{term "\<forall>v'

  1246   \<in> LV (ALT r\<^sub>1 r\<^sub>2) s. \<not> (v' :\<sqsubset>val

  1247   Left w\<^sub>1)"}

  1248   implies

  1249   @{term "\<forall>v' \<in> LV r\<^sub>1

  1250   s. \<not> (v' :\<sqsubset>val w\<^sub>1)"}

  1251   \end{center}

  1252 

  1253   \noindent This can be done because of ?? we can infer that for every

  1254   @{text v'} in @{term "LV r\<^sub>1 s"} and @{term "v'

  1255   :\<sqsubset>val w\<^sub>1"} also @{term "Left v' :\<sqsubset>val

  1256   Left w\<^sub>1"} holds. This gives a contradiction. Consequently, we

  1257   can use the induction hypothesis to obtain @{term "s \<in> r\<^sub>1

  1258   \<rightarrow> w\<^sub>1"} and then conclude this case with @{term "s

  1259   \<in> ALT r\<^sub>1 r\<^sub>2 \<rightarrow> v\<^sub>1"}.\smallskip

  1260 

  1261   \item[$\bullet$] Case @{term "v\<^sub>1 \<in> LV (ALT r\<^sub>1

  1262   r\<^sub>2) s"} with @{term "v\<^sub>1 = Right w\<^sub>1"} and @{term

  1263   "w\<^sub>1 \<in> LV r\<^sub>2 s"}: Like above we can use the 

  1264   induction hypothesis in order to infer @{term "s \<in> r\<^sub>2

  1265   \<rightarrow> w\<^sub>1"}. In order to conclude we still need to

  1266   obtain @{term "s \<notin> L r\<^sub>1"}. Let us suppose the opposite.

  1267   Then there is a @{term v'} such that @{term "v' \<in> LV r\<^sub>1 s"}

  1268   by Prop ??? and hence @{term "Left v' \<in> LV (ALT r\<^sub>1 r\<^sub>2) s"}.

  1269   But then we can use the second assumption of the theorem to infer that 

  1270   @{term "\<not>(Left v' :\<sqsubset>val Right w\<^sub>1)"}, which cannot be the case.

  1271   Therefore @{term "s \<notin> L r\<^sub>1"} must hold and we can also conclude in this

  1272   case.

  1273 

  1274  

  1275 

  1276 

  1277   \end{itemize}

  1278