diff options
Diffstat (limited to 'language/l2_rules.ott')
| -rw-r--r-- | language/l2_rules.ott | 194 |
1 files changed, 118 insertions, 76 deletions
diff --git a/language/l2_rules.ott b/language/l2_rules.ott index e348e14a..a4624527 100644 --- a/language/l2_rules.ott +++ b/language/l2_rules.ott @@ -762,6 +762,15 @@ E_d |- u ~< t,S_N E_t(id) gives {tid0 |-> kinf0, .., tidn |-> kinfn}, S_N, tag, u u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect +ui == ( implicit<ne>, t0 , .. , tm ) +<E_t,E_d>,(t0,..,tm) |- (exp0,..,expm) : ui' gives (exp0',..,expm'),I,E_t' +E_d,t |- :E_app: id (annot, exp'0, .., exp'm) : uj gives uj', exp'',S_N',effect' +------------------------------------------------------------ :: appImplicit +<E_t,E_d>,t |- :E_app: id(exp0,..,expm) : uj gives exp'', I u+ <S_N,effect>u+ <S_N',effect'>, E_t + + +E_t(id) gives {tid0 |-> kinf0, .., tidn |-> kinfn}, S_N, tag, u +u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect <E_t,E_d>,ui |- exp : ui' gives exp',I,E_t' E_d,t |- :E_app: id (exp') : uj gives uj', exp'',S_N',effect' ------------------------------------------------------------ :: app @@ -799,40 +808,42 @@ S_N' == u+ </S_N'i//i/> ------------------------------------------------------------ :: record <E_t,<E_k,E_a,E_r,E_e>>,t |- { </idi = expi//i/> semi_opt} : x<t_args> gives{ </idi=exp'i//i/> semi_opt}, u+ <S_N u+ S_N', u+ </effecti//i/>>, {} -<E_t,<E_k,E_r,E_e>>,t |- exp : id t_args gives exp', I,E_t -E_r(id t_args) gives </ id'n:t'n//n/> -</ <E_t,<E_k,E_r,E_e>>,ti |- expi : ui gives expi',Ii,E_t//i/> +<E_t,<E_k,E_a,E_r,E_e>>,t |- exp : x<t_args> gives exp', I,E_t +E_r(x<t_args>) gives </ id'n:t'n//n/> +</ <E_t,<E_k,E_a,E_r,E_e>>,ti |- expi : ui gives expi',Ii,E_t//i/> </idi:ti//i/> SUBSET </id'n : t'n//n/> </<E_k,E_a,E_r,E_e> |- ui ~< ti,S_N'i//i/> ------------------------------------------------------------ :: recup -<E_t,<E_k,E_r,E_e>> ,t |- { exp with </idi = expi//i/> semi_opt } : id t_args gives {exp' with </idi = exp'i//i/>}, I u+ </Ii//i/>, E_t +<E_t,<E_k,E_a,E_r,E_e>> ,t |- { exp with </idi = expi//i/> semi_opt } : x<t_args> gives {exp' with </idi = exp'i//i/>}, I u+ </Ii//i/>, E_t -E,t |- exp1 u1 t gives exp'1,I1,E_t ... E,t |- expn : un gives exp'n,In,E_t -length(exp1 ... expn) = num +<E_t,E_d>,t |- exp1 : u1 gives exp'1,I1,E_t' ... <E_t,E_d>,t |- expn : un gives exp'n,In,E_t' +E_d |- u1 ~< t, S_N1 ... E_d |- un ~< t, S_Nn +length(exp1 ... expn) == ne +S_N == {ne=ne2} u+ S_N1 u+ ... u+ S_Nn ------------------------------------------------------------ :: vector -E, vector<ne1,ne2,ord,t> |- [ exp1 , ... , expn ] : vector<ne3,num,ord,u> gives [exp'1,...,exp'n], I1 u+ ... u+ In, E_t +E, vector<ne1 ne2 order t> |- [ exp1 , ... , expn ] : vector<ne1 num order t> gives [exp'1,...,exp'n], <S_N,pure> u+ I1 u+ ... u+ In , E_t -E, vector<ne ne' ord t> |- exp1 : vector<ne1 ne1' inc u> gives exp'1,I1,E_t +E, vector<ne ne' order t> |- exp1 : vector<ne1 ne1' inc u> gives exp'1,I1,E_t E, range<ne2 ne2'> |- exp2 : range<ne3 ne3'> gives exp'2, I2,E_t ------------------------------------------------------------- :: vectorgetInc E, t |- :E_vector_access: exp1 [ exp2 ] : u gives exp'1 [ exp'2], I1 u+ I2 u+ <{ne1<=ne3,ne3+ne3'<=ne1+ne1'},pure>,E_t -E, vector<ne ne' ord t> |- exp1 : vector<ne1 ne1' dec u> gives exp'1,I1,E_t +E, vector<ne ne' order t> |- exp1 : vector<ne1 ne1' dec u> gives exp'1,I1,E_t E, range<ne2 ne2'> |- exp2 : range<ne3 ne3'> gives exp'2, I2,E_t ------------------------------------------------------------- :: vectorgetDec E, t |- :E_vector_access: exp1 [ exp2 ] : u gives exp'1 [ exp'2], I1 u+ I2 u+ <{ne1>=ne3,ne3+(-ne3')<=ne1+(-ne1')},pure>,E_t -E, vector<ne1 ne'1 inc t> |- exp1 : <vector ne2 ne'2 inc u> gives exp'1, I1,E_t +E, vector<ne1 ne'1 inc t> |- exp1 : vector<ne2 ne'2 inc u> gives exp'1, I1,E_t E, range<ne3 ne3'> |- exp2 : range< ne4 ne'4> gives exp'2, I2,E_t E,range <ne5 ne5'> |- exp3 : range< ne6 ne'6> gives exp'3, I3,E_t ------------------------------------------------------------- :: vectorsubInc -E, vector<ne ne' inc t> |- :E_vector_subrange: exp1[ exp2 : exp3 ] : vector<ne7 ne'7 inc u> gives exp'1[exp'2:exp'3], I1 u+ I2 u+ I3 u+ <{ne >= ne4, ne <= ne'4,ne'<=ne4+ne'6,ne4 <= ne2, ne4+ne6' <= ne'2},pure>,E_t +E, vector<ne ne' inc t> |- :E_vector_subrange: exp1[ exp2 .. exp3 ] : vector<ne7 ne'7 inc u> gives exp'1[exp'2:exp'3], I1 u+ I2 u+ I3 u+ <{ne >= ne4, ne <= ne'4,ne'<=ne4+ne'6,ne4 <= ne2, ne4+ne6' <= ne'2},pure>,E_t -E, vector<ne1 ne'1 dec t> |- exp1 : <vector ne2 ne'2 dec u> gives exp'1, I1,E_t +E, vector<ne1 ne'1 dec t> |- exp1 : vector< ne2 ne'2 dec u> gives exp'1, I1,E_t E, range<ne3 ne3'> |- exp2 : range< ne4 ne'4> gives exp'2, I2,E_t E,range <ne5 ne5'> |- exp3 : range< ne6 ne'6> gives exp'3, I3,E_t ------------------------------------------------------------- :: vectorsubDec -E, vector<ne ne' dec t> |- :E_vector_subrange: exp1[ exp2 : exp3 ] : vector<ne7 ne'7 dec u> gives exp'1[exp'2:exp'3], I1 u+ I2 u+ I3 u+ <{ne <= ne4, ne >= ne'4,ne'<=ne'6+(-ne4),ne4' >= ne2, ne'6+(-ne4) <= ne'2},pure>,E_t +E, vector<ne ne' dec t> |- :E_vector_subrange: exp1[ exp2 .. exp3 ] : vector<ne7 ne'7 dec u> gives exp'1[exp'2:exp'3], I1 u+ I2 u+ I3 u+ <{ne <= ne4, ne >= ne'4,ne'<=ne'6+(-ne4),ne4' >= ne2, ne'6+(-ne4) <= ne'2},pure>,E_t E, vector<ne ne' inc t> |- exp : vector< ne1 ne2 inc u> gives exp',I,E_t E, range<ne'1 ne'2> |- exp1 : range<ne3 ne4> gives exp'1,I1,E_t @@ -846,26 +857,43 @@ E,t |- exp2 : u gives exp'2,I2,E_t ------------------------------------------------------------ :: vectorupDec E, vector<ne ne' dec t> |- [ exp with exp1 = exp2 ] : vector< ne1 ne2 dec u> gives [exp' with exp'1 = exp'2], I u+ I1 u+ I2 u+ <{ne1 >= ne3, ne2 >= ne4},pure>,E_t -E |- exp : vector ne1 ne2 order t gives I,E_t -E |- exp1 : enum ne3 ne4 order gives I1,E_t -E |- exp2 : enum ne5 ne6 order gives I2,E_t -E |- exp3 : vector ne7 ne8 order t gives I3,E_t ------------------------------------------------------------- :: vecrangeup -E |- [ exp with exp1 : exp2 = exp3 ] : vector ne1 ne2 order t gives I u+ I1 u+ I2 u+ I3 u+ <{ne1 <= ne3, ne1 <= ne5,ne3+ne4 <= ne5, ne1 + ne2 <= ne5 + ne6 + (- ne3) + (- ne4), ne7 + ne8 = ne1 + ne2 + (- ne3) + (- ne4)},pure>,E_t - -E |- exp : vector ne1 ne2 order t gives I,E_t -E |- exp1 : enum ne3 ne4 order gives I1,E_t -E |- exp2 : enum ne5 ne6 order gives I2,E_t -E |- exp3 : t gives I3,E_t ------------------------------------------------------------- :: vecrangeupvalue -E |- [ exp with exp1 : exp2 = exp3 ] : vector ne1 ne2 order t gives I u+ I1 u+ I2 u+ I3 u+ <{ne1 <= ne3, ne1 <= ne5,ne3+ne4 <= ne5, ne1 + ne2 <= ne5 + ne6 + (- ne3) + (- ne4)},pure>,E_t - - -E_r (id t_args) gives </idi : ti//i/> id : u </id'j : t'j//j/> -<E_t,<E_k,E_r,E_e>>,t'' |- exp : id t_args gives exp', I,E_t +E,vector<ne1 ne2 order t> |- exp : vector< ne3 ne4 inc u> gives exp',I,E_t +E,atom<ne5> |- exp1 : atom<ne6> gives exp1',I1,E_t +E,atom<ne7> |- exp2 : atom<ne8> gives exp2', I2,E_t +E,vector<ne9 ne10 inc t> |- exp3 : vector <ne11 ne12 inc u> gives exp3',I3,E_t +I4 == <{ ne3 <= ne5, ne3+ne4 <= ne7, ne12 = ne8 + (-ne6) , ne6 + one <= ne8},pure> +------------------------------------------------------------ :: vecrangeupInc +E,vector<ne1 ne2 order t> |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector <ne3 ne4 inc u> gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t + +E,vector<ne1 ne2 order t> |- exp : vector< ne3 ne4 inc u> gives exp',I,E_t +E,atom<ne5> |- exp1 : atom<ne6> gives exp1',I1,E_t +E,atom<ne7> |- exp2 : atom<ne8> gives exp2', I2,E_t +E,u |- exp3 : u' gives exp3',I3,E_t +I4 == <{ ne3 <= ne5, ne3+ne4 <= ne7 },pure> +------------------------------------------------------------ :: vecrangeupvalueInc +E,vector<ne1 ne2 order t> |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector <ne3 ne4 inc u> gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t + +E,vector<ne1 ne2 order t> |- exp : vector< ne3 ne4 dec u> gives exp',I,E_t +E,atom<ne5> |- exp1 : atom<ne6> gives exp1',I1,E_t +E,atom<ne7> |- exp2 : atom<ne8> gives exp2', I2,E_t +E,vector<ne9 ne10 dec t> |- exp3 : vector <ne11 ne12 dec u> gives exp3',I3,E_t +I4 == <{ ne5 <= ne3, ne3+(-ne4) <= ne6+(-ne8), ne8+one<=ne6 },pure> +------------------------------------------------------------ :: vecrangeupDec +E,vector<ne1 ne2 order t> |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector <ne3 ne4 dec u> gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t + +E,vector<ne1 ne2 order t> |- exp : vector< ne3 ne4 dec u> gives exp',I,E_t +E,atom<ne5> |- exp1 : atom<ne6> gives exp1',I1,E_t +E,atom<ne7> |- exp2 : atom<ne8> gives exp2', I2,E_t +E,u |- exp3 : u' gives exp3',I3,E_t +I4 == <{ ne5 <= ne3, ne3+(-ne4) <= ne6+(-ne8), ne8+one<=ne6 },pure> +------------------------------------------------------------ :: vecrangeupvalueDec +E,vector<ne1 ne2 order t> |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector <ne3 ne4 dec u> gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t + +E_r (x<t_args>) gives </idi : ti//i/> id : u </id'j : t'j//j/> +<E_t,<E_k,E_a,E_r,E_e>>,t'' |- exp : x< t_args> gives exp', I,E_t E_d,t |- exp'.id : u gives t', exp1', S_N', effect ------------------------------------------------------------ :: field -<E_t,<E_k,E_r,E_e>>,t |- exp.id : u gives exp1',I u+ <S_N',effect>,E_t +<E_t,<E_k,E_a,E_r,E_e>>,t |- exp.id : u gives exp1',I u+ <S_N',effect>,E_t <E_t,E_d>,t'' |- exp : u gives exp',I,E_t </<E_t,E_d>,u |- pati : u'i gives pat'i,E_ti,S_Ni//i/> @@ -874,94 +902,108 @@ E_d,t |- exp'.id : u gives t', exp1', S_N', effect <E_t,E_d>,t |- switch exp { </case pati -> expi//i/> }: u gives switch exp' { </case pat'i -> exp'i//i/> }, I u+ </Ii u+ <S_Ni,pure>//i/>, E_t <E_t,E_d>,t'' |- exp : u gives exp',I,E_t -E_d |- typ |-> t' +E_d |- typ ~> t' E_d,t' |- exp' : u gives u', exp'', S_N,effect E_d,t |- exp'' : t' gives u'', exp''', S_N', effect' ------------------------------------------------------------ :: typed -<E_t,E_d>,t |- (typ) exp : t gives exp''',Iu+<S_N u+ S_N',effect u+ effect'>,E_t +<E_t,E_d>,t |- (typ) exp : t gives exp''',I u+ <S_N u+ S_N',effect u+ effect'>,E_t <E_t,E_d> |- letbind gives E_t1, S_N, effect, {} -<(E_t u+ E_t1),E_d> |- exp : t gives I2, E_t2 +<(E_t u+ E_t1),E_d>,t |- exp : u gives exp', I2, E_t2 ------------------------------------------------------------ :: let -<E_t,E_d> |- letbind in exp : t gives <S_N,effect> u+ I2, E_t +<E_t,E_d>,t |- letbind in exp : t gives exp', <S_N,effect> u+ I2, E_t -E |- exp1 : t1 gives I1,E_t .... E |- expn : tn gives In,E_t +E,t1 |- exp1 : u1 gives exp1',I1,E_t1 .... E,tn |- expn : un gives expn',In,E_tn ------------------------------------------------------------ :: tup -E |- (exp1, .... , expn) : (t1 * .... * tn) gives I1 u+ .... u+ In,E_t +E,(t1, ...., tn) |- (exp1, .... , expn) : (u1 , .... , un) gives (exp1', ...., expn'), I1 u+ .... u+ In,E_t -E |- exp1 : t gives I1,E_t .. E |- expn : t gives In,E_t +<E_t,E_d>,t |- exp1 : u1 gives exp1', I1,E_t1 .. <E_t,E_d>,t |- expn : un gives expn', In,E_tn +E_d |- u1 ~< t,S_N1 .. E_d |- un ~< t,S_Nn ------------------------------------------------------------ :: list -E |- [||exp1, .., expn ||] : list t gives I1 u+ .. u+ In,E_t +<E_t,E_d>,list<t> |- [||exp1, .., expn ||] : list<u> gives [|| exp1', .., expn' ||], <S_N1 u+ .. u+ S_Nn,pure> u+ I1 u+ .. u+ In, E_t -E |- exp1 : bool gives I1,E_t -E |- exp2 : t gives I2,E_t2 -E |- exp3 : t gives I3,E_t3 +E,bit |- exp1 : bit gives exp1',I1,E_t' +E,t |- exp2 : u1 gives exp2',I2,E_t2 +E,t |- exp3 : u2 gives exp3',I3,E_t3 +E_d |- u1 ~< t,S_N1 +E_d |- u2 ~< t,S_N2 ------------------------------------------------------------ :: if -E |- if exp1 then exp2 else exp3 : t gives I1 u+ I2 u+ I3,(E_t2 inter E_t3) +<E_t,E_d>,t |- if exp1 then exp2 else exp3 : u gives if exp1' then exp2' else exp3', <S_N1 u+ S_N2,pure> u+ I1 u+ I2 u+ I3,(E_t2 inter E_t3) -<E_t,E_d> |- exp1 : enum ne1 ne2 order gives I1,E_t -<E_t,E_d> |- exp2 : enum ne3 ne4 order gives I2,E_t -<E_t,E_d> |- exp3 : enum ne5 ne6 order gives I3,E_t -<(E_t u+ {id |-> enum ne1 ne3+ne4 order}),E_d> |- exp4 : t gives I4,(E_t u+ {id |-> enum ne1 ne3+ne4 order}) +<E_t,E_d>,range<ne1 ne2> |- exp1 : range< ne7 ne8> gives exp1', I1,E_t +<E_t,E_d>,range<ne3 ne4> |- exp2 : range< ne9 ne10> gives exp2', I2,E_t +<E_t,E_d>,range<ne5 ne6> |- exp3 : range< ne11 ne12> gives exp3',I3,E_t +<(E_t u+ {id |-> range< ne1 ne4>}),E_d>,unit |- exp4 : t gives exp4',I4,E_t' ----------------------------------------------------------- :: for -<E_t,E_d> |- foreach id from exp1 to exp2 by exp3 exp4 : t gives I1 u+ I2 u+ I3 u+ I4 u+ <{ne1 <= ne3+ne4},pure>,E_t +<E_t,E_d>,unit |- foreach (id from exp1 to exp2 by exp3) exp4 : t gives foreach (id from exp1' to exp2' by exp3') exp4', I1 u+ I2 u+ I3 u+ I4 u+ <{ne1 <= ne3+ne4},pure>,E_t -E |- exp1 : t gives I1,E_t -E |- exp2 : list t gives I2,E_t +E,t |- exp1 : u gives exp1',I1,E_t +E,list<t> |- exp2 : list<u> gives exp2',I2,E_t ------------------------------------------------------------ :: cons -E |- exp1 :: exp2 : list t gives I1 u+ I2,E_t +E,list<t> |- exp1 :: exp2 : list<u> gives exp1'::exp2', I1 u+ I2,E_t -|- lit : t +t |- lit : u => exp,S_N ------------------------------------------------------------ :: lit -<E_t,E_d> |- lit : t gives Ie,E_t +E,t |- lit : u gives exp,<S_N,pure>,E_t -<E_t,E_d> |- exp : t gives I, E_t1 +<E_t,E_d>,unit |- exp : unit gives exp', I, E_t1 ------------------------------------------------------------ :: blockbase -<E_t,E_d> |- { exp } : unit gives I, E_t +<E_t,E_d>,unit |- { exp } : unit gives {exp'}, I, E_t -<E_t,E_d> |- exp : u gives I1, E_t1 -<(E_t u+ E_t1),E_d> |- { </expi//i/> } : t gives I2, E_t2 +<E_t,E_d>,unit |- exp : unit gives exp', I1, E_t1 +<(E_t u+ E_t1),E_d>,unit |- { </expi//i/> } : unit gives {</expi'//i/>}, I2, E_t2 ------------------------------------------------------------ :: blockrec -<E_t,E_d> |- { exp ; </expi//i/> } : t gives I1 u+ I2, E_t +<E_t,E_d>,unit |- { exp ; </expi//i/> } : unit gives {exp'; </expi'//i/>}, I1 u+ I2, E_t +<E_t,E_d>,unit |- exp : unit gives exp', I, E_t1 +------------------------------------------------------------ :: nondetbase +<E_t,E_d>,unit |- nondet { exp } : unit gives {exp'}, I, E_t -<E_t,E_d> |- nondet { exp ; </expi//i/> } : unit +<E_t,E_d>,unit |- exp : unit gives exp', I1, E_t1 +<(E_t u+ E_t1),E_d>,unit |- nondet { </expi//i/> } : unit gives {</expi'//i/>}, I2, E_t2 +------------------------------------------------------------ :: nondetrec +<E_t,E_d>,unit |- nondet { exp ; </expi//i/> } : unit gives {exp'; </expi'//i/>}, I1 u+ I2, E_t -E |- exp:t gives I1, E_t1 -E |- lexp:t gives I2, E_t2 +E,t |- exp:u gives exp', I1, E_t1 +E |- lexp:t gives lexp', I2, E_t2 ------------------------------------------------------------ :: assign -E |- lexp := exp : unit gives I u+ I2, E_t2 +E,unit |- lexp := exp : unit gives lexp' := exp', I u+ I2, E_t2 defn -E |- lexp : t gives I , E_t :: :: check_lexp :: check_lexp_ +E |- lexp : t gives lexp' , I , E_t :: :: check_lexp :: check_lexp_ {{ com Check the left hand side of an assignment }} by -E_t(id) gives register t +E_t(id) gives register<t> ---------------------------------------------------------- :: wreg -<E_t,E_d> |- id : t gives <{},{ wreg }>, E_t +<E_t,E_d> |- id : t gives id,<{},{ wreg }>, E_t -E_t(id) gives reg t +E_t(id) gives reg<t> ---------------------------------------------------------- :: wlocl -<E_t,E_d> |- id : t gives Ie, E_t +<E_t,E_d> |- id : t gives id,Ie, E_t E_t(id) gives t ---------------------------------------------------------- :: var -<E_t,E_d> |- id : t gives Ie,E_t +<E_t,E_d> |- id : t gives id,Ie,E_t id NOTIN dom(E_t) ---------------------------------------------------------- :: wnew -<E_t,E_d> |- id : t gives Ie, {id |-> reg t} +<E_t,E_d> |- id : t gives id,Ie, {id |-> reg<t>} -E_t(id) gives t1 -> t {</base_effecti//i/>, wmem, </base_effect'j//j/>} Extern {} -<E_t,E_d> |- exp : t1 gives I,E_t1 +E_t(id) gives E_k, S_N, Extern, t1 -> t {</base_effecti//i/>, wmem, </base_effect'j//j/>} +<E_t,E_d>,t1 |- exp : u1 gives exp',I,E_t1 ---------------------------------------------------------- :: wmem -<E_t,E_d> |- :LEXP_memory: id(exp) : t gives I u+ <{},{wmem}>,E_t +<E_t,E_d> |- :LEXP_memory: id(exp) : t gives :LEXP_memory: id(exp'),I u+ <S_N,{wmem}>,E_t + +E,atom<ne> |- exp : u gives exp',I1,E_t +E |- lexp : vector<ne1 ne2 inc t> gives lexp',I2,E_t +---------------------------------------------------------- :: wbitInc +E |- lexp [exp] : t gives lexp'[exp'], I1 u+ I2 u+ <{ne1 <= ne, ne1 + ne2 >= ne},pure>,E_t -E |- exp : enum ne1 ne2 order gives I1,E_t -E |- lexp : vector ne3 ne4 order t gives I2,E_t ----------------------------------------------------------- :: wbit -E |- lexp [exp] : t gives I1 u+ I2 u+ <{ne3 <= ne1, ne1 + ne2 <= ne3 + ne4},pure>,E_t +E,atom<ne> |- exp : u gives exp',I1,E_t +E |- lexp : vector<ne1 ne2 dec t> gives lexp',I2,E_t +---------------------------------------------------------- :: wbitDec +E |- lexp [exp] : t gives lexp'[exp'], I1 u+ I2 u+ <{ne <= ne1, ne1 + (-ne2) <= ne},pure>,E_t E |- exp1 : enum ne1 ne2 order gives I1,E_t E |- exp2 : enum ne3 ne4 order gives I2,E_t |