Require Import Coq.Bool.Bool.
Require Import Coq.Arith.Arith.
Require Import Coq.Arith.EqNat.
Require Import Coq.omega.Omega.
Require Import Coq.Lists.List.
Require Import Coq.omega.Omega.
Require Import Coq.Sets.Multiset.
Require Import Coq.Lists.ListSet.
Require Import Coq.Strings.String.
Require Import Coq.Classes.RelationClasses.
Open Scope string_scope.

Import ListNotations.


Set Implicit Arguments.
Scheme Equality for list.

Fixpoint trueForAll {A:Type} (f:A->Prop) (l:list A) : Prop :=
  match l with
  | [] => True
  | h::ts => (f h) /\ (trueForAll f ts)
  end.

Fixpoint btrueForAll {A:Type} (f:A->bool) (l:list A) : bool :=
  match l with
  | [] => true
  | h::ts => andb (f h) (btrueForAll f ts)
  end.

Fixpoint trueForOne {A:Type} (f:A->Prop) (l:list A) : Prop :=
  match l with
  | [] => True
  | h::ts => (f h) \/ (trueForAll f ts)
  end.

Fixpoint appendAny {A:Type} l1 l2 : list A :=
  match l1 with
  | [] => l2
  | h :: t => h :: (appendAny t l2)
  end.

Fixpoint consEnd {A:Type} fs f : (list A) :=
  match fs with
  | [] => [f]
  | h :: t => h :: (consEnd t f)
  end.

Fixpoint lastElement {A:Type} (a:A) (als:list A) : A :=
  match als with
  | [] => a
  | h :: t => lastElement h t
  end.

Fixpoint secondLastElement {A:Type} (a:A) (als:list A) : A :=
  match als with
  | [] => a
  | h::[] => a
  | h1 :: h2 :: t => lastElement h1 (h2::t)
  end.

Fixpoint listWithoutLastElement {A:Type} (als:list A) : list A :=
  match als with
  | [] => []
  | h::[] => []
  | h :: t => h:: listWithoutLastElement t
  end.

Definition isLastElement {A:Type} (a:A) (als:list A) : Prop := (eq a (lastElement a als)).

Lemma listEq : forall {A:Type} (h1:A) h2 ts2 ts1, h1=h2 -> ts2=ts1 -> h1::ts2=h2::ts1.

Lemma listEqHead : forall {A:Type} (h:A) ts2 ts1, ts2=ts1 -> h::ts2=h::ts1.

Lemma listEqTail : forall {A:Type} (h1:A) h2 ts, h1=h2 -> h1::ts=h2::ts.

Fixpoint removeElement {A:Type} (eqA:forall a b : A, {a = b} + {a <> b}) (e:A) (l:list A) : list A :=
  match l with
    | [] => []
    | h::ts => if (eqA h e) then ts else (h::(removeElement eqA e ts))
  end.

Inductive prefixList {A:Type} : (list A) -> (list A) -> Prop :=
  | Empty_PreFix : forall l, prefixList [] l
  | Head_PreFix : forall l1 l2 a, prefixList l1 l2 -> prefixList (a::l1) (a::l2)
  | Next_PreFix : forall l1 l2 a, prefixList l1 l2 -> prefixList l1 (a::l2).

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

Fixpoint noCommonElements {A:Type} (f1:list A) (f2:list A): Prop :=
 match f1 with
  | [] => True
  | f11::f1s => NotIn f11 f2 /\ noCommonElements f1s f2
end.

Fixpoint termsDoNotAppear {A:Type} (f1: list A) (f2:list (list A)): Prop :=
 match f2 with
  | [] => True
  | f21::f2s => noCommonElements f1 f21 /\ termsDoNotAppear f1 f2s
end.

Fixpoint someCommonElements {A:Type} (f1:list A) (f2:list A): Prop :=
 match f1 with
  | [] => False
  | f11::f1s => In f11 f2 \/ someCommonElements f1s f2
end.

Fixpoint mapFunction {A:Type} {B:Type} (f:A -> B) (als:list A) : (list B) :=
  match als with
    | [] => []
    | h::ts => (f h)::(mapFunction f ts)
  end.

Fixpoint mapListFunction {A:Type} {B:Type} (f:A -> (list B)) (als:list A) : (list B) :=
  match als with
    | [] => []
    | h::ts => appendAny (f h) (mapListFunction f ts)
  end.



Inductive orderedSubList {A:Type} : (list A) -> (list A) -> Prop :=
 | Empty_O_SubList : forall l, orderedSubList [] l
 | Same_O_SubList : forall l1 l2 h1 h2, orderedSubList l1 l2 -> orderedSubList (h1::l1) (h2::l2)
 | Next_O_SubList : forall (l1:list A) l2 h, orderedSubList l1 l2 -> orderedSubList l1 (h::l2).

Lemma idIsOrderedSublist : forall {A:Type} (rl:list A), orderedSubList rl rl.

Definition freshNameSetup : Type := string. Definition freshNameProto : Type := string.
Definition sidTerm : Type := string.
Definition publicName : Type := string.
Inductive name : Type :=
  | Fresh_S : freshNameSetup -> name
  | Fresh_P : freshNameProto -> name
  | Pub : publicName -> name.

Definition n : string := "n".
Definition x : string := "x".

Definition names : Type := list name.

Definition variable : Type := string.
Definition variables : Type := list variable.

Inductive baseTerm : Type :=
  | Var : variable -> baseTerm
  | Name : name -> baseTerm.

