Load Sec1_SyntaxDefs.

Inductive b2p : bool -> Prop :=
  | b2pt : True -> b2p true.

Definition beq_string (s1:string) (s2:string) : bool :=
           if (string_dec s1 s2) then true else false.

Lemma beq_string_EQ : forall s1 s2, beq_string s1 s2 = true -> s1 = s2.

Fixpoint beq_A_list (A:Type) (beq_A: A->A->bool) (s1:list A) (s2:list A) : bool :=
  match s1,s2 with
   | [],[] => true
   | h1::ts1, h2::ts2 => andb (beq_A h1 h2) (beq_A_list beq_A ts1 ts2)
   | _, _ => false
  end.

Fixpoint eq_A_list (A:Type) (eq_A: A->A->Prop) (s1:list A) (s2:list A) : Prop :=
  match s1,s2 with
   | [],[] => True
   | h1::ts1, h2::ts2 => (eq_A h1 h2) /\ (eq_A_list eq_A ts1 ts2)
   | _, _ => False
  end.

Definition beq_string_list : (list string) -> (list string) -> bool := beq_A_list beq_string.

Definition eq_string (s1:string) (s2:string) : Prop := b2p (beq_string s1 s2).

Definition eq_string_list (s1: list string) (s2:list string) : Prop := b2p (beq_string_list s1 s2).

Fixpoint beq_name (n1:name) (n2:name) : bool :=
  match n1,n2 with
    | Fresh_P s1 , Fresh_P s2 => beq_string s1 s2
    | Fresh_S s1 , Fresh_S s2 => beq_string s1 s2
    | Pub s1, Pub s2 => beq_string s1 s2
    | _, _ => false
   end.

Definition eq_name (n1:name) (n2:name) : Prop := b2p (beq_name n1 n2).

Definition beq_names : (list name) -> (list name) -> bool := beq_A_list beq_name.

Lemma beq_name_EQ : forall n1 n2, beq_name n1 n2 = true -> n1 = n2.

Definition name_dec : forall b1 b2 : name, {b1 = b2} + {b1 <> b2}.
Defined.

Fixpoint beq_baseTerm (t1:baseTerm) (t2:baseTerm) : bool :=
  match t1,t2 with
    | Var x,Var y => beq_string x y
    | Name n1, Name n2 => beq_name n1 n2
    | _, _ => false
   end.

Fixpoint eq_baseTerm (t1:baseTerm) (t2:baseTerm) : Prop :=
  match t1,t2 with
    | Var x,Var y => eq_string x y
    | Name n1, Name n2 => eq_name n1 n2
    | _, _ => False
   end.

Definition baseTerm_dec : forall b1 b2 : baseTerm, {b1 = b2} + {b1 <> b2}.
Defined.

Definition beq_baseTerms : (list baseTerm) -> (list baseTerm) -> bool := beq_A_list beq_baseTerm.

Definition eq_baseTerms : (list baseTerm) -> (list baseTerm) -> Prop := eq_A_list eq_baseTerm.

Definition baseTerms_dec : forall bl1 bl2 : (list baseTerm), {bl1 = bl2} + {bl1 <> bl2}.
Defined.

Definition beq_term (t1:term) (t2:term) : bool :=
  match t1,t2 with
    | (Bterm b1), (Bterm b2) => beq_baseTerm b1 b2
    | (Func f1 l1), (Func f2 l2) => andb (beq_string f1 f2) (beq_baseTerms l1 l2)
    | _, _ => false
   end.

Definition beq_terms : (list term) -> (list term) -> bool := beq_A_list beq_term.

Definition eq_term (t1:term) (t2:term) : Prop :=
  match t1,t2 with
    | (Bterm b1), (Bterm b2) => eq_baseTerm b1 b2
    | (Func f1 l1), (Func f2 l2) => (eq_string f1 f2) /\ (eq_baseTerms l1 l2)
    | _, _ => False
   end.

