(* Names *)

Parameter name: Set.

(* Capabilities *)

Inductive cap: Set :=
    name2cap : name -> cap
  | In : cap -> cap
  | Out : cap -> cap
  | to : cap -> cap
  | path : cap -> cap -> cap.

Inductive notin_name_cap [m:name]: cap -> Prop :=
    notin_name_cap_name : (n:name)~m=n -> (notin_name_cap m (name2cap n))
  | notin_name_cap_in   : (M:cap)(notin_name_cap m M) ->
                          (notin_name_cap m (In M))
  | notin_name_cap_out  : (M:cap)(notin_name_cap m M) ->
                          (notin_name_cap m (Out M))
  | notin_name_cap_to   : (M:cap)(notin_name_cap m M) ->
                          (notin_name_cap m (to M))
  | notin_name_cap_path : (M,N:cap)(notin_name_cap m M) ->
                          (notin_name_cap m N) ->
                          (notin_name_cap m (path M N)).

Inductive isin_name_cap [m:name]: cap -> Prop :=
    isin_name_cap_name : (isin_name_cap m (name2cap m))
  | isin_name_cap_in   : (M:cap)(isin_name_cap m M) ->
                         (isin_name_cap m (In M))
  | isin_name_cap_out  : (M:cap)(isin_name_cap m M) ->
                         (isin_name_cap m (Out M))
  | isin_name_cap_to   : (M:cap)(isin_name_cap m M) ->
                         (isin_name_cap m (to M))
  | isin_name_cap_path : (M,N:cap)
                         (isin_name_cap m M) \/ (isin_name_cap m N) ->
                         (isin_name_cap m (path M N)).

(* Groups *)

Parameter group : Set.

(* Lists of groups *)

Inductive Glist : Set :=
   emptyG : Glist
 | consG  : group -> Glist -> Glist.

Inductive Glist_notin [x:group] : Glist -> Prop :=
   Glist_notin_emptyG : (Glist_notin x emptyG)
 | Glist_notin_consG  : (y:group)(l:Glist)
                        ~x=y -> (Glist_notin x l) ->
                        (Glist_notin x (consG y l)).

Inductive Glist_isin [x:group] : Glist -> Prop :=
   Glist_isin_group : (Glist_isin x (consG x emptyG))
 | Glist_isin_consG : (y:group)(l:Glist)
                      x=y \/ (Glist_isin x l) ->
                      (Glist_isin x (consG y l)).

(* Message types and exchange types *)

Inductive msgType : Set :=
    amb_type : group -> msgType
  | cap_type : group -> group -> msgType.

Inductive comType : Set :=
    Shh : comType
  | msg : msgType -> comType.