Definition baseTerms : Type := list baseTerm.

Definition func_name : Type := string.

Inductive term : Type :=
  | Func : func_name -> list baseTerm -> term
  | Bterm : baseTerm -> term.

Definition terms : Type := list term.

Inductive tpair: Type :=
  | pair : term -> term -> tpair
  | emptypair : tpair.

Definition tpairs : Type := list tpair.

Inductive actionLabel : Type :=
  | ActLabel : name -> terms -> actionLabel.

Inductive label : Type :=
 | BasicLabel : list actionLabel -> label
 | LoggedLabel : actionLabel -> list actionLabel -> label
 | LoggedSIDLabel : baseTerm -> actionLabel -> list actionLabel -> label.

Definition emptyLabel := (BasicLabel []).

Inductive fact : Type :=
  | IN : terms -> fact

  | OUT : terms -> fact

  | K : terms -> fact

  | STATE : name -> terms -> fact

  | FR_P : baseTerm -> fact.

Definition facts : Type := list fact.

Definition trace : Type := list label.

Inductive rule : Type :=
  | RuleSetup : facts -> label -> facts -> rule
  | RuleProto : facts -> label -> facts -> rule.

Definition ruleList : Type := list rule.

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_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 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 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 getTermsAL (al:actionLabel) : terms :=
match al with
   | ActLabel NM TRMS => TRMS
end.