Definition eq_termFuncName (t1:term) (t2:term) : Prop :=
  match t1,t2 with
    | (Func f1 l1), (Func f2 l2) => (eq_string f1 f2)
    | _, _ => False
   end.

Definition eq_terms : (list term) -> (list term) -> Prop := eq_A_list eq_term.

Definition term_dec : forall t1 t2 : term, {t1 = t2} + {t1 <> t2}.
Defined.

Definition terms_dec : forall ts1 ts2 : terms, {ts1 = ts2} + {ts1 <> ts2}.
Defined.

Fixpoint beq_fact (f1:fact) (f2:fact) : bool :=
  match f1,f2 with
   | IN ts1, IN ts2 => beq_terms ts1 ts2
   | OUT ts1, OUT ts2 => beq_terms ts1 ts2
   | K ts1, K ts2 => beq_terms ts1 ts2
   | STATE n1 ts1, STATE n2 ts2 => andb (beq_name n1 n2) (beq_terms ts1 ts2)
   | FR_P bt1, FR_P bt2 => beq_baseTerm bt1 bt2
   | _, _ => false
  end.

Fixpoint eq_fact (f1:fact) (f2:fact) : Prop :=
  match f1,f2 with
   | IN ts1, IN ts2 => eq_terms ts1 ts2
   | OUT ts1, OUT ts2 => eq_terms ts1 ts2
   | K ts1, K ts2 => eq_terms ts1 ts2
   | STATE n1 ts1, STATE n2 ts2 => eq_name n1 n2 /\ eq_terms ts1 ts2
   | FR_P bt1, FR_P bt2 => eq_baseTerm bt1 bt2
   | _, _ => False
  end.

Definition eq_facts : (list fact) -> (list fact) -> Prop := eq_A_list eq_fact.

Definition beq_facts : (list fact) -> (list fact) -> bool := beq_A_list beq_fact.

Definition fact_dec : forall f1 f2 : fact, {f1 = f2} + {f1 <> f2}.
Defined.

Definition facts_dec : forall fs1 fs2 : facts, {fs1 = fs2} + {fs1 <> fs2}.
Defined.

Definition tpair_dec : forall tp1 tp2 : tpair, {tp1 = tp2} + {tp1 <> tp2}.
Defined.

Definition tpairs_dec : forall ts1 ts2 : tpairs, {ts1 = ts2} + {ts1 <> ts2}.
Defined.

Definition beq_var (v1:variable) (v2:variable) : bool := beq_string v1 v2.
Definition beq_vars_list : (list variable) -> (list variable) -> bool := beq_A_list beq_var.

Definition beq_actionLabel (a1:actionLabel) (a2:actionLabel) : bool :=
  match a1, a2 with
   | ActLabel n1 ts1, ActLabel n2 ts2 => andb (beq_name n1 n2) (beq_terms ts1 ts2)
   end.

Definition beq_actionLabels : (list actionLabel) -> (list actionLabel) -> bool := beq_A_list beq_actionLabel.

Definition actionLabel_dec : forall t1 t2 : actionLabel, {t1 = t2} + {t1 <> t2}.
Defined.

Definition actionLabels_dec : forall t1 t2 : list actionLabel, {t1 = t2} + {t1 <> t2}.
Defined.

Definition eq_actionLabel (a1:actionLabel) (a2:actionLabel) : Prop := b2p (beq_actionLabel a1 a2).

Definition eq_actionLabels (al1:list actionLabel) (al2:list actionLabel) : Prop := b2p (beq_actionLabels al1 al2).

Definition label_dec : forall l1 l2 : label, {l1 = l2} + {l1 <> l2}.
Defined.

Definition beq_label (l1:label) (l2:label) : bool :=
  match l1, l2 with
   | BasicLabel ll1 , BasicLabel ll2 => beq_actionLabels ll1 ll2
   | LoggedLabel al1 ll1 , LoggedLabel al2 ll2 => andb (beq_actionLabel al1 al2) (beq_actionLabels ll1 ll2)
   | _, _ => false
  end.