Inductive notin_group_msgType [g:group] : msgType -> Prop :=
    notin_group_msgType_amb_type  : (h:group)~g=h ->
                                    (notin_group_msgType g (amb_type h))
  | notin_group_msgType_cap_type  : (h,h':group)~g=h -> ~g=h' ->
                                    (notin_group_msgType g (cap_type h h')).

Inductive notin_group_comType [g:group] : comType -> Prop :=
    notin_group_comType_Shh        : (notin_group_comType g Shh)
  | notin_group_comType_msg        : (W:msgType)
                                    (notin_group_msgType g W) ->
                                    (notin_group_comType g (msg W)).

Inductive isin_group_msgType [g:group] : msgType -> Prop :=
    isin_group_msgType_amb_type  : (h:group)(T:comType)g=h ->
                                   (isin_group_msgType g (amb_type h))
  | isin_group_msgType_cap_type  : (h,h':group)g=h \/ g=h' ->
                                   (isin_group_msgType g (cap_type h h')).

Inductive isin_group_comType [g:group] : comType -> Prop :=
    isin_group_comType_msg       : (W:msgType)
                                   (isin_group_msgType g W) ->
                                   (isin_group_comType g (msg W)).

Inductive groupType: Set :=
  gr: Glist -> Glist -> Glist -> comType -> groupType.

(* Processes *)

Mutual Inductive proc: Set :=
    nil : proc
  | action : cap -> proc -> proc
  | output : cap -> proc -> proc
  | input : (name -> proc) -> msgType -> proc
  | par : proc -> proc -> proc
  | ambient : cap -> proc -> proc
  | bang : proc -> proc
  | nu : group -> (name -> proc) -> proc
  | nuG : res -> proc
with res: Set :=
    proc2res : proc -> res
  | resG : groupType -> (group -> res) -> res.

Parameter type_group: group -> groupType -> Prop.
Parameter type_name: name -> msgType -> Prop.

Definition inclist:= [l1:Glist][l2:Glist](g:group)(Glist_isin g l1) -> (Glist_isin g l2).

Inductive good_msg : cap -> msgType -> Prop :=
    good_msg_exp_n    : (n:name)(g:group)
                        (type_name n (amb_type g)) -> (good_msg (name2cap n) (amb_type g))
  | good_exp_in       : (M:cap)(g1,g2:group)(S,C,E:Glist)(T:comType)
                        (type_group g2 (gr S C E T)) ->
                        (good_msg M (amb_type g1)) ->
                        (Glist_isin g1 C) ->
                        (good_msg (In M) (cap_type g2 g2))
  | good_exp_out      : (M:cap)(g1,g2:group)
                        (S1,S2,C1,C2,E1,E2:Glist)(T1,T2:comType)
                        (type_group g1 (gr S1 C1 E1 T1)) ->
                        (type_group g2 (gr S2 C2 E2 T2)) ->
                        (good_msg M (amb_type g1)) ->
                        (Glist_isin g1 C2) ->
                        (inclist S1 S2) ->
                        (good_msg (Out M) (cap_type g2 g2))
  | good_exp_to       : (M:cap)(g1,g2:group)(S,C,E:Glist)(T:comType)
                        (type_group g2 (gr S C E T)) ->
                        (good_msg M (amb_type g1)) ->
                        (Glist_isin g1 E) ->
                        (good_msg (to M) (cap_type g1 g2))
  | good_msg_exp_path : (M,M':cap)(g1,g2,g3:group)
                        (good_msg M (cap_type g3 g2)) ->
                        (good_msg M' (cap_type g1 g3)) ->
                        (good_msg (path M M') (cap_type g1 g2)).

Inductive good_proc : proc -> group -> Prop :=
    good_proc_nil     : (g:group)(good_proc nil g)
  | good_proc_prefix  : (M:cap)(g1,g2:group)(P:proc)
                        (good_msg M (cap_type g1 g2)) -> (good_proc P g1) ->
                        (good_proc (action M P) g2)
  | good_proc_input   : (P:name->proc)(W:msgType)(g:group)(S,C,E:Glist)
                        ((x:name)(type_name x W) -> (good_proc (P x) g)) ->
                        (type_group g (gr S C E (msg W))) ->
                        (good_proc (input P W) g)
  | good_proc_output  : (P:proc)(M:cap)(W:msgType)(g:group)(S,C,E:Glist)
                        (good_proc P g) ->
                        (good_msg M W) ->
                        (type_group g (gr S C E (msg W))) ->
                        (good_proc (output M P) g)
  | good_proc_amb     : (P:proc)(S,C,E:Glist)(M:cap)(g,g':group)(T:comType)
                        (good_proc P g) ->
                        (good_msg M (amb_type g)) ->
                        (type_group g (gr S C E T)) ->
                        (Glist_isin g' S) ->
                        (good_proc (ambient M P) g')
  | good_proc_par     : (P,Q:proc)(g:group)
                        (good_proc P g) -> (good_proc Q g) ->
                        (good_proc (par P Q) g)
  | good_proc_repl    : (P:proc)(g:group)
                        (good_proc P g) -> (good_proc (bang P) g)
  | good_proc_res     : (P:name->proc)(g,g':group)
                        ((m:name)(type_name m (amb_type g')) -> (good_proc (P m) g)) ->
                        (good_proc (nu g' P) g)
with good_res : res -> group -> Prop :=
    good_res_proc2res : (P:proc)(g:group)
                        (good_proc P g) -> (good_res (proc2res P) g)
  | good_res_Gres     : (P:group->res)(g:group)(G:groupType)
                        ((g':group)~g=g' -> (type_group g' G) ->
                         (good_res (P g') g)
                        ) -> (good_res (resG G P) g).

Inductive star_group : Set :=
   simple : group -> star_group
 | star   : group -> star_group.

Inductive starGlist : Set :=
   starEmptyG : starGlist
 | starConsG  : star_group -> starGlist -> starGlist.

Inductive starGlist_notin [x:star_group] : starGlist -> Prop :=
   starGlist_notin_emptyG : (starGlist_notin x starEmptyG)
 | starGlist_notin_consG  : (y:star_group)(l:starGlist)
                            ~x=y -> (starGlist_notin x l) ->
                            (starGlist_notin x (starConsG y l)).

Inductive starGlist_isin [x:star_group] : starGlist -> Prop :=
   starGlist_isin_group : (starGlist_isin x (starConsG x starEmptyG))
 | starGlist_isin_consG : (y:star_group)(l:starGlist)
                          x=y \/ (starGlist_isin x l) ->
                          (starGlist_isin x (starConsG y l)).

Definition inc_starGlist:= [l1:starGlist][l2:starGlist](g:star_group)(starGlist_isin g l1) -> (starGlist_isin g l2).

Inductive starGroupType: Set :=
  gr_star: starGlist -> Glist -> Glist -> comType -> starGroupType.

Fixpoint star_clear[l:starGlist]: Glist :=
  Cases l of
      starEmptyG => emptyG
    | (starConsG (simple g) l') => (consG g (star_clear l'))
    | (starConsG (star g) l') => (consG g (star_clear l'))
  end.

Fixpoint append_starGlist[l:starGlist]: starGlist -> starGlist :=
  [l':starGlist]Cases l of
                    starEmptyG => l'
                  | (starConsG g l'') => (starConsG g (append_starGlist l'' l'))
                end.

Fixpoint append_Glist[l:Glist]: Glist -> Glist :=
  [l':Glist]Cases l of
                emptyG => l'
             | (consG g l'') => (consG g (append_Glist l'' l'))
            end.

Inductive env: Set :=
   emptyE: env
 | consEgroup: group -> starGroupType -> env -> env
 | consEname: name -> msgType -> env -> env.

Fixpoint append_env[e:env]: env -> env :=
  [e':env]Cases e of
              emptyE => e'
            | (consEgroup g gt e'') => (consEgroup g gt (append_env e'' e'))
            | (consEname n W e'') => (consEname n W (append_env e'' e'))
          end.

Inductive remove_group: env -> group -> env -> Prop :=
    empty_remove: (g:group)(remove_group emptyE g emptyE)
  | group_remove1: (e,e':env)(g:group)(t:starGroupType)(remove_group e g e') -> (remove_group (consEgroup g t e) g e')
  | group_remove2: (e,e':env)(g,g':group)(t:starGroupType)(remove_group e g' e') -> ~g=g' -> (remove_group (consEgroup g t e) g' (consEgroup g t e'))
  | name_remove: (e,e':env)(n:name)(W:msgType)(g:group)(remove_group e g e') -> (remove_group (consEname n W e) g (consEname n W e')).

Inductive add_S: group -> starGlist -> env -> starGlist -> Prop :=
    add_S_empty: (g:group)(S:starGlist)(add_S g S emptyE S)
  | add_S_group1: (g:group)(S,S',S'':starGlist)(C,E:Glist)(t:comType)(e:env)(add_S g S e S') -> (add_S g S (consEgroup g (gr_star S'' C E t) e) (append_starGlist S' S''))
  | add_S_group2: (g,g':group)(S,S':starGlist)(t:starGroupType)(e:env)~g=g' -> (add_S g S e S') -> (add_S g S (consEgroup g' t e) S')
  | add_S_name: (n:name)(W:msgType)(g:group)(S,S':starGlist)(e:env)(add_S g S e S') -> (add_S g S (consEname n W e) S').

Inductive add_C: group -> Glist -> env -> Glist -> Prop :=
    add_C_empty: (g:group)(C:Glist)(add_C g C emptyE C)
  | add_C_group1: (g:group)(S:starGlist)(C,C',C'',E:Glist)(t:comType)(e:env)(add_C g C e C') -> (add_C g C (consEgroup g (gr_star S C'' E t) e) (append_Glist C' C''))
  | add_C_group2: (g,g':group)(C,C':Glist)(t:starGroupType)(e:env)~g=g' -> (add_C g C e C') -> (add_C g C (consEgroup g' t e) C')
  | add_C_name: (n:name)(W:msgType)(g:group)(C,C':Glist)(e:env)(add_C g C e C') -> (add_C g C (consEname n W e) C').

Inductive add_E: group -> Glist -> env -> Glist -> Prop :=
    add_E_empty: (g:group)(E:Glist)(add_E g E emptyE E)
  | add_E_group1:(g:group)(S:starGlist)(C,E,E',E'':Glist)(t:comType)(e:env)(add_E g E e E')
    -> (add_E g E (consEgroup g (gr_star S C E'' t) e) (append_Glist E' E''))
  | add_E_group2: (g,g':group)(E,E':Glist)(t:starGroupType)(e:env)~g=g' -> (add_E g E e E') -> (add_E g E (consEgroup g' t e) E')
  | add_E_name: (n:name)(W:msgType)(g:group)(E,E':Glist)(e:env)(add_E g E e E') -> (add_E g E (consEname n W e) E').

Inductive union_env: env -> env -> env -> Prop :=
    trivial_union: (e:env)(union_env emptyE e e)
  | group_union: (e,e',e'',e''':env)(g:group)(S,S':starGlist)(C,C',E,E':Glist)(t:comType)
                 (remove_group e' g e''') -> (union_env e e''' e'') ->
                 (add_S g S e' S') ->
                 (add_C g C e' C') ->
                 (add_E g E e' E') ->
                 (union_env (consEgroup g (gr_star S C E t) e) e' (consEgroup g (gr_star S' C' E' t) e''))
  | name_union: (e,e',e'':env)(n:name)(W:msgType)(union_env e e' e'') -> (union_env (consEname n W e) e' (consEname n W e'')).

Inductive name_in_env: name -> msgType -> env -> Prop :=
    name_in_env1: (n:name)(W:msgType)(g:group)(t:starGroupType)(e:env)(name_in_env n W e) -> (name_in_env n W (consEgroup g t e))
  | name_in_env2: (n,n':name)(W,W':msgType)(e:env)~n=n' \/ ~W=W' -> (name_in_env n W e) -> (name_in_env n W (consEname n' W' e))
  | name_in_env3: (n:name)(W:msgType)(e:env)(name_in_env n W (consEname n W e)).

Inductive group_in_env: group -> starGroupType -> env -> Prop :=
    group_in_env1: (n:name)(W:msgType)(g:group)(t:starGroupType)(e:env)(group_in_env g t e) -> (group_in_env g t (consEname n W e))
  | group_in_env2: (g,g':group)(t,t':starGroupType)(e:env)~g=g' \/ ~t=t' -> (group_in_env g t e) -> (group_in_env g t (consEgroup g' t' e))
  | group_in_env3: (g:group)(t:starGroupType)(e:env)(group_in_env g t (consEgroup g t e)).

Definition unify_env : env -> env -> Prop :=
[e1:env][e2:env]
((n:name)(W1,W2:msgType)(name_in_env n W1 e1) -> (name_in_env n W2 e2) -> W1=W2) /\
((g:group)(S1,S2:starGlist)(C1,C2,E1,E2:Glist)(t1,t2:comType)
 (group_in_env g (gr_star S1 C1 E1 t1) e1) -> (group_in_env g (gr_star S2 C2 E2 t2) e2) -> t1=t2).

Inductive closure: starGlist -> Glist -> env -> Prop :=
    elim_star: (l:starGlist)(e:env)((g:group)(S:starGlist)(C,E:Glist)(t:comType)(starGlist_isin (star g) l) /\ (group_in_env g (gr_star S C E t) e) -> (inc_starGlist S l)) -> (closure l (star_clear l) e)
  | add_grp: (l,S:starGlist)(C,E,l':Glist)(t:comType)(g:group)(e:env)(starGlist_isin (star g) l) -> (group_in_env g (gr_star S C E t) e) -> ~(inc_starGlist S l) -> (closure (append_starGlist l S) l' e) -> (closure l l' e).

Axiom TYPE_NAME: (n:name)(g:group)(e:env)(name_in_env n (amb_type g) e) -> (type_name n (amb_type g)).

Axiom TYPE_GROUP: (g:group)(S:starGlist)(C,E:Glist)(t:comType)(e:env)(group_in_env g (gr_star S C E t) e) -> (S':Glist)(closure S S' e) -> (type_group g (gr S' C E t)).

Inductive msg_inf: cap -> msgType -> env -> Prop :=
    msg_inf_name : (x:name)(g:group)
                   (msg_inf (name2cap x) (amb_type g) (consEname x (amb_type g) emptyE))
  | msg_inf_to   : (x:name)(g1,g2:group)(t:comType)
                   (msg_inf (to (name2cap x)) (cap_type g1 g2)
                     (consEname x (amb_type g1)
                     (consEgroup g2 (gr_star starEmptyG emptyG (consG g1 emptyG) t) emptyE))
                   )
  | msg_inf_in   : (x:name)(g1,g2:group)(t:comType)
                   (msg_inf (In (name2cap x)) (cap_type g2 g2)
                     (consEname x (amb_type g1)
                     (consEgroup g2 (gr_star (starConsG (simple g1) starEmptyG) (consG g1 emptyG) emptyG t) emptyE))
                   )
  | msg_inf_out  : (x:name)(g1,g2:group)(t:comType)
                   (msg_inf (Out (name2cap x)) (cap_type g2 g2)
                     (consEname x (amb_type g1)
                     (consEgroup g1 (gr_star starEmptyG emptyG emptyG t)
                     (consEgroup g2 (gr_star (starConsG (star g1) starEmptyG) (consG g1 emptyG) emptyG t) emptyE)))
                   )
  | msg_inf_path : (M,N:cap)(g1,g2,g3:group)(W,W':msgType)(e1,e2,e3:env)
                   (msg_inf M W e1) -> (msg_inf N W' e2) ->
                   W=(cap_type g1 g2) -> W'=(cap_type g3 g1) ->
                   (unify_env e1 e2) ->
                   (union_env e1 e2 e3) ->
                   (msg_inf (path M N) (cap_type g3 g2) e3).

Lemma MSG_INF_SOUND: (M:cap)(W:msgType)(e:env)(msg_inf M W e) -> (good_msg M W).

Proof.

Induction M; Intros.

Inversion H.
Apply good_msg_exp_n.
Apply TYPE_NAME with (consEname n (amb_type g) emptyE).
Apply name_in_env3.

Inversion H0.
Apply good_exp_in with g1 (consG g1 emptyG) (consG g1 emptyG) emptyG t.
Apply TYPE_GROUP with (starConsG (simple g1) starEmptyG) e.
Rewrite <-H3; Apply group_in_env1.
Apply group_in_env3.
Cut (star_clear (starConsG (simple g1) starEmptyG))=(consG g1 emptyG); [Intro | Auto].
Rewrite <-H4; Apply elim_star; Intros.
Inversion_clear H5; Inversion_clear H6; Inversion_clear H5; Inversion_clear H6.
Apply good_msg_exp_n.
Apply TYPE_NAME with e.
Rewrite <-H3; Apply name_in_env3.
Apply Glist_isin_group.

Inversion H0.
Apply good_exp_out with g1 emptyG (consG g1 emptyG) emptyG (consG g1 emptyG) emptyG emptyG t t.
Apply TYPE_GROUP with starEmptyG e.
Rewrite <-H3; Apply group_in_env1; Apply group_in_env3.
Cut (star_clear starEmptyG)=emptyG; [Intro | Auto].
Rewrite <-H4; Apply elim_star; Intros.
Inversion_clear H5; Inversion_clear H6.
Apply TYPE_GROUP with (starConsG (star g1) starEmptyG) e.
Rewrite <-H3; Apply group_in_env1; Apply group_in_env2.
Right; Unfold not; Intros.
Inversion_clear H4.
Apply group_in_env3.
Cut (star_clear (starConsG (star g1) starEmptyG))=(consG g1 emptyG); [Intro | Auto].
Rewrite <-H4; Apply elim_star; Intros.
Inversion_clear H5.
Inversion H6.
Rewrite H8 in H7; Rewrite <-H3 in H7; Inversion H7.
Inversion H11.
Inversion_clear H18.
Absurd g1=g1; Auto.
Inversion H20.
Inversion_clear H27.
Unfold inc_starGlist; Intros; Assumption.
Unfold inc_starGlist; Intros.
Apply starGlist_isin_consG; Right; Assumption.
Inversion_clear H8.
Inversion H10.
Rewrite H11 in H7; Rewrite <-H3 in H7; Inversion H7.
Inversion H14.
Inversion_clear H21.
Absurd g1=g1; Auto.
Inversion H23.
Inversion_clear H30.
Unfold inc_starGlist; Intros; Assumption.
Unfold inc_starGlist; Intros.
Apply starGlist_isin_consG; Right; Assumption.
Inversion_clear H10.
Apply good_msg_exp_n; Apply TYPE_NAME with e.
Rewrite <-H3; Apply name_in_env3.
Apply Glist_isin_group.
Unfold inclist; Intros.
Apply Glist_isin_consG; Right; Assumption.

Inversion H0.
Apply good_exp_to with emptyG emptyG (consG g1 emptyG) t.
Apply TYPE_GROUP with starEmptyG e.
Rewrite <-H3; Apply group_in_env1.
Apply group_in_env3.
Cut (star_clear starEmptyG)=emptyG; [Intro | Auto].
Rewrite <-H4; Apply elim_star; Intros.
Inversion_clear H5; Inversion_clear H6.
Apply good_msg_exp_n.
Apply TYPE_NAME with e.
Rewrite <-H3; Apply name_in_env3.
Apply Glist_isin_group.

Inversion H1.
Apply good_msg_exp_path with g1; [Rewrite H6 in H4; Apply H with e1 | Rewrite H7 in H5; Apply H0 with e2]; Auto.

Qed.

(* Raw processes *)

Inductive raw_proc: Set :=
   raw_nil : raw_proc
 | raw_action : cap -> raw_proc -> raw_proc
 | raw_output : cap -> raw_proc -> raw_proc
 | raw_input : (name -> raw_proc) -> raw_proc
 | raw_par : raw_proc -> raw_proc -> raw_proc
 | raw_ambient : cap -> raw_proc -> raw_proc
 | raw_bang : raw_proc -> raw_proc
 | raw_nu : (name -> raw_proc) -> raw_proc.

Inductive proc_inf: raw_proc -> proc -> group -> env -> Prop :=
    proc_inf_null   : (g:group)(t:comType)(proc_inf raw_nil nil g (consEgroup g (gr_star starEmptyG emptyG emptyG t) emptyE))
  | proc_inf_prefix : (M:cap)(W:msgType)(e1,e2,e3:env)(R:raw_proc)(P:proc)(g1,g2,g3:group)
                      (msg_inf M W e1) -> (proc_inf R P g1 e2) ->
                      W=(cap_type g1 g2) -> 
                      (unify_env e1 e2) ->
                      (union_env e1 e2 e3) ->
                      (proc_inf (raw_action M R) (action M P) g2 e3)
  | proc_inf_input  : (W:msgType)(S:starGlist)(C,E:Glist)(t:comType)(R:name->raw_proc)(P:name->proc)(e:env)(g:group)
                      (group_in_env g (gr_star S C E t) e) -> t=(msg W) ->
                      ((x:name)(proc_inf (R x) (P x) g (consEname x (amb_type g) e))) ->
                      (proc_inf (raw_input R) (input P W) g e)
  | proc_inf_output : (R:raw_proc)(P:proc)(M:cap)(W:msgType)(g:group)(e1,e2,e3:env)
                      (proc_inf R P g e1) -> (msg_inf M W e2) ->
                      (unify_env e1 (consEgroup g (gr_star starEmptyG emptyG emptyG (msg W)) e2)) ->
                      (union_env e1 (consEgroup g (gr_star starEmptyG emptyG emptyG (msg W)) e2) e3) ->
                      (proc_inf (raw_output M R) (output M P) g e3)
  | proc_inf_par    : (R,R':raw_proc)(P,P':proc)(g1,g2:group)(e1,e2,e3:env)
                      (proc_inf R P g1 e1) -> (proc_inf R' P' g2 e2) ->
                      g1=g2 ->
                      (unify_env e1 e2) ->
                      (union_env e1 e2 e3) ->
                      (proc_inf (raw_par R R') (par P P') g2 e3)
  | proc_inf_amb    : (x:name)(W:msgType)(R:raw_proc)(P:proc)(g,g':group)(e,e':env)(t:comType)
                      (msg_inf (name2cap x) W (consEname x W emptyE)) -> (proc_inf R P g e) ->
                      W=(amb_type g) ->
                      (unify_env e (consEname x W (consEgroup g (gr_star (starConsG (simple g') starEmptyG) emptyG emptyG t) emptyE))) ->
                      (union_env e (consEname x W (consEgroup g (gr_star (starConsG (simple g') starEmptyG) emptyG emptyG t) emptyE)) e') -> 
                      (proc_inf (raw_ambient (name2cap x) R) (ambient (name2cap x) P) g' e')
  | proc_inf_res    : (R:name->raw_proc)(P:name->proc)(e:env)(g,g':group)
                      ((x:name)(proc_inf (R x) (P x) g (consEname x (amb_type g') e))) ->
                      (proc_inf (raw_nu R) (nu g' P) g e)
  | proc_inf_repl   : (R:raw_proc)(P:proc)(g:group)(e:env)(proc_inf R P g e) -> (proc_inf (raw_bang R) (bang P) g e).

Axiom dec_group: (g,h:group)g=h \/ ~g=h.

Lemma REMOVE_N: (e,e':env)(g:group)(remove_group e g e') ->
                (n:name)(W:msgType)(name_in_env n W e) ->
                (name_in_env n W e').

Proof.

Induction 1; Intros; Auto.

Inversion H2; Auto.

Apply name_in_env1; Apply H1; Inversion H3; Auto.

Inversion H2.
Apply name_in_env2; [Assumption | Apply H1; Auto].
Apply name_in_env3; Apply H1; Inversion H2; Auto.

Qed.

Lemma REMOVE_N2: (e,e':env)(g:group)(remove_group e g e') ->
                 (n:name)(W:msgType)(name_in_env n W e') ->
                 (name_in_env n W e).

Proof.

Induction 1; Intros; Auto.

Apply name_in_env1; Apply H1; Assumption.
Inversion H3; Apply name_in_env1; Apply H1; Assumption.

Inversion H2.
Apply name_in_env2; [Assumption | Apply H1; Assumption].
Apply name_in_env3.

Qed.

Lemma GLIST_DEC: (l,l':Glist)l=l' \/ ~l=l'.

Proof.

Induction l; Intros.

Case l'.
Left; Trivial.
Intros; Right; Unfold not; Intros.
Inversion_clear H.

Case l'.
Intros; Right; Unfold not; Intros.
Inversion_clear H0.
Intros; Elim (dec_group g g1); Elim (H g2); Intros.
Rewrite H0; Rewrite H1; Left; Trivial.
Right; Unfold not; Intros.
Inversion H2.
Absurd g0=g2; Assumption.
Right; Unfold not; Intros.
Inversion H2.
Absurd g=g1; Assumption.
Right; Unfold not; Intros.
Inversion H2.
Absurd g=g1; Assumption.

Qed.

Lemma STAR_GROUP_DEC: (s,s':star_group)s=s' \/ ~s=s'.

Proof.

Induction s; Intros.

Case s'.
Intro; Elim (dec_group g g0); Intros.
Rewrite H; Left; Trivial.
Right; Unfold not; Intros; Inversion H0; Absurd g=g0; Assumption.
Intro; Right; Unfold not; Intros.
Inversion_clear H.

Case s'.
Right; Unfold not; Intros.
Inversion_clear H.
Intro; Elim (dec_group g g0); Intros.
Rewrite H; Left; Trivial.
Right; Unfold not; Intros; Inversion H0; Absurd g=g0; Assumption.

Qed.

Lemma STAR_GLIST_DEC: (l,l':starGlist)l=l' \/ ~l=l'.

Proof.

Induction l; Intros.

Case l'.
Left; Trivial.
Intros; Right; Unfold not; Intros; Inversion_clear H.

Case l'.
Right; Unfold not; Intros; Inversion_clear H0.
Intros; Elim (STAR_GROUP_DEC s s1); Elim (H s2); Intros.
Rewrite H0; Rewrite H1; Left; Trivial.
Right; Unfold not; Intros; Inversion H2; Absurd s0=s2; Assumption.
Right; Unfold not; Intros; Inversion H2; Absurd s=s1; Assumption.
Right; Unfold not; Intros; Inversion H2; Absurd s=s1; Assumption.

Qed.

Lemma MSG_TYPE_DEC: (W,W':msgType)W=W' \/ ~W=W'.

Proof.

Intro; Pattern W; Apply msgType_ind; Intros.

Case W'.
Intro; Elim (dec_group g g0); Intros.
Rewrite H; Left; Trivial.
Right; Unfold not; Intros; Inversion H0; Absurd g=g0; Assumption.
Intros; Right; Unfold not; Intros; Inversion_clear H.

Case W'.
Intro; Right; Unfold not; Intros; Inversion_clear H.
Intros; Elim (dec_group g g1); Elim (dec_group g0 g2); Intros.
Rewrite H; Rewrite H0; Left; Trivial.
Right; Unfold not; Intros; Inversion H1; Absurd g0=g2; Assumption.
Right; Unfold not; Intros; Inversion H1; Absurd g=g1; Assumption.
Right; Unfold not; Intros; Inversion H1; Absurd g=g1; Assumption.

Qed.

Lemma COM_TYPE_DEC: (c,c':comType)c=c' \/ ~c=c'.

Proof.

Intro; Pattern c; Apply comType_ind; Intros; Auto.

Case c'.
Left; Trivial.
Intro; Right; Unfold not; Intros; Inversion_clear H.

Case c'.
Right; Unfold not; Intros; Inversion_clear H.
Intro; Elim (MSG_TYPE_DEC m m0); Intros.
Rewrite H; Left; Trivial.
Right; Unfold not; Intros; Inversion H0; Absurd m=m0; Assumption.

Qed.

Lemma STAR_GROUP_TYPE_DEC: (s,t:starGroupType)s=t \/ ~s=t.

Proof.

Induction s; Intros.

Case t.
Intros; Elim (STAR_GLIST_DEC s0 s1); Elim (GLIST_DEC g g1); Elim (GLIST_DEC g0 g2); Elim (COM_TYPE_DEC c c0); Intros.
Rewrite H; Rewrite H0; Rewrite H1; Rewrite H2; Left; Trivial.
Right; Unfold not; Intros; Inversion H3; Absurd c=c0; Assumption.
Right; Unfold not; Intros; Inversion H3; Absurd g0=g2; Assumption.
Right; Unfold not; Intros; Inversion H3; Absurd g0=g2; Assumption.
Right; Unfold not; Intros; Inversion H3; Absurd g=g1; Assumption.
Right; Unfold not; Intros; Inversion H3; Absurd g=g1; Assumption.
Right; Unfold not; Intros; Inversion H3; Absurd g=g1; Assumption.
Right; Unfold not; Intros; Inversion H3; Absurd g=g1; Assumption.
Right; Unfold not; Intros; Inversion H3; Absurd s0=s1; Assumption.
Right; Unfold not; Intros; Inversion H3; Absurd s0=s1; Assumption.
Right; Unfold not; Intros; Inversion H3; Absurd s0=s1; Assumption.
Right; Unfold not; Intros; Inversion H3; Absurd s0=s1; Assumption.
Right; Unfold not; Intros; Inversion H3; Absurd s0=s1; Assumption.
Right; Unfold not; Intros; Inversion H3; Absurd s0=s1; Assumption.
Right; Unfold not; Intros; Inversion H3; Absurd s0=s1; Assumption.
Right; Unfold not; Intros; Inversion H3; Absurd s0=s1; Assumption.

Qed.

Lemma REMOVE_G: (e,e':env)(g:group)(remove_group e g e') ->
                (g':group)(s:starGroupType)(group_in_env g' s e') ->
                (group_in_env g' s e).

Proof.

Induction 1; Intros; Auto.

Elim (dec_group g' g0); Elim (STAR_GROUP_TYPE_DEC s t); Intros.
Rewrite H3; Rewrite H4; Apply group_in_env3.
Apply group_in_env2.
Right; Assumption.
Apply H1; Assumption.
Apply group_in_env2.
Left; Assumption.
Apply H1; Assumption.
Apply group_in_env2.
Left; Assumption.
Apply H1; Assumption.

Inversion H3.
Apply group_in_env2; Auto.
Apply group_in_env3.

Inversion H2; Apply group_in_env1; Auto.

Qed.

Lemma REMOVE_G2: (e,e':env)(g:group)(remove_group e g e') ->
                 (g':group)~g=g' -> (s:starGroupType)(group_in_env g' s e) ->
                 (group_in_env g' s e').

Proof.

Induction 1; Intros; Auto.

Apply H1; Auto.
Inversion H3.
Assumption.
Absurd g'=g0; Auto.

Elim (dec_group g0 g'0); Elim (STAR_GROUP_TYPE_DEC s t); Intros.
Rewrite H5; Rewrite H6; Apply group_in_env3.
Apply group_in_env2.
Right; Assumption.
Apply H1; Inversion H4.
Assumption.
Auto.
Assumption.
Absurd s=t; Assumption.
Apply group_in_env2.
Left; Auto.
Apply H1; Inversion H4.
Assumption.
Auto.
Assumption.
Absurd g0=g'0; Auto.
Apply group_in_env2.
Left; Auto.
Apply H1; Inversion H4.
Assumption.
Auto.
Assumption.
Absurd s=t; Assumption.

Inversion H3; Apply group_in_env1; Apply H1; Assumption.

Qed.

Lemma UNIFY_LESS: (g:group)(s:starGroupType)(e,e',e'':env)
                  (unify_env (consEgroup g s e) e') ->
                  (remove_group e' g e'') ->
                  (unify_env e e'').

Proof.

Unfold unify_env; Intros; Split; Intros.

Inversion_clear H.
Apply H3 with n.
Apply name_in_env1; Assumption.
Apply REMOVE_N2 with e'' g; Assumption.

Inversion_clear H.
Apply H4 with g0 S1 S2 C1 C2 E1 E2.
Elim (dec_group g0 g); Elim (STAR_GROUP_TYPE_DEC (gr_star S1 C1 E1 t1) s); Intros.
Rewrite H; Rewrite H5; Apply group_in_env3.
Apply group_in_env2.
Right; Unfold not; Intros; Absurd (gr_star S1 C1 E1 t1)=s; Assumption.
Assumption.
Apply group_in_env2.
Left; Unfold not; Intros; Absurd g0=g; Assumption.
Assumption.
Apply group_in_env2.
Left; Unfold not; Intros; Absurd g0=g; Assumption.
Assumption.
Apply REMOVE_G with e'' g; Assumption.

Qed.

Axiom dec_name: (n,m:name)n=m \/ ~n=m.

Lemma UNIFY_LESS2: (e,e':env)(n:name)(W:msgType)
                   (unify_env (consEname n W e) e') ->
                   (unify_env e e').

Proof.

Unfold unify_env; Intros; Split; Intros.

Inversion_clear H.
Apply H2 with n0; Auto.
Elim (dec_name n n0); Elim (MSG_TYPE_DEC W W1); Intros.
Rewrite H; Rewrite H4; Apply name_in_env3.
Apply name_in_env2.
Right; Auto.
Assumption.
Apply name_in_env2.
Left; Auto.
Assumption.
Apply name_in_env2.
Left; Auto.
Assumption.

Inversion_clear H.
Apply H3 with g S1 S2 C1 C2 E1 E2; Auto.
Apply group_in_env1; Assumption.

Qed.

Lemma UNION_IN: (e1,e2,e:env)(g:group)(S:starGlist)(C,E:Glist)(t:comType)
                (unify_env e1 e2) -> (union_env e1 e2 e) ->
                (group_in_env g (gr_star S C E t) e2) ->
                (Ex [S':starGlist](Ex [C':Glist](Ex [E':Glist](group_in_env g (gr_star S' C' E' t) e)))).

Proof.

Induction e1; Intros.

Inversion H0; Exists S; Exists C; Exists E; Rewrite <-H4; Assumption.

Inversion H1.
Elim (dec_group g g0); Intros.
Exists S'; Exists C'; Exists E'.
Rewrite <-H13; Rewrite <-H13 in H2; Unfold unify_env in H0; Inversion_clear H0.
Cut t=t0; [Intro | Idtac].
Rewrite H0; Apply group_in_env3.
Cut t0=t; [Intro; Auto | Idtac].
Apply H15 with g S0 S C0 C E0 E; Auto.
Rewrite <-H4; Apply group_in_env3.
Cut (EX S':starGlist | (EX C':Glist | (EX E':Glist | (group_in_env g0 (gr_star S' C' E' t) e'')))); [Intro | Apply H with e''' S C E].
Inversion_clear H14.
Inversion_clear H15.
Inversion_clear H14.
Exists x; Exists x0; Exists x1; Apply group_in_env2.
Left; Auto.
Assumption.
Apply UNIFY_LESS with g s e2; Auto.
Assumption.
Apply REMOVE_G2 with e2 g; Auto.

Inversion H1.
Cut (EX S':starGlist | (EX C':Glist | (EX E':Glist | (group_in_env g (gr_star S' C' E' t) e'')))); [Intro | Apply H with e2 S C E].
Inversion_clear H9.
Inversion_clear H10.
Inversion_clear H9.
Exists x; Exists x0; Exists x1; Apply group_in_env1.
Assumption.
Apply UNIFY_LESS2 with n m; Assumption.
Assumption.
Assumption.

Qed.

Axiom CLOSURE_EX: (S:starGlist)(g:group)(C,E:Glist)(t:comType)(e:env)(group_in_env g (gr_star S C E t) e) -> (Ex [S':Glist](closure S S' e)).

Axiom GROUP_IN_UNION: (e1,e2,e3:env)(union_env e1 e2 e3) ->
                      (g,g':group)(S,S':starGlist)(C,C',E,E':Glist)(t:comType)
                      (group_in_env g (gr_star S C E t) e2) ->
                      (starGlist_isin (simple g') S) ->
                      (group_in_env g (gr_star S' C' E' t) e3) ->
                      (starGlist_isin (simple g') S').

Lemma GLIST_ISIN: (l:starGlist)(g:group)(starGlist_isin (simple g) l) ->
                  (Glist_isin g (star_clear l)).

Proof.

Induction l; Intros.

Inversion_clear H.

Inversion H0.
Simpl.
Apply Glist_isin_group.
Inversion_clear H2.
Rewrite <-H4; Simpl.
Apply Glist_isin_consG.
Left; Trivial.
Case s; Intro.
Simpl; Apply Glist_isin_consG.
Right; Apply H; Assumption.
Simpl; Apply Glist_isin_consG.
Right; Apply H; Assumption.

Qed.

Lemma STARGLIST_ISIN_APPEND: (l,l':starGlist)(s:star_group)
                             (starGlist_isin s l) ->
                             (starGlist_isin s (append_starGlist l l')).

Proof.

Induction l; Intros.

Inversion_clear H.

Simpl.
Inversion H0.
Apply starGlist_isin_consG; Left; Trivial.
Inversion_clear H2.
Rewrite H4; Apply starGlist_isin_consG; Left; Trivial.
Apply starGlist_isin_consG; Right; Apply H; Assumption.

Qed.

Lemma GROUP_IN_CLOSURE: (S:starGlist)(S':Glist)(e:env)(g:group)(closure S S' e) -> (starGlist_isin (simple g) S) -> (Glist_isin g S').

Proof.

Induction 1; Intros.

Apply GLIST_ISIN; Assumption.

Apply H4.
Apply STARGLIST_ISIN_APPEND; Assumption.

Qed.

Lemma PROC_INF_SOUND: (R:raw_proc)(P:proc)(g:group)(e:env)(proc_inf R P g e) -> (good_proc P g).

Proof.

Induction R; Intros.

Inversion_clear H; Apply good_proc_nil.

Inversion H0.
Apply good_proc_prefix with g1.
Rewrite H5 in H3; Apply MSG_INF_SOUND with e1; Assumption.
Apply H with e2; Assumption.

Inversion H0.
Elim (UNION_IN e1 (consEgroup g (gr_star starEmptyG emptyG emptyG (msg W)) e2) e g starEmptyG emptyG emptyG (msg W)); Intros.
Inversion_clear H10; Inversion_clear H11.
Elim (CLOSURE_EX x g x0 x1 (msg W) e H10); Intros.
Apply good_proc_output with W x2 x0 x1.
Apply H with e1; Assumption.
Apply MSG_INF_SOUND with e2; Assumption.
Apply TYPE_GROUP with x e; Assumption.
Assumption.
Assumption.
Apply group_in_env3.

Inversion H0.
Elim (CLOSURE_EX S g C E t e H2); Intros.
Apply good_proc_input with x C E.
Intros; Apply H with x0 (consEname x0 (amb_type g) e); Auto.
Rewrite H3 in H2; Apply TYPE_GROUP with S e; Assumption.

Inversion_clear H1.
Rewrite H4 in H2; Apply good_proc_par; [Apply H with e1 | Apply H0 with e2]; Assumption.

Inversion H0.
Elim (UNION_IN e0 (consEname x W (consEgroup g0 (gr_star (starConsG (simple g) starEmptyG) emptyG emptyG t) emptyE)) e g0 (starConsG (simple g) starEmptyG) emptyG emptyG t); Intros.
Inversion_clear H11; Inversion_clear H12.
Elim (CLOSURE_EX x0 g0 x1 x2 t e H11); Intros.
Apply good_proc_amb with x3 x1 x2 g0 t.
Apply H with e0; Assumption.
Rewrite H5 in H3; Apply MSG_INF_SOUND with (consEname x (amb_type g0) emptyE); Assumption.
Apply TYPE_GROUP with x0 e; Assumption.
Apply GROUP_IN_CLOSURE with x0 e.
Assumption.
Apply GROUP_IN_UNION with e0 (consEname x W (consEgroup g0 (gr_star (starConsG
(simple g) starEmptyG) emptyG emptyG t) emptyE)) e g0 (starConsG (simple g)
starEmptyG) emptyG x1 emptyG x2 t; Auto.
Apply group_in_env1; Apply group_in_env3.
Apply starGlist_isin_consG; Left; Trivial.
Assumption.
Assumption.
Apply group_in_env1; Apply group_in_env3.

Inversion H0.
Apply good_proc_repl; Apply H with e; Assumption.

Inversion H0.
Apply good_proc_res; Intros.
Apply H with m (consEname m (amb_type g') e); Auto.

Qed.