Fixpoint getTermsLabel (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.

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


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

Fixpoint getFreshProtoNamesList (trs: list trace) : list freshNameProto :=
  match trs with
    | [] => []
    | h::ts => appendAny (getFreshProtoNamesinTrace h) (getFreshProtoNamesList ts)
  end.

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

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

Fixpoint commonFreshNames (fr1:list freshNameProto) (fr2:list freshNameProto): list freshNameProto :=
 match fr1 with
  | [] => []
  | fr11 :: fr1s => if (InFresh fr11 fr2) then (fr11::(commonFreshNames fr1s fr2)) else commonFreshNames fr1s fr2
end.



Fixpoint noInputOrOutput (fs:facts) : Prop :=
   match fs with
  | [] => True
  | f::fss => match f with
                | IN ts => False
                | OUT ts => False
                | K ts => noInputOrOutput fss
                | STATE n ts => noInputOrOutput fss
                | FR_P bt => noInputOrOutput fss
               end
  end.

Fixpoint noOutputs (fs:facts) : Prop :=
   match fs with
  | [] => True
  | f::fss => match f with
                | IN ts => noOutputs fss
                | OUT ts => False
                | K ts => noOutputs fss
                | STATE n ts => noOutputs fss
                | FR_P bt => noOutputs fss
               end
  end.

Fixpoint noOutput (f:fact) : Prop :=
  match f with
  | IN t => True
  | OUT t => False
  | K t => True
  | STATE n t => True
  | FR_P fp => True
  end.

Fixpoint noInputs (fs:facts) : Prop :=
   match fs with
  | [] => True
  | f::fss => match f with
                | IN ts => False
                | OUT ts => noInputs fss
                | K ts => noInputs fss
                | STATE n ts => noInputs fss
                | FR_P bt => noInputs fss
               end
  end.

Fixpoint hasInput (fs:facts) : Prop :=
   match fs with
  | [] => False
  | f::fss => match f with
                | IN ts => True
                | OUT ts => hasInput fss
                | K ts => hasInput fss
                | STATE n ts => hasInput fss
                | FR_P bt => hasInput fss
               end
  end.
Fixpoint hasOutput (fs:facts) : Prop :=
   match fs with
  | [] => False
  | f::fss => match f with
                | IN ts => hasOutput fss
                | OUT ts => True
                | K ts => hasOutput fss
                | STATE n ts => hasOutput fss
                | FR_P bt => hasOutput fss
               end
  end.

Fixpoint oneOutput (fs:facts) : Prop :=
   match fs with
  | [] => False
  | f::fss => match f with
                | IN ts => oneOutput fss
                | OUT ts => noOutputs fss
                | K ts => oneOutput fss
                | STATE n ts => oneOutput fss
                | FR_P bt => oneOutput fss
               end
  end.

Fixpoint oneOutputIs (fs:facts) (out:fact) : Prop :=
   match fs with
  | [] => False
  | f::fss => match f with
                | IN ts => oneOutputIs fss out
                | OUT ts1 => match out with
                               | OUT ts2 => ts1=ts2 /\ noOutputs fss
                               | _ => False
                              end
                | K ts => oneOutputIs fss out
                | STATE n ts => oneOutputIs fss out
                | FR_P bt => oneOutputIs fss out
               end
  end.

Fixpoint minOneOutput (fs:facts) : Prop :=
   match fs with
  | [] => False
  | f::fss => match f with
                | IN ts => minOneOutput fss
                | OUT ts => True
                | K ts => minOneOutput fss
                | STATE n ts => minOneOutput fss
                | FR_P bt => minOneOutput fss
               end
  end.

Fixpoint moreThanOneOutput (fs:facts) : Prop :=
   match fs with
  | [] => False
  | f::fss => match f with
                | IN ts => moreThanOneOutput fss
                | OUT ts => oneOutput fss
                | K ts => moreThanOneOutput fss
                | STATE n ts => moreThanOneOutput fss
                | FR_P bt => moreThanOneOutput fss
               end
  end.

Fixpoint oneInput (fs:facts) : Prop :=
   match fs with
  | [] => False
  | f::fss => match f with
                | IN ts => noInputs fss
                | OUT ts => oneInput fss
                | K ts => oneInput fss
                | STATE n ts => oneInput fss
                | FR_P bt => oneInput fss
               end
  end.

Fixpoint oneInputIs (fs:facts) (infact:fact) : Prop :=
   match fs with
  | [] => False
  | f::fss => match f with
                | IN ts1 => match infact with
                               | IN ts2 => ts1=ts2 /\ noInputs fss
                               | _ => False
                              end
                | OUT ts => oneInputIs fss infact
                | K ts => oneInputIs fss infact
                | STATE n ts => oneInputIs fss infact
                | FR_P bt => oneInputIs fss infact
               end
  end.

Fixpoint minOneInput (fs:facts) : Prop :=
   match fs with
  | [] => False
  | f::fss => match f with
                | IN ts => True
                | OUT ts => minOneInput fss
                | K ts => minOneInput fss
                | STATE n ts => minOneInput fss
                | FR_P bt => minOneInput fss
               end
  end.

Fixpoint oneInputAndNoOutputs (fs:facts) : Prop :=
   match fs with
  | [] => False
  | f::fss => match f with
                | IN ts1 => noInputs fss /\ noOutputs fss
                | OUT ts => False
                | K ts => oneInputAndNoOutputs fss
                | STATE n ts => oneInputAndNoOutputs fss
                | FR_P bt => oneInputAndNoOutputs fss
               end
  end.

Fixpoint oneInputAndNoOutputIs (fs:facts) (infact:fact) : Prop :=
   match fs with
  | [] => False
  | f::fss => match f with
                | IN ts1 => match infact with
                               | IN ts2 => ts1=ts2 /\ noInputs fss /\ noOutputs fss
                               | _ => False
                              end
                | OUT ts => False
                | K ts => oneInputAndNoOutputIs fss infact
                | STATE n ts => oneInputAndNoOutputIs fss infact
                | FR_P bt => oneInputAndNoOutputIs fss infact
               end
  end.

Fixpoint oneOutputAndNoInput (fs:facts) : Prop :=
   match fs with
  | [] => False
  | f::fss => match f with
                | IN ts => False
                | OUT ts1 => noOutputs fss /\ noInputs fss
                | K ts => oneOutputAndNoInput fss
                | STATE n ts => oneOutputAndNoInput fss
                | FR_P bt => oneOutputAndNoInput fss
               end
  end.

Fixpoint oneOutputAndNoInputIs (fs:facts) (out:fact) : Prop :=
   match fs with
  | [] => False
  | f::fss => match f with
                | IN ts => False
                | OUT ts1 => match out with
                               | OUT ts2 => ts1=ts2 /\ noOutputs fss /\ noInputs fss
                               | _ => False
                              end
                | K ts => oneOutputAndNoInputIs fss out
                | STATE n ts => oneOutputAndNoInputIs fss out
                | FR_P bt => oneOutputAndNoInputIs fss out
               end
  end.

Fixpoint oneOutputXorInputIs (fs:facts) (trms:terms) : Prop :=
   match fs with
  | [] => False
  | f::fss => match f with
                | IN ts => ts=trms
                | OUT ts => ts=trms
                | K ts => oneOutputXorInputIs fss trms
                | STATE n ts => oneOutputXorInputIs fss trms
                | FR_P bt => oneOutputXorInputIs fss trms
               end
  end.

Fixpoint oneOrNoOutput (fs:facts) : Prop :=
   match fs with
  | [] => True
  | f::fss => match f with
                | IN ts => oneOrNoOutput fss
                | OUT ts => noOutputs fss
                | K ts => oneOrNoOutput fss
                | STATE n ts => oneOrNoOutput fss
                | FR_P bt => oneOrNoOutput fss
               end
  end.

Fixpoint oneOrNoInput (fs:facts) : Prop :=
   match fs with
  | [] => True
  | f::fss => match f with
                | IN ts => noInputs fss
                | OUT ts => oneOrNoInput fss
                | K ts => oneOrNoInput fss
                | STATE n ts => oneOrNoInput fss
                | FR_P bt => oneOrNoInput fss
               end
  end.

Fixpoint oneInputXorOutput (fs:facts) : Prop :=
   match fs with
  | [] => False
  | f::fss => match f with
                | IN ts => noInputs fss /\ noOutputs fss
                | OUT ts => noInputs fss /\ noOutputs fss
                | K ts => oneInputXorOutput fss
                | STATE n ts => oneInputXorOutput fss
                | FR_P bt => oneInputXorOutput fss
               end
  end.

Fixpoint oneOrNoInputXorOutput (fs:facts) : Prop :=
   match fs with
  | [] => True
  | f::fss => match f with
                | IN ts => noInputs fss /\ noOutputs fss
                | OUT ts => noInputs fss /\ noOutputs fss
                | K ts => oneOrNoInputXorOutput fss
                | STATE n ts => oneOrNoInputXorOutput fss
                | FR_P bt => oneOrNoInputXorOutput fss
               end
  end.

Lemma oneInAndNoOutIsOneInOrOutIs : forall facts trms,
 oneInputAndNoOutputIs facts (IN trms) -> oneOutputXorInputIs facts trms.

Lemma oneOutAndNoInIsOneInOrOutIs : forall facts trms,
 oneOutputAndNoInputIs facts (OUT trms) -> oneOutputXorInputIs facts trms.



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.

Fixpoint baseTermAtSamePosBaseTerms (btm:baseTerm) (bts1: list baseTerm) (bts2:list baseTerm) : Prop :=
  match bts1, bts2 with
    | bt1::btst1, bt2::btst2 => ( bt1=btm /\ bt2=btm ) \/ baseTermAtSamePosBaseTerms btm btst1 btst2
    | _, _ => False
  end.

Definition baseTermAtSamePosTerm (bt:baseTerm) (t1: term) (t2: term) : Prop :=
  match t1, t2 with
    | Bterm bt1, Bterm bt2 => bt1=bt /\ bt2=bt
    | Func n1 bts1, Func n2 bts2 => (n1=n2 /\ baseTermAtSamePosBaseTerms bt bts1 bts2)
    | _, _ => False
  end.

Fixpoint baseTermAtSamePosTerms (bt:baseTerm) (ts1: list term) (ts2:list term) : Prop :=
  match ts1, ts2 with
    | t1::ts1t, t2::ts2t => (baseTermAtSamePosTerm bt t1 t2) \/ (baseTermAtSamePosTerms bt ts1t ts2t)
    | _, _ => False
  end.

Definition variableInInputAndOutputOld (x:variable) (newRule:rule) (pastRules: list rule) : Prop :=
  match pastRules with
    | [] => False
    | prule::prules => exists ts1 ts2, member (IN ts1) (premiseFacts newRule)
                       /\ member (OUT ts2) (conclFacts (lastElement prule prules))
                       /\ baseTermAtSamePosTerms (Var x) ts1 ts2
 end.

Fixpoint termPresentInFirstOutputFound (ts:terms) (pastRules:list rule) : Prop :=
  match pastRules with
    | [] => False
    | prule::prules => if (beq_facts (getOutFactConclusion (conclFacts (lastElement prule prules))) [])
                        then termPresentInFirstOutputFound ts prules
                          else (member (OUT ts) (conclFacts (lastElement prule prules)))
  end.


Definition variableInInputAndOutput (x:variable) (newRule:rule) (pastRules: list rule) : Prop :=
  match pastRules with
    | [] => False
    | prule::prules => exists ts1 ts2, (member (IN ts1) (premiseFacts newRule))
                       /\ termPresentInFirstOutputFound ts2 pastRules
                       /\ baseTermAtSamePosTerms (Var x) ts1 ts2
 end.

Fixpoint NameDoesNotAppearInFacts (n:name) (fs:facts) : Prop :=
   match fs with
    | [] => True
    | fh::fst => match fh with
                   | STATE nm1 ts1 => n <> nm1 /\ (NameDoesNotAppearInFacts n fst)
                   | _ => (NameDoesNotAppearInFacts n fst)
                  end
   end.

Fixpoint stateFactNameDoesNotAppear (f:fact) (fs:facts) : Prop :=
   match f with
    | STATE n ts => NameDoesNotAppearInFacts n fs
    | _ => True
   end.

Fixpoint stateAppearsOnce (f:fact) (fs:facts) : Prop :=
  match fs, f with
    | fh::fst, STATE n1 ts1 => match fh with
                                 | STATE n2 ts2 => (n1=n2 /\ ts1=ts2 /\ NameDoesNotAppearInFacts n1 fst)
                                                   \/ (n1 <> n2 /\ stateAppearsOnce f fst)
                                 | _ => stateAppearsOnce f fst
                               end
    | _, _ => False
  end.

Fixpoint TermsInSamePosition (tm1:terms) (tm2:terms) (t1:term) (t2:term) : Prop :=
  match tm1, tm2 with
   | tm11::tm1s, tm21::tm2s => ((eq_term tm11 t1) /\ (eq_term tm21 t2)) \/ (TermsInSamePosition tm1s tm2s t1 t2)
   | [], [] => False
   | [], _::_ => False
   | _::_, [] => False
  end.

Fixpoint AllTermsEqualPositionWise (tm1:terms) (tm2:terms) : Prop :=
  match tm1, tm2 with
   | tm11::tm1s, tm21::tm2s => (eq_term tm11 tm21 ) /\ (AllTermsEqualPositionWise tm1s tm2s)
   | [], [] => True
   | [], _::_ => False
   | _::_, [] => False
  end.

Fixpoint AllSubTermsEqualPositionWise (bt1:list baseTerm) (bt2:list baseTerm) : Prop :=
  match bt1, bt2 with
   | bt11::bt1s, bt21::bt2s => (eq_baseTerm bt11 bt21 ) /\ (AllSubTermsEqualPositionWise bt1s bt2s)
   | [], [] => True
   | [], _::_ => False
   | _::_, [] => False
  end.

Fixpoint PresentInOutputInputConsecutiveRules (RL:list rule) (t1:term) (t2:term) : Prop :=
match RL with
  | r1::rs => match rs with
                    | rs1::rst => match getOutFactProtoRule r1, getInFactProtoRule rs1 with
                                          | [OUT lt1], [IN lt2] => TermsInSamePosition lt1 lt2 t1 t2
                                          | _,_ => False
                                  end
                    | [] => False
                end
  | [] => False
  end.

Fixpoint comparebaseTerms (t1: baseTerms) (t2: baseTerms) : list tpair :=
match t1, t2 with
      | t11::ts1, t21::ts2 =>
                         (match t11, t21 with
                              | Var v1, Var v2 => if (beq_var v1 v2)
                                                                  then (comparebaseTerms ts1 ts2)
                                                              else (pair (Bterm t11) (Bterm t21))::(comparebaseTerms ts1 ts2)
                              | Name nm1, Name nm2 => if (beq_name nm1 nm2)
                                                           then (comparebaseTerms ts1 ts2)
                                                              else (pair (Bterm t11) (Bterm t21))::(comparebaseTerms ts1 ts2)
                              | _, _ => (comparebaseTerms ts1 ts2)
                          end)
      | _,_ => []
  end.

Fixpoint compareTerms (t1: terms) (t2: terms) : list tpair :=
match t1, t2 with
      | t11::ts1, t21::ts2 =>
                        (match t11, t21 with
                        | Bterm bt1, Bterm bt2 => if (beq_baseTerm bt1 bt2)
                                                          then (compareTerms ts1 ts2)
                                                              else (pair t11 t21)::(compareTerms ts1 ts2)
                        | Func n1 bts1, Func n2 bts2 => if (beq_string n1 n2)
                                                           then (comparebaseTerms bts1 bts2)
                                                              else (pair t11 t21)::(compareTerms ts1 ts2)
                        | _, _ => (compareTerms ts1 ts2)
                        end)
      | _,_ => []
  end.


Fixpoint commonInPairs (p1:tpair) (p2:tpair) : bool :=
  match p1,p2 with
    | pair h1 t1, pair h2 t2 => orb (beq_term h1 h2) ( orb (beq_term h1 t2) (beq_term t1 t2))
    | _,_ => false
  end.

Fixpoint commonInList (ts1:terms) (ts2:terms) : bool :=
  match ts1 with
    | ts11::ts1s => orb (memberWith ts11 ts2 beq_term) (commonInList ts1s ts2)
    | [] => false
  end.

Fixpoint joinPairs (p1:tpair) (p2:tpair) : terms :=
  match p1,p2 with
    | pair h1 t1, pair h2 t2 => t2::(t1::(h2::(h1::[])))
    | _,_ => []
  end.

Fixpoint PairToList (p1:tpair) : terms :=
  match p1 with
    | pair h1 t1 => (t1::(h1::[]))
    | emptypair => []
  end.

Fixpoint uniqueTerms (tm: terms) : terms :=
  match tm with
    | t1::ts => if (memberWith t1 ts beq_term) then (uniqueTerms ts) else t1::(uniqueTerms ts)
    | [] => []
  end.

Fixpoint listIsASublist (t:terms) (lt:terms) : bool :=
  match t with
    | t1::ts => andb (memberWith t1 lt beq_term) (listIsASublist ts lt)
    | [] => true
  end.

Fixpoint listMembersAlreadyPresent (t:terms) (lt:list terms) : bool :=
  match lt with
    | lt1::lts => orb (listIsASublist t lt1) (listMembersAlreadyPresent t lts)
    | [] => false
  end.

Fixpoint finalListWithDuplicatesRemoved (t1:terms) (lt: list terms) : terms :=
 match lt with
   | lt1::lts => if (commonInList lt1 t1)
                        then (t1)
                        else (uniqueTerms (appendAny t1 (finalListWithDuplicatesRemoved t1 lts )))
   | [] => []
  end.

Fixpoint finalListsWithDuplicatesRemoved (lt: list terms) : list terms :=
  match lt with
    | t1::ts => (finalListWithDuplicatesRemoved t1 ts) :: (finalListsWithDuplicatesRemoved ts )
    | [] => []
  end.

Fixpoint collectStateFacts (rlst:ruleList) : facts :=
  match rlst with
  | rl1::rls => appendAny (appendAny (getStateFacts (premiseFacts rl1 )) (getStateFacts (conclFacts rl1 ))) (collectStateFacts rls)
  | [] => []
  end.

Fixpoint CheckTermsUSF (f1:fact) (fs:list fact) (t1:term) (t2:term) : Prop :=
match fs with
  | fs1::fst => match f1, fs1 with
                   | STATE n1 tm1, STATE n2 tm2 => if (beq_name n1 n2) then (TermsInSamePosition tm1 tm2 t1 t2)
                                                    else (CheckTermsUSF f1 fst t1 t2)
                   | _,_ => False
                 end
  | [] => False
end.

Fixpoint CheckFactsInUSF (fls:facts) (t1:term) (t2:term) : Prop :=
match fls with
  | f1::fs => (CheckTermsUSF f1 fs t1 t2) \/ (CheckFactsInUSF fs t1 t2)
  | [] => False
end.

Fixpoint CheckTermsUAF (f1:fact) (fs:list fact) (t1:term) (t2:term) : Prop :=
match fs with
  | fs1::fst => match f1, fs1 with
                   | STATE n1 tm1, STATE n2 tm2 => if (beq_name n1 n2) then (TermsInSamePosition tm1 tm2 t1 t2)
                                                    else (CheckTermsUAF f1 fst t1 t2)
                   | _,_ => False
                 end
  | [] => False
end.

Fixpoint CheckFactsInUAF (fls:facts) (t1:term) (t2:term) : Prop :=
match fls with
  | f1::fs => (CheckTermsUAF f1 fs t1 t2) \/ (CheckFactsInUAF fs t1 t2)
  | [] => False
end.


Fixpoint nameAndConstantDoNotAppear (n:name) (c:publicName) (fs:facts) : Prop :=
  match fs with
    | [] => True
    | fh::fst => match fh with
                  | STATE n2 ts => ((n=n2 /\ NotIn (Bterm (Name (Pub c))) ts) \/ n <> n2 )
                                  /\ (nameAndConstantDoNotAppear n c fst)
                  | _ => nameAndConstantDoNotAppear n c fst
                 end
  end.

Fixpoint termIsOnlyConstant (t:term) (n:name) (rs:(list rule)) : Prop :=
  match t with
    | Bterm (Name (Pub c)) => nameAndConstantDoNotAppear n c (allConclFacts rs)
    
    | _ => False
  end.

Fixpoint termIsFresh (t:term) (r:rule) : Prop :=
  match t with
    | Bterm (Var x) => member (FR_P (Var x)) (premiseFacts r)
    | _ => False
  end.

Fixpoint wellFormedSetupPremiseFact (f:fact) : Prop :=
  match f with
  | IN t => True
  | OUT t => False
  | K t => False
  | STATE n t => True
  | FR_P n => match n with
                  | Var v => True
                  | _ => False
                 end
  end.

Definition wellFormedSetupPremiseFacts : facts -> Prop := trueForAll wellFormedSetupPremiseFact.

Fixpoint wellFormedConclusionFact (f:fact) : Prop :=
  match f with
  | IN t => False
  | OUT t => True
  | K t => False
  | STATE n t => True
  | FR_P fp => False
  end.

Fixpoint wellFormedConclusionFacts (fs: facts) : Prop :=
  (match fs with
  | f1::fss => wellFormedConclusionFact f1 /\ wellFormedConclusionFacts fss
  | [] => True
  end)
  /\ (oneOrNoOutput fs).

Fixpoint wellFormedSetupLabel (l:label) :=
  match l with
    | BasicLabel l => True
    | LoggedLabel a l => False
    | LoggedSIDLabel t a l => False
  end.

Fixpoint wellFormedSetupRule (r:rule) : Prop :=
  match r with
    | RuleSetup fs1 l fs2 => ((wellFormedSetupPremiseFacts fs1) /\ (wellFormedSetupLabel l)) /\ (wellFormedConclusionFacts fs2)
    | _ => False
  end.

Definition wellFormedSetupRules : ruleList -> Prop := trueForAll wellFormedSetupRule.


Fixpoint wellFormedProtoPremiseFact (f:fact) : Prop :=
  match f with
  | IN t => True
  | OUT t => False
  | K t => False
  | STATE n t => True
  | FR_P n => match n with
                  | Var v => True
                  | _ => False
                 end
  end.

Fixpoint wellFormedProtoPremiseFacts (fs: facts) : Prop :=
(match fs with
  | f1::fss => wellFormedProtoPremiseFact f1 /\ wellFormedProtoPremiseFacts fss
  | [] => True
  end)
  /\ (oneOrNoInput fs).

Fixpoint wellFormedProtoRule (r:rule) : Prop :=
  match r with
    | RuleProto fs1 l fs2 => (wellFormedProtoPremiseFacts fs1) /\ (wellFormedConclusionFacts fs2)
    | _ => False
  end.

Fixpoint inputsOutputsFromRule (r : rule) : facts :=
  appendAny (getInFactProtoRule r) (getOutFactProtoRule r).

Fixpoint inputsOutputsFromRuleList (rl : ruleList) : facts :=
  match rl with
     | r1::rs => appendAny (inputsOutputsFromRule r1) (inputsOutputsFromRuleList rs)
     | [] => []
  end.

Fixpoint alternateInputsOutputs (fs : facts) : Prop :=
  match fs with
     | f1::fs => match fs with
                      | fs1:: fss => match f1,fs1 with
                                       | IN _, IN _ => False
                                       | OUT _, OUT _ => False
                                       | _, _ => alternateInputsOutputs fs
                                     end
                      | [] => True
                  end
    | [] => True
  end.

Fixpoint wellFormedProtoRules (rl: ruleList) : Prop :=
  (match rl with
  | r1::rs => wellFormedProtoRule r1 /\ wellFormedProtoRules rs
  | [] => True
  end)
  /\ (alternateInputsOutputs (inputsOutputsFromRuleList rl)).

Fixpoint wellFormedRule (r:rule) : Prop :=
  match r with
    | RuleSetup fs1 l fs2 => wellFormedSetupRule r
    | RuleProto fs1 l fs2 => wellFormedProtoRule r
  end.

Fixpoint wellFormedAllowedSequences (allowSeq:list ruleList) : Prop :=
  match allowSeq with
  | al1::als => (wellFormedProtoRules al1) /\ (wellFormedAllowedSequences als)
  | [] => True
  end.

Fixpoint wellFormedLoggedLabel (l:label) :=
  match l with
    | BasicLabel l => False
    | LoggedLabel a l => True
    | LoggedSIDLabel t a l => False
  end.

Fixpoint wellFormedLoggedSIDLabel (l:label) :=
  match l with
    | BasicLabel l => False
    | LoggedLabel a l => False
    | LoggedSIDLabel t a l => True
  end.

Lemma wellFormedTail : forall h ts, wellFormedSetupRules (h::ts) -> wellFormedSetupRules(ts).


Fixpoint InputToOutputProtocolRule (r:rule) : Prop :=
 match r with
    | RuleProto fs1 l fs2 => (oneInput fs1) /\ (noOutputs fs1) /\ (noInputs fs2) /\ (oneOutput fs2)
    | _ => False
  end.

Fixpoint InputToStateProtocolRule (r:rule) : Prop :=
 match r with
    | RuleProto fs1 l fs2 => (oneInput fs1) /\ (noOutputs fs1) /\ (noInputs fs2) /\ (noOutputs fs2)
    | _ => False
  end.

Fixpoint StateToOutputProtocolRule (r:rule) : Prop :=
 match r with
    | RuleProto fs1 l fs2 => (noInputs fs1) /\ (noOutputs fs1) /\ (noInputs fs2) /\ (oneOutput fs2)
    | _ => False
  end.

Fixpoint StateToStateProtocolRule (r:rule) : Prop :=
 match r with
    | RuleProto fs1 l fs2 => (noInputs fs1) /\ (noOutputs fs1) /\ (noInputs fs2) /\ (noOutputs fs2)
    | _ => False
  end.

Fixpoint wellFormedProtoRuleInOutState (r:rule) : Prop :=
(InputToOutputProtocolRule r ) \/ (InputToStateProtocolRule r)
\/ (StateToOutputProtocolRule r) \/ (StateToStateProtocolRule r).

Fixpoint wellFormedProtoRuleNoInOut (rs:ruleList) : Prop :=
  match rs with
    | [] => True
    | r::rss => ((StateToOutputProtocolRule r) /\ (wellFormedProtoRuleFromInOut rss))
                  \/ ((StateToStateProtocolRule r) /\ (wellFormedProtoRuleNoInOut rss))
   end
with
  wellFormedProtoRuleFromInOut (rs:ruleList) : Prop :=
  match rs with
    | [] => True
    | r::rss => ((InputToStateProtocolRule r) /\ (wellFormedProtoRuleNoInOut rss))
                  \/ ((StateToStateProtocolRule r) /\ (wellFormedProtoRuleFromInOut rss))
                    \/ ((InputToOutputProtocolRule r) /\ (wellFormedProtoRuleFromInOut rss))
   end.

Definition wellformedRulesFromState (fs:facts) (rs:ruleList) : Prop :=
  (oneInputXorOutput fs /\ wellFormedProtoRuleFromInOut rs)
    \/ ( noInputOrOutput fs /\ wellFormedProtoRuleNoInOut rs).


Fixpoint InputToOutputSetupRule (r:rule) : Prop :=
 match r with
    | RuleSetup fs1 l fs2 => (oneInput fs1) /\ (noOutputs fs1) /\ (noInputs fs2) /\ (oneOutput fs2)
    | _ => False
  end.

Fixpoint InputToStateSetupRule (r:rule) : Prop :=
 match r with
    | RuleSetup fs1 l fs2 => (oneInput fs1) /\ (noOutputs fs1) /\ (noInputs fs2) /\ (noOutputs fs2)
    | _ => False
  end.

Fixpoint StateToOutputSetupRule (r:rule) : Prop :=
 match r with
    | RuleSetup fs1 l fs2 => (noInputs fs1) /\ (noOutputs fs1) /\ (noInputs fs2) /\ (oneOutput fs2)
    | _ => False
  end.

Fixpoint StateToStateSetupRule (r:rule) : Prop :=
 match r with
    | RuleSetup fs1 l fs2 => (noInputs fs1) /\ (noOutputs fs1) /\ (noInputs fs2) /\ (noOutputs fs2)
    | _ => False
  end.

Fixpoint wellFormedSetupRuleNoInOut (rs:ruleList) : Prop :=
  match rs with
    | [] => True
    | r::rss => ((StateToOutputSetupRule r) /\ (wellFormedSetupRuleFromInOut rss))
                  \/ ((StateToStateSetupRule r) /\ (wellFormedSetupRuleNoInOut rss))
   end
with
  wellFormedSetupRuleFromInOut (rs:ruleList) : Prop :=
  match rs with
    | [] => True
    | r::rss => ((InputToStateSetupRule r) /\ (wellFormedSetupRuleNoInOut rss))
                  \/ ((StateToOutputSetupRule r) /\ (wellFormedSetupRuleFromInOut rss))
                    \/ ((InputToOutputSetupRule r) /\ (wellFormedSetupRuleFromInOut rss))
   end.

Definition wellformedRulesFromStateSetup (fs:facts) (rs:ruleList) : Prop :=
  (oneInputXorOutput fs /\ wellFormedSetupRuleFromInOut rs)
    \/ ( noInputOrOutput fs /\ wellFormedSetupRuleNoInOut rs).

Fixpoint outputRule (r:rule) := StateToOutputProtocolRule r /\ InputToOutputProtocolRule r.
Fixpoint noOutputRule (r:rule) := StateToStateProtocolRule r /\ InputToStateProtocolRule r.
Fixpoint inputRule (r:rule) := InputToStateProtocolRule r /\ InputToOutputProtocolRule r.
Fixpoint noInputRule (r:rule) := StateToStateProtocolRule r /\ StateToOutputProtocolRule r.


Lemma noOutputsMeansNoOutputsInAnyFact: forall f fs, noOutputs (f::fs) -> (noOutput f /\ noOutputs fs).


Lemma oneOrNoOutputFactsInConclusion : forall f1 t f2,
   wellFormedProtoRule (RuleProto f1 t f2) -> oneOrNoOutput f2.

Lemma oneOrNoInputFactsInPremise : forall f1 t f2,
   wellFormedProtoRule (RuleProto f1 t f2) -> oneOrNoInput f1.

Lemma noOutputFactsInPremise : forall f1 l f2,
   wellFormedProtoRule (RuleProto f1 l f2) -> noOutputs f1.

Lemma noInputFactsInConclusion : forall f1 l f2,
   wellFormedProtoRule (RuleProto f1 l f2) -> noInputs f2.

Definition substitution := variable -> name.

Definition substitutions := list substitution.

Definition null : name := Pub "null".

Definition subs_empty : substitution :=
  (fun _ => null).

Definition update (sigma : substitution)
                   (v : variable ) (n : name) :=
  fun x' => if beq_string v x' then n else sigma x'.

Notation "v '!->' n" := (update subs_empty v n) (at level 100).
Notation "v '!->' n ';' sigma" := (update sigma v n)
                              (at level 100, n at next level, right associativity).

Definition compose (sigma1 : substitution) (sigma2 : substitution) : variable -> name :=
  fun v => if (beq_name (sigma1 v) null) then (sigma2 v) else (sigma1 v).

Definition substsAgree (sigma1 : substitution) (sigma2 : substitution) : Prop :=
  forall x, sigma1 x = null \/ sigma2 x = null \/ sigma1 x=sigma2 x.

Lemma agreeSubstComposeOrder : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall x, compose sigma1 sigma2 x = compose sigma2 sigma1 x.

Definition exampleSubs := "ltkA" !-> Fresh_S "ltkA"; subs_empty.

Fixpoint applySubBaseTerm (sigma:substitution) (t:baseTerm) : baseTerm :=
  match t with
  | Var v => if (beq_name (sigma v) null) then (Var v) else Name (sigma v)
  | Name n => Name n
  end.

Definition applySubBaseTerms (sigma:substitution) (ts:baseTerms) : baseTerms
     := map (applySubBaseTerm sigma) ts.

Fixpoint applySubTerm (sigma:substitution) (t:term) : term :=
  match t with
  | Func f bts => Func f (applySubBaseTerms sigma bts)
  | Bterm bt => Bterm (applySubBaseTerm sigma bt)
  end.

Definition applySubTerms : substitution -> terms -> terms
     := fun sigma => map (applySubTerm sigma).

Fixpoint applySubActionLabel (sigma:substitution) (lb:actionLabel) : actionLabel :=
  match lb with
   | ActLabel n ts => ActLabel n (applySubTerms sigma ts)
  end.

Definition applySubLabel (sigma:substitution) (lb:label) : label :=
  match lb with
    | BasicLabel ll => BasicLabel (map ( applySubActionLabel sigma) ll)
    | LoggedLabel lg ll => LoggedLabel (applySubActionLabel sigma lg) (map (applySubActionLabel sigma) ll)
    | LoggedSIDLabel t lg ll => LoggedSIDLabel (applySubBaseTerm sigma t)(applySubActionLabel sigma lg) (map (applySubActionLabel sigma) ll)
  end.

Fixpoint applySubFact (sigma:substitution) (f:fact) : fact :=
match f with
  | IN terms => IN (applySubTerms sigma terms)
  | OUT terms => OUT (applySubTerms sigma terms)
  | K terms => K (applySubTerms sigma terms)
  | STATE name terms => STATE name (applySubTerms sigma terms)
  | FR_P freshName => FR_P (applySubBaseTerm sigma freshName)
  end.

Definition applySubFacts : substitution -> facts -> facts
     := fun sigma => map (applySubFact sigma).

Fixpoint applySubRule (sigma:substitution) (r:rule) : rule :=
match r with
  | RuleSetup f1 l f2 => RuleSetup (applySubFacts sigma f1) (applySubLabel sigma l) (applySubFacts sigma f2)
  | RuleProto f1 l f2 => RuleProto (applySubFacts sigma f1) (applySubLabel sigma l) (applySubFacts sigma f2)
end.

Definition applySubRuleList : substitution -> ruleList -> ruleList := fun sigma => map (applySubRule sigma).

Definition applySubRuleLists : substitution -> list ruleList -> list ruleList := fun sigma => map (applySubRuleList sigma).

Definition applySubTrace : substitution -> trace -> trace := fun sigma => map (applySubLabel sigma).

Definition applySubTraces : substitution -> list trace -> list trace := fun sigma => map (applySubTrace sigma).

Lemma agreeSubstComposeOrderBaseTerm : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall bt, applySubBaseTerm (compose sigma1 sigma2) bt
                                            = applySubBaseTerm (compose sigma2 sigma1) bt.

Lemma agreeSubstComposeOrderBaseTerms : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall bt, applySubBaseTerms (compose sigma1 sigma2) bt
                                            = applySubBaseTerms (compose sigma2 sigma1) bt.

Lemma agreeSubstComposeOrderTerm : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall tm, applySubTerm (compose sigma1 sigma2) tm
                                            = applySubTerm (compose sigma2 sigma1) tm.

Lemma agreeSubstComposeOrderTerms : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall tm, applySubTerms (compose sigma1 sigma2) tm
                                            = applySubTerms (compose sigma2 sigma1) tm.

Lemma agreeSubstComposeOrderActionLabel : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall al, applySubActionLabel (compose sigma1 sigma2) al
                                            = applySubActionLabel (compose sigma2 sigma1) al.

Lemma agreeSubstComposeOrderLabel : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall l, applySubLabel (compose sigma1 sigma2) l
                                            = applySubLabel (compose sigma2 sigma1) l.

Lemma agreeSubstComposeOrderTrace : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall t, applySubTrace (compose sigma1 sigma2) t
                                            = applySubTrace (compose sigma2 sigma1) t.