Definition eq_label (l1:label) (l2:label) : Prop :=
  match l1, l2 with
   | BasicLabel ll1 , BasicLabel ll2 => eq_A_list eq_actionLabel ll1 ll2
   | LoggedLabel lg1 ll1 , LoggedLabel lg2 ll2 => eq_A_list eq_actionLabel ll1 ll2
                                                    /\ eq_actionLabel lg1 lg2
   | _, _ => False
  end.

Definition beq_trace : trace -> trace -> bool := beq_A_list beq_label.

Definition eq_trace : trace -> trace -> Prop := eq_A_list eq_label.

Definition rule_dec : forall r1 r2 : rule, {r1 = r2} + {r1 <> r2}.
Defined.

Definition rules_dec : forall r1 r2 : ruleList, {r1 = r2} + {r1 <> r2}.
Defined.

Fixpoint member {A:Type} (r:A) (rl:list A) : Prop :=
  match rl with
   | [] => False
   | r1::rs => r=r1 \/ (member r rs)
  end.

Fixpoint memberWith {A:Type} (x : A) (l : list A) (beq_test : A->A->bool) : bool :=
    match l with
      | [] => false
      | h :: ts => orb (beq_test x h) (memberWith x ts beq_test)
    end.

Fixpoint memberOnce {A:Type} (a : A) (ls : list A) : Prop :=
  match ls with
    | [] => False
    | h::ts => a = h /\ NotIn a ts
  end.

Definition removeFact : fact -> facts -> facts := removeElement fact_dec.

Fixpoint removeFacts (facts1:facts) (facts2:facts) : facts :=
  match facts1 with
    | [] => facts2
    | h::ts => removeFact h (removeFacts ts facts2)
  end.


Fixpoint subList (l1:list fact) (l2:list fact) : Prop :=
  match l1,l2 with
    | [],_ => True
    | _,[] => False
    | h1::t,l2 => (In h1 l2) /\ (subList t (removeFact h1 l2))
  end.

Definition b_inLabel (al:actionLabel) (lb:label) : bool :=
 match lb with
   | BasicLabel ll1 => memberWith al ll1 beq_actionLabel
   | LoggedLabel lg1 ll1 => orb (beq_actionLabel al lg1) (memberWith al ll1 beq_actionLabel)
   | LoggedSIDLabel t lg1 ll1 => orb (beq_actionLabel al lg1) (memberWith al ll1 beq_actionLabel)
  end.

Fixpoint inLabel (al:actionLabel) (lb:label) : Prop :=
    match lb with
      | BasicLabel ll => member al ll
      | LoggedLabel lg ll => ( eq_actionLabel lg al) \/ member al ll
      | LoggedSIDLabel t lg ll => ( eq_actionLabel lg al) \/ member al ll
    end.

Fixpoint inLoggedSIDLabel (al:actionLabel) (lb:label) : Prop :=
    match lb with
      | BasicLabel ll => False
      | LoggedLabel lg ll => False
      | LoggedSIDLabel t lg ll => ( eq_actionLabel lg al)
    end.

Fixpoint al_in_Trace (al:actionLabel) (tr:trace) : Prop :=
    match tr with
      | [] => False
      | lbl1 :: lbs => inLabel al lbl1 \/ (al_in_Trace al lbs)
    end.

Fixpoint LoggedAL_in_Trace (al:actionLabel) (tr:trace) : Prop :=
    match tr with
      | [] => False
      | lbl1 :: lbs => inLoggedSIDLabel al lbl1 \/ (LoggedAL_in_Trace al lbs)
    end.

Fixpoint LoggedLbl_in_Trace (lbl:label) (tr:trace) : Prop :=
    match tr with
      | [] => False
      | lbl1 :: lbs => (eq_label lbl lbl1) \/ (LoggedLbl_in_Trace lbl lbs)
    end.

Definition b_label_in_Trace (lb:label) (tr:trace) : bool := memberWith lb tr beq_label.

Definition b_labelS_in_Trace (lb:label) (tr:trace) : bool := memberWith lb tr beq_label.

Definition beq_trace_in_Traces (tr:trace) (trlist:list trace) : bool := memberWith tr trlist beq_trace.

Definition beq_actionLabelName (a1:actionLabel) (a2:actionLabel) : bool :=
  match a1, a2 with
   | ActLabel n1 ts1, ActLabel n2 ts2 => (beq_name n1 n2)
   end.

Definition eq_actionLabelName (a1:actionLabel) (a2:actionLabel) : Prop := b2p (beq_actionLabelName a1 a2).

Definition b_inLabelwithName (al:actionLabel) (lb:label) : bool :=
 match lb with
   | BasicLabel ll1 => memberWith al ll1 beq_actionLabelName
   | LoggedLabel lg1 ll1 => orb (beq_actionLabelName al lg1) (memberWith al ll1 beq_actionLabelName)
   | LoggedSIDLabel t lg1 ll1 => orb (beq_actionLabelName al lg1) (memberWith al ll1 beq_actionLabelName)
  end.

Fixpoint memberName (al:actionLabel) (lb:list actionLabel) : Prop :=
  match lb with
   | [] => False
   | l1::ls => (eq_actionLabelName al l1) \/ (memberName al ls)
  end.

Fixpoint inLabelwithName (al:actionLabel) (lb:label) : Prop :=
    match lb with
      | BasicLabel ll => memberName al ll
      | LoggedLabel lg ll => ( eq_actionLabelName lg al) \/ memberName al ll
      | LoggedSIDLabel t lg ll => ( eq_actionLabelName lg al) \/ memberName al ll
    end.

Fixpoint b_ALinTemplatewithName (al:actionLabel) (tm:trace) : bool :=
  match tm with
  | [] => false
  | tm1::tms => orb (b_inLabelwithName al tm1) (b_ALinTemplatewithName al tms)
  end.

Fixpoint b_ALinStdTemplateswithName (al:actionLabel) (StdTemps:list trace) : bool :=
  match StdTemps with
  | [] => false
  | tm1::tms => orb (b_ALinTemplatewithName al tm1) (b_ALinStdTemplateswithName al tms)
  end.

Definition ALinTemplatewithName (al:actionLabel) (tm:trace) : Prop := b2p (b_ALinTemplatewithName al tm).

Definition ALinStdTemplateswithName (al:actionLabel) (tms:list trace) : Prop := b2p (b_ALinStdTemplateswithName al tms).

Fixpoint InList (tm : term) (tmlist : terms) : bool :=
  match tmlist with
  | [] => false
  | ml1::mls => orb (beq_term tm ml1) (InList tm mls)
  end.

Fixpoint commonTerms (v1:terms) (v2:terms): terms :=
 match v1 with
  | [] => []
  | v11 :: v1s => if InList v11 v2 then (v11::(commonTerms v1s v2)) else commonTerms v1s v2
end.

Fixpoint InFreshList (tm : freshNameProto) (tmlist : list freshNameProto) : bool :=
  match tmlist with
  | [] => false
  | ml1::mls => orb (beq_term (Bterm (Name (Fresh_P tm))) (Bterm (Name (Fresh_P ml1)))) (InFreshList tm mls)
  end.

Fixpoint commonTermsAL (alp1:actionLabel) (alp2:actionLabel): terms :=
  match alp1, alp2 with
  | ActLabel nm1 vars1, ActLabel nm2 vars2 => commonTerms vars1 vars2
  end.


Fixpoint hasFunction (tm:terms) : Prop :=
match tm with
  | tm1::tms => match tm1 with
                          | Func _ _ => True
                          | _ => hasFunction tms
                 end
  | [] => False
end.

Fixpoint hasPubNameInBaseTerms (btm:baseTerms) : Prop :=
match btm with
    | btm1::btms => match btm1 with
                       | (Var _) => hasPubNameInBaseTerms btms
                       | (Name nm) => match nm with
                                          | Pub _ => True
                                          | _ => hasPubNameInBaseTerms btms
                                         end
                      end
  | [] => False
end.

Fixpoint b_hasPubNameInBaseTerms (btm:baseTerms) : bool :=
match btm with
    | btm1::btms => match btm1 with
                       | (Var _) => b_hasPubNameInBaseTerms btms
                       | (Name nm) => match nm with
                                          | Pub _ => true
                                          | _ => b_hasPubNameInBaseTerms btms
                                         end
                      end
  | [] => false
end.

Fixpoint hasPubName (tm:terms) : Prop :=
match tm with
  | tm1::tms => match tm1 with
                    | Func f bts => hasPubNameInBaseTerms bts
                    | Bterm bt => match bt with
                       | (Var _) => hasPubName tms
                       | (Name nm) => match nm with
                                          | Pub _ => True
                                          | _ => hasPubName tms
                                         end
                      end

                 end
  | [] => False
end.

Fixpoint getPubNameInBaseTerms (t:term) (btm:baseTerms) : term :=
match btm with
    | btm1::btms => match btm1 with
                       | (Var _) => getPubNameInBaseTerms t btms
                       | (Name nm) => match nm with
                                          | Pub pn => Bterm (Name (Pub pn))
                                          | _ => getPubNameInBaseTerms t btms
                                         end
                      end
  | [] => t
end.

Fixpoint getPubName (t:term) (tm:terms) : term :=
match tm with
  | tm1::tms => match tm1 with
                    | Func f bts => getPubNameInBaseTerms t bts
                    | Bterm bt => match bt with
                       | (Var _) => getPubName t tms
                       | (Name nm) => match nm with
                                          | Pub pn => Bterm (Name (Pub pn))
                                          | _ => getPubName t tms
                                         end
                      end

                 end
  | [] => t
end.

Fixpoint b_hasPubName (tm:terms) : bool :=
match tm with
  | tm1::tms => match tm1 with
                    | Func f bts => b_hasPubNameInBaseTerms bts
                    | Bterm bt => match bt with
                       | (Var _) => b_hasPubName tms
                       | (Name nm) => match nm with
                                          | Pub _ => true
                                          | _ => b_hasPubName tms
                                         end
                      end

                 end
  | [] => false
end.

Fixpoint b_hasFunction (tm:terms) : bool :=
match tm with
  | tm1::tms => match tm1 with
                          | Func _ _ => true
                          | _ => b_hasFunction tms
                 end
  | [] => false
end.

Fixpoint selectFunctions (tm: terms) : terms :=
match tm with
  | Func f bt1::tms => (Func f bt1)::(selectFunctions tms)
  | _ ::tms => (selectFunctions tms)
  | [] => []
end.

Fixpoint premiseFacts (r:rule) : facts :=
  match r with
    | RuleSetup f1 l f2 => f1
    | RuleProto f1 l f2 => f1
  end.

Fixpoint conclFacts (r:rule) : facts :=
  match r with
    | RuleSetup f1 l f2 => f2
    | RuleProto f1 l f2 => f2
  end.

Fixpoint allPremiseFacts (rs:(list rule)) : facts :=
  match rs with
    | [] => []
    | r::rst => appendAny (premiseFacts r) (allPremiseFacts rst)
   end.

Fixpoint allConclFacts (rs:(list rule)) : facts :=
  match rs with
    | [] => []
    | r::rst => appendAny (conclFacts r) (allConclFacts rst)
  end.

Fixpoint allFactsRL (rs:(list rule)) : facts :=
  appendAny (allPremiseFacts rs) (allConclFacts rs).

Fixpoint labelR (r:rule) : label :=
  match r with
    | RuleSetup f1 l f2 => l
    | RuleProto f1 l f2 => l
  end.

Fixpoint getInFactPremise (fp:facts) : facts :=
match fp with
       | f1::fs => match f1 with
                         | IN _ => appendAny [f1](getInFactPremise fs)
                         | OUT _ => (getInFactPremise fs)
                         | K _ => (getInFactPremise fs)
                         | STATE _ _ => (getInFactPremise fs)
                         | FR_P _ => (getInFactPremise fs)
                   end
      | [] => []
end.

Fixpoint getFrFactPremise (fp:facts) : facts :=
match fp with
       | f1::fs => match f1 with
                         | IN _ => (getFrFactPremise fs)
                         | OUT _ => (getFrFactPremise fs)
                         | K _ => (getFrFactPremise fs)
                         | STATE _ _ => (getFrFactPremise fs)
                         | FR_P _ => appendAny [f1](getFrFactPremise fs)
                   end
      | [] => []
end.

Fixpoint getOutFactConclusion (fp:facts) : facts :=
match fp with
       | f1::fs => match f1 with
                         | IN _ => (getOutFactConclusion fs)
                         | OUT _ => appendAny [f1] (getOutFactConclusion fs)
                         | K _ => (getOutFactConclusion fs)
                         | STATE _ _ => (getOutFactConclusion fs)
                         | FR_P _ => (getOutFactConclusion fs)
                   end
      | [] => []
end.

Fixpoint getOutFactProtoRule (rl:rule) : facts :=
  match rl with
  | (RuleProto fp1 lp fp2) => getOutFactConclusion fp2
  | (RuleSetup fp1 lp fp2) => []
  end.

Fixpoint getInFactProtoRule (rl:rule) : facts :=
  match rl with
  | (RuleProto fp1 lp fp2) => getInFactPremise fp1
  | (RuleSetup fp1 lp fp2) => []
  end.

Fixpoint getFrFactProtoRule (rl:rule) : facts :=
  match rl with
  | (RuleProto fp1 lp fp2) => getFrFactPremise fp1
  | (RuleSetup fp1 lp fp2) => []
  end.

Fixpoint getFrFactSetupRule (rl:rule) : facts :=
  match rl with
  | (RuleProto fp1 lp fp2) => []
  | (RuleSetup fp1 lp fp2) => getFrFactPremise fp1
  end.

Fixpoint removeOutInfromFactList (fs: facts) : facts :=
match fs with
  | [] => []
  | fs1::fss => match fs1 with
                         | IN _ => (removeOutInfromFactList fss)
                         | OUT _ => (removeOutInfromFactList fss)
                         | K _ => appendAny [fs1] (removeOutInfromFactList fss)
                         | STATE _ _ => appendAny [fs1] (removeOutInfromFactList fss)
                         | FR_P _ => appendAny [fs1] (removeOutInfromFactList fss)
                   end
end.


Fixpoint getStateFacts (fp:facts) : facts :=
match fp with
       | f1::fs => match f1 with
                         | IN _ => (getStateFacts fs)
                         | OUT _ => (getStateFacts fs)
                         | K _ => (getStateFacts fs)
                         | STATE _ _ => appendAny [f1](getStateFacts fs)
                         | FR_P _ => (getStateFacts fs)
                   end
      | [] => []
end.

Fixpoint getLogRL (rl: ruleList) : trace :=
  match rl with
    | [] => []
    | rl1::rls => match labelR rl1 with
                    | LoggedLabel lg lb1 => (LoggedLabel lg [])::(getLogRL rls)
                    | _ => getLogRL rls
                   end
  end.

Fixpoint onlyBasicLogsInRL (rl: ruleList) : Prop :=
  match rl with
    | [] => True
    | rl1::rls => match labelR rl1 with
                    | BasicLabel lb1 => True /\ (onlyBasicLogsInRL rls)
                    | _ => False
                   end
  end.

Fixpoint getTermsAL (al:actionLabel) : terms :=
match al with
   | ActLabel NM TRMS => TRMS
end.

Fixpoint getTermsLoggedLabel (l1:label) : terms :=
  match l1 with
    | (LoggedSIDLabel t al lb) => (Bterm t):: (getTermsAL al)
    | (LoggedLabel al lb) => []
    | (BasicLabel als) => []
  end.


Fixpoint getFreshProtoNamesinAL (al: list actionLabel) : list freshNameProto :=
 match al with
  | al1::als => match al1 with
                  | ActLabel (Fresh_P fp) t => fp ::(getFreshProtoNamesinAL als)
                  | _ => getFreshProtoNamesinAL als
                 end
  | [] => []
 
 end.

Fixpoint getFreshProtoNamesinLabel (lb: label) : list freshNameProto :=
  match lb with
    | LoggedSIDLabel t al als => match al with
                                  | ActLabel (Fresh_P fp) t => fp :: (getFreshProtoNamesinAL als)
                                  | _ => getFreshProtoNamesinAL als
                                 end
    | BasicLabel al => []
    | LoggedLabel al als => []
   end.


Inductive getSID : label -> baseTerm -> Prop :=
       | validSID : forall t al als, getSID (LoggedSIDLabel t al als) t.

Inductive getParsFromLog : label -> terms -> Prop :=
       | validTerms : forall t alname alterms als, getParsFromLog (LoggedSIDLabel t (alname alterms) als) alterms.

Fixpoint getLogTrace (t:trace) : trace :=
  match t with
    | [] => []
    | h::ts => match h with
                 | LoggedLabel lg lb1 => (LoggedLabel lg [])::(getLogTrace ts)
                 | _ => getLogTrace ts
                end
  end.


Definition constantsInBaseTerm (bt:baseTerm) : variables :=
  match bt with
    | Name (Pub v) => [v]
    | _ => []
  end.

Definition constantsInBaseTerms : (list baseTerm) -> variables := mapListFunction constantsInBaseTerm.

Definition constantsInTerm (t:term) : variables :=
  match t with
    | Func fn bts => constantsInBaseTerms bts
    | Bterm bt => constantsInBaseTerm bt
  end.
Definition constantsInTerms : (list term) -> variables := mapListFunction constantsInTerm.

Definition variablesInBaseTerm (bt:baseTerm) : variables :=
  match bt with
    | Var v => [v]
    | _ => []
  end.

Definition variablesInBaseTerms : (list baseTerm) -> variables := mapListFunction variablesInBaseTerm.

Definition variablesInTerm (t:term) : variables :=
  match t with
    | Func fn bts => variablesInBaseTerms bts
    | Bterm bt => variablesInBaseTerm bt
  end.

Definition variablesInTerms : (list term) -> variables := mapListFunction variablesInTerm.

Definition variablesInFact (f:fact) : variables :=
  match f with
  | IN ts => variablesInTerms ts
  | OUT ts => variablesInTerms ts
  | K ts => variablesInTerms ts
  | STATE n ts => variablesInTerms ts
  | FR_P bt => variablesInBaseTerm bt
  end.

Definition variablesInRule (r:rule) : variables :=
  match r with
    | RuleSetup f1 l f2 => mapListFunction variablesInFact f1
    | RuleProto f1 l f2 => mapListFunction variablesInFact f1
  end.

Definition freshNameInBaseTerm (bt:baseTerm) : list freshNameProto :=
  match bt with
    | Name nm => match nm with
                      | Fresh_P fp => [fp]
                      | _ => []
                 end
    | _ => []
  end.

Definition freshNamesInBaseTerms : (list baseTerm) -> list freshNameProto := mapListFunction freshNameInBaseTerm.

Definition freshNamesInTerm (t:term) : list freshNameProto :=
  match t with
    | Func fn bts => freshNamesInBaseTerms bts
    | Bterm bt => freshNameInBaseTerm bt
  end.

Definition freshNamesInTerms : (list term) -> list freshNameProto := mapListFunction freshNamesInTerm.

Fixpoint getFreshProtoNamesinLoggedSIDTrace (tr: trace) : list freshNameProto :=
  match tr with
    | [] => []
    | h::ts => match h with
                 | LoggedSIDLabel t al als => match al with
                                                   | ActLabel nm t => appendAny (freshNamesInTerms t) (getFreshProtoNamesinLoggedSIDTrace ts)
                                                  end
                 | BasicLabel al => (getFreshProtoNamesinLoggedSIDTrace ts)
                 | LoggedLabel al lb => (getFreshProtoNamesinLoggedSIDTrace ts)
                end
   end.

Fixpoint getFreshProtoNamesinTrace (tr: trace) : list freshNameProto :=
  match tr with
    | [] => []
    | h::ts => match h with
                 | LoggedLabel al als => match al with
                                                   | ActLabel nm t => appendAny (freshNamesInTerms t) (getFreshProtoNamesinTrace ts)
                                                 end
                 | BasicLabel al => (getFreshProtoNamesinTrace ts)
                 | LoggedSIDLabel t al lb => (getFreshProtoNamesinTrace ts)
                end
   end.

Definition getFreshProtoNamesList : (list trace) -> list freshNameProto := mapListFunction getFreshProtoNamesinTrace.

Fixpoint getFrNamesPremiseProto (fp:facts) : list freshNameProto :=
match fp with
       | f1::fs => match f1 with
                         | IN _ => (getFrNamesPremiseProto fs)
                         | OUT _ => (getFrNamesPremiseProto fs)
                         | K _ => (getFrNamesPremiseProto fs)
                         | STATE _ _ => (getFrNamesPremiseProto fs)
                         | FR_P fp1 =>
                                    match fp1 with
                                      | (Var _) => getFrNamesPremiseProto fs
                                      | (Name nm) => match nm with
                                                        | Fresh_S _ => (getFrNamesPremiseProto fs)
                                                        | Fresh_P fn => fn::(getFrNamesPremiseProto fs)
                                                        | Pub _ => (getFrNamesPremiseProto fs)
                                                        end
                                     end
                   end
      | [] => []
end.

Fixpoint getFrNamesPremiseSetup (fp:facts) : list freshNameSetup :=
match fp with
       | f1::fs => match f1 with
                         | IN _ => (getFrNamesPremiseSetup fs)
                         | OUT _ => (getFrNamesPremiseSetup fs)
                         | K _ => (getFrNamesPremiseSetup fs)
                         | STATE _ _ => (getFrNamesPremiseSetup fs)
                         | FR_P fp1 =>
                                    match fp1 with
                                      | (Var _) => getFrNamesPremiseSetup fs
                                      | (Name nm) => match nm with
                                                        | Fresh_S fss => (fss::getFrNamesPremiseSetup fs)
                                                        | Fresh_P _ => (getFrNamesPremiseSetup fs)
                                                        | Pub _ => (getFrNamesPremiseSetup fs)
                                                        end
                                     end
                   end
      | [] => []
end.

Fixpoint InFresh (fr : freshNameProto) (frlist : list freshNameProto) : bool :=
  match (member fr frlist) with
  | True => true
  end.

Fixpoint commonFreshNames (f1:list freshNameProto) (f2:list freshNameProto): list freshNameProto :=
 match f1 with
  | [] => []
  | f11 :: f1s => if InFreshList f11 f2 then (f11::(commonFreshNames f1s f2)) else commonFreshNames f1s f2
end.

Fixpoint getVarsInTemplate (tr:trace) : list variable :=
  match tr with
    | [] => []
    | h::ts => match h with
                 | LoggedSIDLabel t al als => match al with
                                                  | ActLabel nm t => appendAny (variablesInTerms t) (getVarsInTemplate ts)
                                                end
                 | BasicLabel al => (getVarsInTemplate ts)
                 | LoggedLabel al lb => (getVarsInTemplate ts)
                end
   end.