(*Set Warnings "-notation-overridden,-parsing".*)
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.Structures.Orders.
Require Import Ascii. *)
Require Import Coq.Classes.RelationClasses.
Open Scope string_scope.


Import ListNotations.

Set Nested Proofs Allowed. 

Set Implicit Arguments.
Scheme Equality for list.
(** Contents :

   0: General House Keeping

   1: Syntax definitions 

   2: Equality, membership and extraction functions for the syntax
      2A: Equality functions
      2B: Membership functions
      2C: Extraction of submembers functions

   3: Tests and Definitions for Well formedness 
       3A: Functions to test no or One Input / Output in facts
       3B: Definitions on Variables and Terms  for Equivalence proof 
       3B: Well formedness definitions 
       3C: Some useful lemmas on well formedness

   4: Substitution

   5: Ground terms and rules instances

   6: Tamarin Reduction

   7: Example

   8: Definitions from Chapter 5 of the thesis

   9: Definitions from Chapter 6 of the thesis

   10: Definitions and Proofs from Chapter 6 and 7
      10A: Types of Facts allowed in the system  

  11: Definitions from Chapter 6 of thesis

**)


(** ==========================
  *** 0: General House Keeping
   =========================== *)

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.

(* normal generic append has been overwritten by the string library *)
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.
Proof.
  intros. induction H. induction H0. reflexivity.
Qed.

Lemma listEqHead : forall {A:Type} (h:A) ts2 ts1, ts2=ts1 -> h::ts2=h::ts1.
Proof.
  intros. apply listEq. reflexivity. assumption.
Qed.

Lemma listEqTail : forall {A:Type} (h1:A) h2 ts, h1=h2 -> h1::ts=h2::ts.
Proof.
  intros. apply listEq. assumption. reflexivity. 
Qed.

(* This removes the first matching element in a list, if any *) 
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 subList {A:Type} : (list A) -> (list A) -> Prop :=
 | Empty_SubList : forall l, subList [] l
 | Same_SubList  : forall l1 l2 h1, subList l1 l2 -> subList (h1::l1) (h1::l2)
 | Next_SubList  : forall (l1:list A) l2 h, subList l1 (consEnd l2 h) -> subList l1 (h::l2).

 *)

(* Fixpoint subList {A:Type}  (l1:list A)  (l2:list A) : Prop :=
  match l1 with
    | []     => True
    | h1::t  => (In h1 l2) /\ (subList t (removeElement h1 l2))
  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.
Proof.
  induction rl.
  + apply Empty_O_SubList.
  + apply Same_O_SubList. assumption.
Qed.

(* 
Lemma idIsSublist : forall {A:Type} (rl:list A), subList rl rl.
Proof.
  induction rl.
  + apply Empty_SubList.
  + apply Same_SubList. assumption.
Qed.
 *)


 
(** ============================
       1: Syntax definitions 
    ===========================**)

(*These are the domains of terms, I think this can probabaly be improved **)

Definition freshNameSetup : Type := string.  (* fr from tamarin *) 
Definition freshNameProto : Type := string.  (* fr from tamarin *)

Definition sidTerm : Type := string. (* Session ID*)

Definition publicName : Type := string.  (* pub from tamarin *)

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.
(** Action Label with facts (values) *)

Inductive actionLabel : Type :=
  | ActLabel : name -> terms -> actionLabel. (** I'm not sure if this should be name, of some over kind *)

(** Label with facts : List of Action Label with facts (values) *)

(*
Def2,2 in the paper adds optional logs into labels
We model this by replacing labels as lists of action labels: Definition label : Type := list actionLabel.
with two subtypes for labels i.e., labels with logs, and labels without logs. 
*)

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   (** An input **)
  | OUT   : terms -> fact   (** An output **)  
  | K     : terms -> fact   (** Attacker knowledge *)
  | STATE : name -> terms -> fact(** General protocol state informtaion. I'm not sure if this should be name, or some over kind kind of identifier*)
  | FR_P  : baseTerm -> fact.   (** A new fresh name in protocol stage**)

Definition facts : Type := list fact.

(** A rule is a triple : pattern followed by Label followed by patterns *)

Definition trace : Type := list label.

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

(* A protocol is modelled as a list of these rules:*)
(** A ruleList : List of rule *)
Definition ruleList : Type := list rule.



(** =================================== 
 ***  2: Equality, membership and extraction functions for the syntax
 =================================== **)
(** =================================== 
      2A: Equality functions
 =================================== **)
(** We have defined two versions for the same definitions
 anything starting with "b" returns a bool otherwise Prop *)

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

(** "beq_string s1 s2 "checks whether two strings are equal *)

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.
Proof.
  intros. unfold beq_string in H. destruct (string_dec s1 s2) eqn:D. assumption. inversion H.
Qed.

(* This is probably defined in one of the standard libs *)
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.

(* This is probably defined in one of the standard libs *)
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.

(** "beq_string_list s1 s2 "checks whether two lists of strings are equal *)

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).

(** "eq_base_term t1 t2 "checks whether two baseterms  are equal *)

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.
Proof.
  intros. destruct n1; destruct n2; inversion H; 
  apply beq_string_EQ in H1; subst; reflexivity.
Qed.

Definition name_dec : forall b1 b2 : name, {b1 = b2} + {b1 <> b2}.
   decide equality;apply string_dec.
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}.
   decide equality.
   + apply string_dec.
   + destruct n0; destruct n1.
    - decide equality;  apply string_dec.
    - decide equality;  apply string_dec.
    - right. unfold not. intro. inversion H.
    - right. unfold not. intro. inversion H.
    - decide equality;  apply string_dec.
    -  right. unfold not. intro. inversion H.
    -  right. unfold not. intro. inversion H.
    -  right. unfold not. intro. inversion H.
    - decide equality;  apply string_dec.
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}.
   decide equality. apply baseTerm_dec.
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}.
   decide equality.
   + apply baseTerms_dec.
   + apply string_dec.
   + apply baseTerm_dec.
Defined.

Definition terms_dec : forall ts1 ts2 : terms, {ts1 = ts2} + {ts1 <> ts2}.
   decide equality. apply term_dec.
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}.
   decide equality; try apply terms_dec.
   + apply name_dec.
   + apply baseTerm_dec.
Defined.

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


Definition tpair_dec : forall tp1 tp2 : tpair, {tp1 = tp2} + {tp1 <> tp2}.
   decide equality; try apply terms_dec.
   + apply term_dec.
   + apply term_dec.
Defined.

Definition tpairs_dec : forall ts1 ts2 : tpairs, {ts1 = ts2} + {ts1 <> ts2}.
   decide equality. apply tpair_dec.
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}.
   decide equality.
   + apply terms_dec.
   + apply name_dec.
Defined.

Definition actionLabels_dec : forall t1 t2 : list actionLabel, {t1 = t2} + {t1 <> t2}.
   decide equality. apply actionLabel_dec.
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}.
      decide equality. 
      apply actionLabels_dec. 
      apply actionLabels_dec. apply actionLabel_dec. 
      apply actionLabels_dec. apply actionLabel_dec. 
      apply baseTerm_dec.
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}.
   decide equality; try apply facts_dec; try apply label_dec.
Defined.

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


(** ==============================================
      2B: Membership functions : MEMBERSHIP TESTS 
==================================================**)

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.


(* This removes the first matching fact in a list, if any *) 
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.

(* 
Fixpoint subList (l1:list fact)  (l2:list fact) : Prop :=
  match l1 with
    | []     => True
    | h1::t  => (In h1 l2) /\ (subList t (removeFact h1 l2))
  end.
 *)
(*
Lemma idIsSublist : forall rl, subList rl rl.
Proof.
  induction rl.
  + reflexivity.
  + simpl. split. left. auto. unfold removeFact. simpl. 
Qed.

 *)
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.

(** "inLabel al lb" verifies whether the action label "al" is in the
label "lb" or not **)
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.


(** "inLoggedSIDLabel al lb" verifies whether the action label "al" is in the
LoggedSIDLabel "lb" or not **)
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.

(** "al_in_Trace al tr" verifies whether the action label "al" is in the
trace "tr" or not **)
Fixpoint al_in_Trace (al:actionLabel) (tr:trace) : Prop :=
    match tr with
      | [] => False
      | lbl1 :: lbs => inLabel al lbl1 \/ (al_in_Trace al lbs)
    end.  


(** "LoggedAL_in_Trace al tr" verifies whether the action label "al" is in the
trace "tr" or not **)
Fixpoint LoggedAL_in_Trace (al:actionLabel) (tr:trace) : Prop :=
    match tr with
      | [] => False
      | lbl1 :: lbs => inLoggedSIDLabel al lbl1 \/ (LoggedAL_in_Trace al lbs)
    end.


(** "LoggedLbl_in_Trace al tr" verifies whether the Label "lbl" is in the
trace "tr" or not **)
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.


(** "b_lbl_inTrace lb tr" verifies whether label "lb" is in trace "tr" or not **)
(** "lb" is either the first member of "tr" or somehere before the end of trace**)
 
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.

(* MEMBERSHIP TESTS for template *)


(** "beq_actionLabelName a1 a2 "checks whether two action labels in template have the same name *)
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).

(** "inLabelName al lb" verifies whether the action label "al" is in the
label "lb" or not **)
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.


(* For Definition SelectName *)

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.


(** ================================================================================
    2C: Extraction of submembers : Functions to extract facts/logs etc. from rules 
  =================================================================================*)


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.

(* For Tamarin Reduction *)

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      => [] (*We assume that there will not be any label of this type after annotating the rules with SID*)
   end.



(* "getSID lbl SID" holds if "SID" used in the label "lbl". 
 *)
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.


(* N.B. variables in a trace may become fresh names later, so this only really
   makes sense for a ground trace *)

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.


(**=====================================================
   3: Tests and Definitions for Well formedness 
  =======================================================**)

(* ===========================================
  3A: Functions to test no or One Input / Output in facts
  ==========================================================*)

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.


(* Rajiv:Proved.  *)
Lemma oneInAndNoOutIsOneInOrOutIs : forall facts trms,
 oneInputAndNoOutputIs facts (IN trms) ->  oneOutputXorInputIs facts trms.
Proof.
    intros. induction facts0.
      + inversion H.
      + destruct a.
        - simpl in H. simpl. destruct H. simpl. auto.
        - simpl in H.  inversion H.
        - simpl in H. simpl. apply IHfacts0. auto.
        - simpl in H. simpl. apply IHfacts0. auto.
        - simpl in H. simpl. apply IHfacts0. auto.
Qed.


(* To be used *)
Lemma oneOutAndNoInIsOneInOrOutIs : forall facts trms,
 oneOutputAndNoInputIs facts (OUT trms) ->  oneOutputXorInputIs facts trms.
Proof.
  intros. induction facts0.
    + inversion H.
    + destruct a.
        - simpl in H.  inversion H.
        - simpl in H. simpl. destruct H. auto.
        - simpl in H. simpl. apply IHfacts0. auto.
        - simpl in H. simpl. apply IHfacts0. auto.
        - simpl in H. simpl. apply IHfacts0. auto.
Qed.
 

 
(**=====================================
 constants and variables in term 
 ========================================*)

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.


(* Some general functions for working with the syntax *)
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.




(** ====================================================================
  3B : Definitions on Variables and Terms  for Equivalence proof 
  ====================================================================*)



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.

(* "variableInInputAndOutput" verifies if the terms present in the Input fact 
are present in the first previous OUT fact from earlier rules.
There may either be no OUT fact in the previous rule, or, if there is, then the terms must match up. *)

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.


(* Helper functions for Def 8 *)
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.


(* Helper functions for Def 10 *)
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) (*?? What if Functions have different names?*)
                        end)
      |  _,_               => []
  end.



(* Functions to process Pairs and Lists*)

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.


(* If pairs have a common element, join the pairs in a list  *)
Fixpoint joinPairs (p1:tpair) (p2:tpair) : terms :=
  match p1,p2 with
    | pair h1 t1, pair h2 t2 => t2::(t1::(h2::(h1::[])))
    | _,_            => []
  end.

(* If pair does not have any common element with other pair, convert it to a list  *)
Fixpoint PairToList (p1:tpair) : terms :=
  match p1 with
    | pair h1 t1   => (t1::(h1::[]))
    | emptypair    => []
  end.

(* "uniqueTerms" is essentially union of terms *)
Fixpoint uniqueTerms (tm: terms) : terms :=
  match tm with
    | t1::ts  => if (memberWith t1 ts beq_term) then (uniqueTerms ts) else t1::(uniqueTerms ts)
    | []          => []
  end.


(* "listIsASublist t t" verifies if all the members of first list "t" present in the second list "lt" *)
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.


(* "finalListWithDuplicatesRemoved" is essentially union of lists that ignores any sublists present *)
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.


(* "finalListWithDuplicatesRemoved" is essentially union of lists that ignores any sublists present *)
Fixpoint finalListsWithDuplicatesRemoved (lt: list terms)  : list terms :=
  match lt with
    | t1::ts  => (finalListWithDuplicatesRemoved t1 ts) :: (finalListsWithDuplicatesRemoved ts ) 
    | []          => []
  end.


(* Collect all the state facts from the rule list *)
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.


(* In the term, we just a consider a public name (we exclude an application of functions to fixed
   public names, but could add this if needed) *)

(* True if the constant c does not appear in a state called n *)
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)
    (* We could add functions case here *)
    | _ => False
  end.

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




(** ================================
***   3C: Well formedness definitions 
====================================*)

(* well Formedness of Setup Rules *)

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.

(* well Formedness of Protocol Rules *)


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).
Proof.
   unfold wellFormedSetupRules. simpl. intros. inversion H. assumption.
Qed.

(* ====================================================*)
(* TOM: new definition of well formed Protocol rule *)
(* ====================================================*)

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). 


(* Rajiv: New definition of well formed Setup rule *)
(* Eaxctly same well formedness conditions as those of protocol rules  *)

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.

(* ================================================
  3D: Some useful lemmas on well formedness
  ================================================= *)
(* Unused *)

Lemma noOutputsMeansNoOutputsInAnyFact: forall f fs, noOutputs (f::fs) -> (noOutput f /\ noOutputs fs).
Proof.
 intros;
 induction fs.
  + split.
    - induction f.
      * apply H.
      * apply H.
      * apply H.
      * apply H.
      * apply H.
    -  induction f.
      * apply H. 
      * simpl in H. simpl. inversion H.
      * apply H. 
      * apply H.  
      * apply H.  
  + split. 
    - induction f.
      * simpl in H. destruct a. simpl. apply IHfs. simpl. apply H. simpl; inversion H.  destruct IHfs. simpl. apply H. apply H0. destruct IHfs. simpl. apply H. apply H0.
        destruct IHfs. simpl. apply H. apply H0. 
      * auto.
      * destruct IHfs. simpl. simpl in H. destruct a. auto. inversion H. eauto. auto. auto. auto. 
      * destruct IHfs. simpl. simpl in H. destruct a. auto. inversion H. eauto. auto. auto. auto. 
      * destruct IHfs. simpl. simpl in H. destruct a. auto. inversion H. eauto. auto. auto. auto. 
    -  simpl in H. destruct f. auto. inversion H. auto. auto.  auto. 
Qed.

(* Unused *)

Lemma oneOrNoOutputFactsInConclusion : forall  f1 t f2,
   wellFormedProtoRule (RuleProto f1 t f2) -> oneOrNoOutput f2.
Proof. intros. inversion H. induction f2.
      + apply H1.
      + apply H1.
Qed.

(* Unused *)
Lemma oneOrNoInputFactsInPremise : forall  f1 t f2,
   wellFormedProtoRule (RuleProto f1 t f2) -> oneOrNoInput f1.
Proof. intros. inversion H. induction f1.
      + apply H0.
      + apply H0.
Qed.

(* Unused *)
Lemma noOutputFactsInPremise : forall  f1 l f2,
   wellFormedProtoRule (RuleProto f1 l f2) -> noOutputs f1.
Proof. intros. inversion H.  induction f1.
      + apply H0.
      + destruct a.
        - simpl. apply IHf1.
          * simpl in H. simpl. split. destruct H. destruct H. destruct H. apply H4. apply H1.
          * simpl in H.  destruct H. destruct H. destruct H. apply H4.
        - simpl in H. simpl. destruct H. destruct H. destruct H. auto.
        - simpl. apply IHf1.
          * simpl in H.  destruct H. destruct H. destruct H. inversion H.        
         * simpl in H.  destruct H. destruct H. destruct H. inversion H.
        - simpl. apply IHf1.
         * simpl in H. simpl. split. destruct H. destruct H. destruct H. apply H4. apply H1.
         * simpl in H.  destruct H. destruct H. destruct H. apply H4.
        - simpl. apply IHf1.
         * simpl in H. simpl. split. destruct H. destruct H. destruct H. apply H4. apply H1.
         * simpl in H.  destruct H. destruct H. destruct H. apply H4.
Qed.

(* Unused *)
Lemma noInputFactsInConclusion : forall  f1 l f2,
   wellFormedProtoRule (RuleProto f1 l f2) -> noInputs f2.
Proof. intros. inversion H.  induction f2.
      + apply H1.
      + destruct a.
        - simpl. simpl in H1. destruct H1. destruct H1. auto.
        - simpl. apply IHf2.
          * simpl. split. simpl in H.  destruct H. destruct H2. destruct H2. apply H; apply H4. 
            simpl in H1. destruct H1. destruct H1. apply H3.
          *  simpl in H1. destruct H1. destruct H1. apply H3.
        - simpl. simpl in H1. destruct H1. destruct H1. inversion H1.
        - simpl. simpl in H1. destruct H1. destruct H1. apply IHf2. 
          * simpl. split.  apply H0. apply H3.
          * auto.
        - simpl. simpl in H1. destruct H1. destruct H1. apply IHf2. 
          * simpl. split.  apply H0. apply H3.
          * auto.
Qed.

(** ===================== 
  *** 4: Substitution
 ===================== **)

(** This section defines the mechanics of how Substitution works. 

 based on SOFTWARE FOUNDATIONS: 
https://softwarefoundations.cis.upenn.edu/lf-current/Maps.html
https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html **)

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.
Proof.
  intros. unfold compose. 
  destruct (beq_name (sigma1 x0) null) eqn:D1; destruct (beq_name (sigma2 x0) null) eqn:D2.
  + apply beq_name_EQ in D1. apply beq_name_EQ in D2. rewrite D1. rewrite D2. reflexivity. 
  + reflexivity.
  + reflexivity.
  + unfold substsAgree in H. destruct (H x0).
   - rewrite H0 in D1. inversion D1.
   - inversion H0.
     * rewrite H1 in D2. inversion D2.
     * assumption.
Qed.

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.
Proof.
  intros. destruct bt.
  + simpl. unfold compose. destruct (beq_name (sigma1 v) null) eqn:D1; destruct (beq_name (sigma2 v) null) eqn:D2.
    - rewrite D1. reflexivity.
    - rewrite D2. reflexivity.
    - rewrite D1. reflexivity.
    - rewrite D1. rewrite D2.  unfold substsAgree in H. destruct (H v).
      * rewrite H0 in D1. inversion D1.
      * inversion H0.
        ++ rewrite H1 in D2.  inversion D2.
        ++ rewrite H1.  reflexivity. 
   +  reflexivity. 
Qed.

Lemma agreeSubstComposeOrderBaseTerms : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall bt, applySubBaseTerms (compose sigma1 sigma2) bt 
                                            = applySubBaseTerms (compose sigma2 sigma1) bt.
Proof.
  intros. induction bt.
  + reflexivity. 
  + simpl. apply listEq. apply agreeSubstComposeOrderBaseTerm. assumption. apply IHbt.
  Qed.

Lemma agreeSubstComposeOrderTerm : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall tm, applySubTerm (compose sigma1 sigma2) tm 
                                            = applySubTerm (compose sigma2 sigma1) tm.
Proof.
  intros. induction tm.
  + simpl. apply f_equal. apply agreeSubstComposeOrderBaseTerms. assumption.
  + simpl. apply f_equal. apply agreeSubstComposeOrderBaseTerm. assumption.
Qed.

Lemma agreeSubstComposeOrderTerms : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall tm, applySubTerms (compose sigma1 sigma2) tm 
                                            = applySubTerms (compose sigma2 sigma1) tm.
Proof.
  intros. induction tm.
  + reflexivity.
  + simpl. apply listEq. 
    - apply agreeSubstComposeOrderTerm. assumption.
    - assumption.
Qed.

Lemma agreeSubstComposeOrderActionLabel : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall al, applySubActionLabel (compose sigma1 sigma2) al 
                                            = applySubActionLabel (compose sigma2 sigma1) al.
Proof. 
 intros. induction al. induction t.
  + reflexivity.
  + simpl. apply f_equal. apply listEq.
    - apply agreeSubstComposeOrderTerm. assumption.
    - apply agreeSubstComposeOrderTerms. assumption.
Qed.


Lemma agreeSubstComposeOrderLabel : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall l, applySubLabel (compose sigma1 sigma2) l 
                                            = applySubLabel (compose sigma2 sigma1) l.
Proof.
 intros. induction l as [ls|al ls|b al ls].
  +  induction ls.
    * reflexivity.
    * simpl. apply f_equal. apply listEq.
      ** apply agreeSubstComposeOrderActionLabel.  assumption.
      **  inversion IHls. rewrite H1. reflexivity.
  + induction ls.
    * simpl. apply agreeSubstComposeOrderActionLabel with (al:=al) in H.
      rewrite H. reflexivity.
    * simpl.  assert (HA := H).
      apply agreeSubstComposeOrderActionLabel with (al:=al) in H. 
      rewrite H. apply f_equal. apply listEq.
      ** apply agreeSubstComposeOrderActionLabel.  assumption.
      ** inversion IHls.  rewrite H2. reflexivity.
  + induction ls.
    * simpl. assert (HA := H). apply agreeSubstComposeOrderActionLabel with (al:=al) in H.
      rewrite H. apply agreeSubstComposeOrderBaseTerm with (bt:=b) in HA.
      rewrite HA. reflexivity.
    * simpl in IHls. inversion IHls. simpl. assert (HA := H). assert (HB := H). assert (HC := H). 
      apply agreeSubstComposeOrderActionLabel with (al:=al) in H.
      apply agreeSubstComposeOrderActionLabel with (al:=a) in HA.
      rewrite H. rewrite HA. apply agreeSubstComposeOrderBaseTerm with (bt:=b) in HB.
      rewrite HB. apply f_equal. apply listEq.
      -- reflexivity.
      -- apply H3.
Qed.

Lemma agreeSubstComposeOrderTrace : forall sigma1 sigma2,
  substsAgree sigma1 sigma2 -> forall t, applySubTrace (compose sigma1 sigma2) t 
                                            = applySubTrace (compose sigma2 sigma1) t.
Proof.
  intros. induction t.
  + reflexivity.
  + simpl. apply listEq.
    - apply agreeSubstComposeOrderLabel. assumption.
    - apply IHt.
Qed.
 
 

(** =================================== 
 *** 5: Ground terms and rule instances 
 =================================== **)

(* This section defines what a ground instance of a rule, and facts, are *)
(* This is used by the "run" prediciate in the next section *)

(** Ground Defs, these might be better as Props, rather than bools
    I'm not sure at this point, we can always change these to Props later **)

Fixpoint groundBaseTerm (ts:baseTerm) : Prop :=
  match ts with
    | Var v => False
    | _ => True
  end.

Definition groundBaseTerms : baseTerms -> Prop := trueForAll groundBaseTerm.

Fixpoint groundTerm (t:term) : Prop :=
  match t with 
    | Func f ts => groundBaseTerms ts
    | Bterm (Name (Pub n)) => True
    | Bterm (Name (Fresh_S n)) => True
    | Bterm (Name (Fresh_P n)) => True
    | _ => False
  end.

Fixpoint groundTerms (ts:terms) : Prop :=
  match ts with 
    | t::ts => groundTerm t /\ groundTerms ts
    | [] => True
  end.

Fixpoint groundFact (f:fact) : Prop :=
 match f with
  | IN    ts    => groundTerms ts
  | OUT   ts    => groundTerms ts
  | K     ts    => groundTerms ts
  | STATE n ts  => groundTerms ts
  | FR_P  fn    => True
 end.

Fixpoint groundFacts (fs:facts) : Prop :=
  match fs with 
    | f::fs => groundFact f /\ groundFacts fs
    | [] => True
  end.

Definition groundActionLabel (al:actionLabel) : Prop :=
  match al with 
    | ActLabel n ts => groundTerms ts
  end.

Fixpoint groundBasicLabel (lb:list actionLabel) : Prop :=
  match lb with 
    | al::als => groundActionLabel al /\ groundBasicLabel als
    | [] => True
  end.

Definition groundLoggedLabel (lg:actionLabel) (lb:list actionLabel) : Prop :=
   groundActionLabel lg /\ groundBasicLabel lb.


Definition groundLoggedSIDLabel (t:baseTerm) (lg:actionLabel) (lb:list actionLabel) : Prop :=
   groundBaseTerm t /\ groundActionLabel lg /\ groundBasicLabel lb.

Definition groundLabel (lb:label) : Prop :=
  match lb with 
    | BasicLabel ls => groundBasicLabel ls
    | LoggedLabel lg ls => groundLoggedLabel lg ls
    | LoggedSIDLabel t lg ls => groundLoggedSIDLabel t lg ls
  end.

Definition groundRule (r:rule) : Prop :=
  match r with 
    | RuleProto f1 l f2 => groundFacts f1 /\ groundFacts f2 /\ groundLabel l
    | RuleSetup f1 l f2 => groundFacts f1 /\ groundFacts f2 /\ groundLabel l
  end.


(* Ginsts is a function unsed in Tamarin generate all possible ground 
   instances of a rule set.  *)

Inductive ginst : rule -> rule -> Prop :=
  | Ginst : forall r1 r2, (exists sigma, (applySubRule sigma r2) = r1) /\ (groundRule r1) -> ginst r1 r2.

Inductive ginsts : rule -> ruleList -> Prop :=
  | GinstHead : forall r1 r2 rs, (ginst  r1 r2) -> ginsts r1 (r2::rs)
  | GinstTail : forall r1 r2 rs, (ginsts r1 rs) -> ginsts r1 (r2::rs).


(* GinstsWithSigma is a function unsed in Tamarin generate a specific ground 
   instance of a rule set using substitution sigma.  *)

Inductive ginstWithSigma : rule -> substitution -> rule -> Prop :=
  | GinstSigma : forall r1 r2 sigma, (applySubRule sigma r2) = r1 /\ groundRule r1 -> ginstWithSigma r1 sigma r2.

Inductive ginstsWithSigma : rule -> substitution -> ruleList -> Prop :=
  | GinstHeadSigma : forall r1 r2 rs sigma, 
                                  (ginstWithSigma  r1 sigma r2) -> ginstsWithSigma r1 sigma (r2::rs)
  | GinstTailSigma : forall r1 r2 rs sigma, 
                                  (ginstsWithSigma r1 sigma rs) -> ginstsWithSigma r1 sigma (r2::rs).

Lemma composeSubstBaseTerm : forall bt (sigma1:substitution) (sigma2:substitution),
        groundBaseTerm (applySubBaseTerm sigma1 bt)
              -> groundBaseTerm (applySubBaseTerm (compose sigma1 sigma2) bt).
Proof.
  intros. destruct bt.
   - unfold applySubBaseTerm. unfold applySubBaseTerm in H. 
     unfold compose. destruct (beq_name (sigma1 v) null) eqn:D1.
     + inversion H.
     + rewrite D1. reflexivity. 
   - reflexivity.
Qed.



Lemma composeSubstBaseTerms : forall bt (sigma1:substitution) (sigma2:substitution),
        groundBaseTerms (applySubBaseTerms sigma1 bt) 
              -> groundBaseTerms (applySubBaseTerms (compose sigma1 sigma2) bt).
Proof.
  intros. induction bt.
  + reflexivity.
  + simpl. unfold groundBaseTerms. simpl. split.
    - inversion H. apply composeSubstBaseTerm. apply H0.
    - apply IHbt. unfold groundBaseTerms in H. simpl in H. destruct H. apply H0.
Qed. 



Lemma composeSubstGroundTerm : forall tm (sigma1:substitution) (sigma2:substitution),
        groundTerm (applySubTerm sigma1 tm)
              -> groundTerm (applySubTerm (compose sigma1 sigma2) tm).
Proof.
  intros. induction tm.
  + simpl. eapply composeSubstBaseTerms. simpl in H. simpl. auto.
  + destruct b. 2:{
    - unfold applySubTerm. unfold applySubBaseTerm. unfold groundTerm. destruct n0; reflexivity. }
    - unfold  applySubTerm in H. unfold  applySubBaseTerm in H. unfold groundTerm in H.  destruct (beq_name (sigma1 v) null) eqn:D1.
      * inversion H.
      * unfold  applySubTerm. unfold  applySubBaseTerm. unfold groundTerm.  unfold compose. rewrite D1. rewrite D1. apply H.
Qed.



Lemma composeSubstGroundTerms : forall tms (sigma1:substitution) (sigma2:substitution),
        groundTerms (applySubTerms sigma1 tms)
              -> groundTerms (applySubTerms (compose sigma1 sigma2) tms).
Proof.
  intros. induction tms.
  + reflexivity.
  + simpl. inversion H. split.
    - apply composeSubstGroundTerm. apply H0.
    - apply IHtms. apply H1.
Qed.


Lemma composeSubstGroundAL : forall al (sigma1:substitution) (sigma2:substitution),
        groundActionLabel (applySubActionLabel sigma1 al)
              -> groundActionLabel (applySubActionLabel (compose sigma1 sigma2) al).
Proof.
  intros. induction al. simpl. apply composeSubstGroundTerms.
  unfold groundActionLabel in H. simpl in H. assumption.
  Qed.

Lemma composeSubstGroundBasicLabel : forall l (sigma1:substitution) (sigma2:substitution),
        groundBasicLabel (map ( applySubActionLabel sigma1) l) 
              -> groundBasicLabel (map (applySubActionLabel (compose sigma1 sigma2)) l).

Proof. intros. induction l.
 + simpl.  reflexivity.
 + simpl. split. unfold groundLabel in H. simpl in H. destruct H.
    - apply composeSubstGroundAL. auto.
    - apply IHl. inversion H. apply H1.
Qed.




Lemma composeSubstGroundLoggedLabel : forall al ls (sigma1:substitution) (sigma2:substitution),
        groundLoggedLabel 
               (applySubActionLabel sigma1 al) 
               (map (applySubActionLabel sigma1) ls)
              
            -> groundLoggedLabel 
               (applySubActionLabel (compose sigma1 sigma2) al) 
               (map (applySubActionLabel (compose sigma1 sigma2)) ls).

Proof.
  intros. unfold groundLoggedLabel in H.  inversion H.
  unfold groundLoggedLabel. split.
  - apply composeSubstGroundAL. apply H0.
  - induction ls.
    +  simpl. reflexivity.
    + simpl.  inversion H1.  split. 
      * apply composeSubstGroundAL. apply  H2. 
      * apply IHls. split. 
        -- apply  H0. 
        -- apply  H3.
        -- apply  H3. 
Qed.



Lemma composeSubstGroundLoggedSIDLabel : forall al ls t (sigma1:substitution) (sigma2:substitution),
        groundLoggedSIDLabel 
               (applySubBaseTerm sigma1 t) 
               (applySubActionLabel sigma1 al) 
               (map (applySubActionLabel sigma1) ls)
              
            -> groundLoggedSIDLabel 
               (applySubBaseTerm (compose sigma1 sigma2) t)
               (applySubActionLabel (compose sigma1 sigma2) al) 
               (map (applySubActionLabel (compose sigma1 sigma2)) ls).

Proof.
  intros. unfold groundLoggedSIDLabel in H.  inversion H. inversion H1. unfold groundLoggedSIDLabel. split.
  - apply composeSubstBaseTerm. apply  H0.
  - split.
    + apply composeSubstGroundAL. apply  H2.
    + apply composeSubstGroundBasicLabel. apply H3.
Qed.



Lemma composeSubstGroundLabel : forall l (sigma1:substitution) (sigma2:substitution),
        groundLabel (applySubLabel sigma1 l) 
              -> groundLabel (applySubLabel (compose sigma1 sigma2) l).

Proof.
  intros.  induction l as [ls|al ls|ls]. 
  - simpl. apply composeSubstGroundBasicLabel. unfold groundLabel in H. simpl in H.
    assumption. 
  - unfold groundLabel. simpl. apply composeSubstGroundLoggedLabel. 
    unfold groundLabel in H.  simpl in H. apply H. 
  - unfold groundLabel. simpl. apply composeSubstGroundLoggedSIDLabel.
    unfold groundLabel in H.  simpl in H. apply H.
Qed.



(** ====================
 ** 6: Tamarin Reduction
 ======================= **)

(* This section defines Tamarin rule for generating traces *)
(* N.B. Tamarin enforces additional constrainst of allowed traces, 
   i.e., freshnames do not repeat. We do not enforce these here, 
   but we can add them later if needed *)


(* This section defines how a term can be reduced with a particular rule set *)

(** "reduceWithRule r f1 l f2" means that the rule "r" can match the
 facts "f1" and produce the facts "f2" with the label "label"**)

Inductive reduceWithGroundRule : rule -> facts -> label -> facts -> Prop :=
   | R_match : forall r s1, (subList (premiseFacts r) s1) -> 
                       reduceWithGroundRule r s1 (labelR r) 
                         (appendAny (conclFacts r) (removeFacts (premiseFacts r) s1)).

Definition reduceWithRule (r1:rule) (f:facts) (l:label) (f2:facts) : Prop := 
    exists r2,  (ginst r2 r1) /\ reduceWithGroundRule r2 f l f2.  

Definition reduceWithRules (rs:ruleList) (f:facts) (l:label) (f2:facts) : Prop := 
    exists r2,  (ginsts r2 rs) /\ reduceWithGroundRule r2 f l f2.


(** "reduceWithRuleSigma r f1 l f2" means that the rule "r" can match the
 facts "f1" and produce the facts "f2" with the label "label"**)

Definition reduceWithRuleSigma (r1:rule) (sigma:substitution) (f:facts) (l:label) (f2:facts) : Prop := 
    exists r2,  (ginstWithSigma r2 sigma r1) /\ reduceWithGroundRule r2 f l f2.  

Definition reduceWithRulesSigma (rs:ruleList) (sigma:substitution) (f:facts) (l:label) (f2:facts) : Prop := 
    exists r2,  (ginstsWithSigma r2 sigma rs) /\ reduceWithGroundRule r2 f l f2.

Definition freshRuleS (n:freshNameSetup) : rule := (RuleSetup [] emptyLabel [FR_P (Name (Fresh_S n))]).

Definition freshRuleP (n:freshNameProto) : rule := (RuleProto [] emptyLabel [FR_P (Name (Fresh_P n))]).

(* This is the key reduction definition that tells us how a list of 
   protocol rules can be used to generate a trace *)

Inductive run : ruleList -> facts -> trace -> facts -> Prop :=
   | Run_Stop         : forall rl f1, run rl f1 [] f1
   | Run_Step         : forall rl f1 t f2 f3 l,  (reduceWithRules rl f1 l f2) 
                        -> (run rl f2 t f3) -> run rl f1 (l::t) f3
   | Run_Step_Silent  : forall rl f1 t f2 f3,  (reduceWithRules rl f1 emptyLabel f2) 
                        -> (run rl f2 t f3) -> run rl f1 t f3
   | Run_FreshStepP   : forall rl f1 t f2 f3 fn,  (reduceWithRule (freshRuleP fn) f1 emptyLabel f2) 
                        -> (run rl f2 t f3) -> run rl f1 t f3. (* <-- this seems like a hack, but I'm not sure of a better way ... *)

(* N.B. this does not enforce the conditions needed in Tamarin, e.g. fresh names do not repeat, these restrictions need to be added *)


(* This is the key reduction definition that tells us how a list of 
   protocol rules can be used to generate a trace using substitution*)

Inductive runSigma : ruleList -> substitutions -> facts -> trace -> facts -> Prop :=
   | SigmaRun_Stop         : forall rl  f1, runSigma rl [] f1 [] f1
   | SigmaRun_Step         : forall rl sigmaPrev f1 t f2 f3 l sigmaNow,  (reduceWithRulesSigma rl sigmaNow f1 l f2) 
                        -> (runSigma rl sigmaPrev f2 t f3) -> runSigma rl (sigmaNow::sigmaPrev) f1 (l::t) f3
   | SigmaRun_Step_Silent  : forall rl sigmaPrev f1 t f2 f3 sigmaNow,  (reduceWithRulesSigma rl sigmaNow f1 emptyLabel f2) 
                        -> (runSigma rl sigmaPrev f2 t f3) -> runSigma rl (sigmaNow::sigmaPrev) f1 t f3
   | SigmaRun_FreshStepP   : forall rl f1 t f2 f3 fn sigmaPrev sigmaNow,  (reduceWithRuleSigma (freshRuleP fn) sigmaNow f1 emptyLabel f2) 
                        -> (runSigma rl sigmaPrev f2 t f3) -> runSigma rl (sigmaNow::sigmaPrev) f1 t f3. (* <-- this seems like a hack, but I'm not sure of a better way ... *)

(** Some useful Lemmas about traces **)

Lemma reduceWithFirstRule : forall r rl f1 f2 l, reduceWithRule r f1 l f2 -> reduceWithRules (r::rl) f1 l f2.
Proof.
  intros. unfold reduceWithRules. inversion H. inversion H0. exists x0. split.
  - apply GinstHead. assumption.
  - assumption.
Qed.


Lemma reduceWithSecondRule : forall r1 r2 rl f1 f2 l, reduceWithRule r2 f1 l f2 -> reduceWithRules (r1::r2::rl) f1 l f2.
Proof.
  intros. unfold reduceWithRules. inversion H. inversion H0. exists x0. split.
  - apply GinstTail. apply GinstHead. assumption.
  - assumption.
Qed.

Lemma FreshRulePIsAGroundRule : forall fn, groundRule (freshRuleP fn).
Proof.
      intros.
      unfold groundRule. unfold freshRuleP. split.
        + reflexivity.
        + split.
          - unfold groundFacts. split.
            * reflexivity.
            * auto.
          - reflexivity.
Qed.
    
Lemma ProtoFreshNameStep (fn:freshNameProto) : 
           forall fs, reduceWithRule (freshRuleP fn) fs emptyLabel ((FR_P (Name (Fresh_P fn)))::fs).
Proof.
  unfold reduceWithRule.
  exists (freshRuleP fn).
  split. 
  + apply Ginst. split.
    - exists subs_empty. reflexivity.
    - apply FreshRulePIsAGroundRule.
  + unfold freshRuleP. apply R_match. simpl. auto.

Qed.


Lemma FreshRuleSIsAGroundRule : forall fn, groundRule (freshRuleS fn).
Proof.
      intros.
      unfold groundRule. unfold freshRuleS. split.
        + reflexivity.
        + split.
          - unfold groundFacts. split.
            * reflexivity.
            * auto.
          - reflexivity.
Qed.

 
Lemma SetupFreshNameStep (fn:freshNameSetup) : 
           forall fs, reduceWithRule (freshRuleP fn) fs emptyLabel ((FR_P (Name (Fresh_P fn)))::fs).
Proof.
  unfold reduceWithRule.
  exists (freshRuleP fn).
  split.
  + apply Ginst. split.
    - exists subs_empty. reflexivity.
    - apply FreshRulePIsAGroundRule.
  + unfold freshRuleP. apply R_match. simpl. auto. 
Qed.

Lemma ProtoFreshNameStepEmpty (fn:freshNameProto) : 
           reduceWithRule (freshRuleP fn) []  emptyLabel [ FR_P (Name (Fresh_P fn)) ].
Proof. apply ProtoFreshNameStep.  Qed.


Lemma SetupFreshNameStepEmpty (fn:freshNameSetup) : 
           reduceWithRule (freshRuleP fn) []  emptyLabel [ FR_P (Name (Fresh_P fn)) ].
Proof. apply SetupFreshNameStep.  Qed.

Lemma reduceRulesLessImpliesMore : forall r rl f1 l f2, reduceWithRules rl f1 l f2 -> reduceWithRules (r::rl) f1 l f2.
Proof.
  intros.
  inversion H. inversion H0. unfold reduceWithRules. exists x0. split.
   - apply GinstTail. assumption.
   - assumption.
Qed.

Lemma runRulesLessImpliesMore : forall r rl f1 t f2, run rl f1 t f2 -> run (r::rl) f1 t f2.
Proof.
  intros. induction H.
   - apply Run_Stop.
   - eapply Run_Step. apply reduceRulesLessImpliesMore. apply H. assumption.
   - eapply Run_Step_Silent. apply reduceRulesLessImpliesMore. apply H. assumption.
   - eapply Run_FreshStepP. apply H. assumption.
Qed.

Lemma runTransitive : forall rl s1 s2 s3 l1 l2,
     run rl s1 l1 s2 /\ run rl s2 l2 s3 -> run rl s1 (appendAny l1 l2) s3.
Proof.
  intros rl s1 s2 s3 l1 l2 H.
  destruct H.
  induction H ; simpl.
  + apply H0.
  + eapply Run_Step. apply H. auto.
  + eapply Run_Step_Silent. apply H. auto.
  + eapply Run_FreshStepP. apply H. auto.
Qed.



(** The same Lemmas with substitution**)
Lemma reduceWithFirstRuleSigma : forall r rl f1 f2 l sigma, reduceWithRuleSigma r sigma f1 l f2 
                      -> reduceWithRulesSigma (r::rl) sigma f1 l f2.
Proof.
  intros. unfold reduceWithRulesSigma. inversion H. inversion H0. exists x0. split.
  - apply GinstHeadSigma. assumption.
  - assumption.
Qed.


Lemma reduceWithSecondRuleSigma : forall r1 r2 rl f1 f2 l sigma, reduceWithRuleSigma r2 sigma f1 l f2 
                          -> reduceWithRulesSigma (r1::r2::rl) sigma f1 l f2.
Proof.
  intros. unfold reduceWithRulesSigma. inversion H. inversion H0. exists x0. split.
  - apply GinstTailSigma.  apply GinstHeadSigma.  assumption. 
  - assumption.
Qed.

Lemma ProtoFreshNameStepSigma (fn:freshNameProto) : 
           forall fs sigma, reduceWithRuleSigma (freshRuleP fn) sigma fs  emptyLabel ((FR_P (Name (Fresh_P fn)))::fs).
Proof.
  unfold reduceWithRuleSigma.
  exists (freshRuleP fn).
  split.
  + apply GinstSigma. split.
    - reflexivity.
    - apply FreshRulePIsAGroundRule.
  + unfold freshRuleP. apply R_match. simpl. auto. 
Qed.


Lemma SetupFreshNameStepSigma (fn:freshNameSetup) : 
           forall fs sigma, reduceWithRuleSigma (freshRuleP fn) sigma fs emptyLabel ((FR_P (Name (Fresh_P fn)))::fs).
Proof.
  unfold reduceWithRuleSigma.
  exists (freshRuleP fn).
  split.
  + apply GinstSigma. split.
    - reflexivity.
    - apply FreshRulePIsAGroundRule.
  + unfold freshRuleS. apply R_match. simpl. auto. 
Qed.

Lemma ProtoFreshNameStepEmptySigma (fn:freshNameProto) : 
           reduceWithRuleSigma (freshRuleP fn) subs_empty []  emptyLabel [ FR_P (Name (Fresh_P fn)) ].
Proof. apply ProtoFreshNameStepSigma.  Qed.


Lemma SetupFreshNameStepEmptySigma (fn:freshNameSetup) : 
           reduceWithRuleSigma (freshRuleP fn) subs_empty []  emptyLabel [ FR_P (Name (Fresh_P fn)) ].
Proof. apply SetupFreshNameStepSigma.  Qed.

Lemma reduceRulesLessImpliesMoreSigma : forall r rl f1 l f2 sigma, reduceWithRulesSigma rl sigma f1 l f2
           -> reduceWithRulesSigma (r::rl) sigma f1 l f2.
Proof.
  intros.
  inversion H. inversion H0. unfold reduceWithRulesSigma. exists x0. split.
   - apply GinstTailSigma. assumption.
   - assumption.
Qed.


 
Lemma runRulesLessImpliesMoreSigma : forall r rl f1 t f2 sigmas, runSigma rl sigmas f1 t f2 
                    -> runSigma (r::rl)  sigmas f1 t f2.
Proof.
  intros. induction H. 
   - apply SigmaRun_Stop.
   - eapply SigmaRun_Step. apply reduceRulesLessImpliesMoreSigma. apply H. assumption.
   - eapply SigmaRun_Step_Silent. apply reduceRulesLessImpliesMoreSigma. apply H. assumption.
   - eapply SigmaRun_FreshStepP. apply H. assumption.
Qed.




Lemma runTransitiveSigma : forall rl f1 f2 f3 l1 l2 sigmas1 sigmas2,
     runSigma rl sigmas1 f1 l1 f2 /\ runSigma rl sigmas2 f2 l2 f3 -> runSigma rl (appendAny sigmas1 sigmas2) f1 (appendAny l1 l2) f3.
Proof.
  intros rl s1 s2 s3 l1 l2 sigmas1 sigmas2 H.
  destruct H. 
  induction H ; simpl.
  + apply H0.
  + eapply SigmaRun_Step. apply H. apply IHrunSigma. auto.
  + eapply SigmaRun_Step_Silent. apply H. auto.
  + eapply SigmaRun_FreshStepP. apply H. auto.
Qed.


(** ===================== 
  *** 7: Example  
 ===================== **)
(* This section shows how we can generate a trace for an example 
   Tamarin protocol, taken from https://github.com/tamarin-prover/manual/blob/master/code/NSLPK3.spthy *)

(* First we define that rules that model an attacker: *)
Definition varX : term := Bterm (Var "x") .
Definition varY : term := Bterm (Var "Y") .
Definition AttackerReceive (ts:terms) : rule := RuleProto [ OUT ts ] emptyLabel [ K ts ].
Definition AttackerReceive1 : rule := RuleProto [ OUT [varX] ] emptyLabel [ K [varX] ].
Definition AttackerReceive2 : rule := RuleProto [ OUT [varX;varY] ] emptyLabel [ K [varX]; K [varY] ].
Definition AttackerSend (ts:terms) : rule := RuleProto [ K ts ] emptyLabel [ IN ts ].
Definition AttackerSend1 : rule := RuleProto [ K [varX] ] emptyLabel [ K [varX] ].
Definition AttackerSend2 : rule := RuleProto [ K [varX]; K [varY] ] emptyLabel [ IN [varX; varY] ].
Definition LtkFact : name := Pub "LtkFact".
Definition ltkA_var : baseTerm := (Var  "ltkA").
Definition ltkB_var : baseTerm := (Var  "ltkB").
(* 
Definition ltkA_var : freshNameSetup := "ltkA".
Definition ltkB_var : freshNameSetup := "ltkB".
 *)
Definition PkFact : name := Pub "PkFact".
Definition PkName : string := "Pkname".
Definition Pk : string := "Pkname".
Definition A : term := Bterm (Name (Pub "A")).
Definition B : term := Bterm (Name (Pub "B")).
Definition C : term := Bterm (Name (Pub "C")).

(* The first protocol setup rule is:
rule Register_pk:
  [ Fr(~ltkA) ]
  -->
  [ !Ltk($A, ~ltkA), !Pk($A, pk(~ltkA)), Out(pk(~ltkA)) ]
*)

(* $A means any constant, we model this here by making multiple copies of the rule.
   As our key theorem will be of the form, forall rule list ..., this is valid *)


Definition registerPKruleA : rule := RuleSetup [ FR_P ltkA_var ] emptyLabel 
                                [STATE LtkFact [A;   (Bterm ltkA_var)]; STATE PkFact [A; Func PkName [ltkA_var]];
                                       OUT [Func PkName [ltkA_var]] ].


Definition registerPKruleB : rule := RuleSetup [ FR_P ltkB_var ] emptyLabel 
                                [STATE LtkFact [B;  (Bterm ltkB_var)]; STATE PkFact [B; Func PkName [ltkB_var]]; 
                                          OUT [Func PkName [ltkB_var]] ].
 

(* The rule for the first step of the protocol models the sending of the first message:
rule I_1:
  let m1 = aenc{'1', ~ni, $I}pkR
  in
    [ Fr(~ni), !Pk($R, pkR) ]
  --[ OUT_I_1(m1)]->
    [ Out( m1 ), St_I_1($I, $R, ~ni)]

*)
Definition St_I_1 : name := Pub "St_I_1".

Definition ni : baseTerm := (Var  "ni"). 

(* Definition ni : freshNameProto := "ni". *)

Definition m1 : term :=  Func "aenc" [ ni; (Name (Pub "A"))].

Definition I_1_A_to_B : rule := RuleProto  [(FR_P  ni); STATE PkFact [B; Func PkName [ltkB_var]]]  
                                      (BasicLabel [ ActLabel (Pub "Out") [m1] ])
                                      [OUT [m1]; STATE St_I_1 [A; B; (Bterm ni)]; STATE PkFact [B; Func PkName [ltkB_var]]].

(* This rule only let's "A" send the first message. We would need more rules to model others starting the protocol *)

(* The whole protoocl is modelled by all of the rules:*)
Definition ProtocolRules : ruleList := [registerPKruleA; registerPKruleB; I_1_A_to_B].


(* The first step of the protocol is to generate a fresh name for A *)
Lemma protocolRun1Step : run ProtocolRules [] [] [FR_P (Name (Fresh_P "ltkA")) ].
Proof.
  apply Run_FreshStepP with (fn:="ltkA") (f2:= [FR_P (Name (Fresh_P "ltkA")) ]).
  + apply (SetupFreshNameStep "ltkA").
  + apply Run_Stop.
Qed.

(* The second step of the protocol is to generate a fresh name for B *)
Lemma protocolRun2Step : run ProtocolRules [] [] 
              [FR_P (Name (Fresh_P "ltkB")); FR_P (Name (Fresh_P "ltkA"))].
Proof.
  apply Run_FreshStepP  with (fn:="ltkA") (f2:= [FR_P (Name (Fresh_P "ltkA")) ]).
  + apply (SetupFreshNameStep "ltkA").
  +   apply Run_FreshStepP  with (fn:="ltkB") (f2:= [FR_P (Name (Fresh_P "ltkB")); FR_P (Name (Fresh_P "ltkA"))]).
    - apply (SetupFreshNameStep "ltkB") with (fs:=[FR_P (Name (Fresh_P "ltkA")) ]).
    - apply Run_Stop.
Qed.

(* The third step of the protocol, sets up A's keys using the registerPKruleA rule*)
(* For this we need a substitution that maps the variable "ltkA" to a name:*)

Definition mapLtkAvarToName := "ltkA" !-> Fresh_P "ltkA"; subs_empty.

(* This is the ground version of the rule we will use: *) 
Definition registerPKruleAground : rule := RuleSetup [ FR_P (Name (Fresh_P "ltkA")) ] 
                                emptyLabel 
                                [STATE LtkFact [A; Bterm (Name (Fresh_P "ltkA"))]; 
                                 STATE PkFact [A; Func PkName [(Name (Fresh_P "ltkA"))]]; 
                                 OUT [Func PkName [(Name (Fresh_P "ltkA"))]] ].

Lemma protocolRun2to3Step : run ProtocolRules
              [FR_P (Name (Fresh_P "ltkB")); FR_P (Name (Fresh_P "ltkA"))]
              []
              [STATE LtkFact [A; (Bterm (Name (Fresh_P "ltkA")))]; 
               STATE PkFact [A; Func PkName [(Name (Fresh_P "ltkA"))]]; 
               OUT [Func PkName [(Name (Fresh_P "ltkA"))]];
               FR_P (Name (Fresh_P "ltkB"))].
Proof.
  eapply Run_Step_Silent.
   + unfold ProtocolRules. unfold reduceWithRules. exists registerPKruleAground. split. 
     - apply GinstHead. apply Ginst. split. 
       * exists mapLtkAvarToName. reflexivity.
       * unfold groundRule. unfold registerPKruleAground. split. 
        unfold groundFacts. split. reflexivity. reflexivity. split. unfold groundFacts. split. 
        unfold groundFact. unfold groundTerms. split. reflexivity. split. reflexivity. 
        reflexivity. split. unfold groundFact. unfold groundTerms. split. reflexivity. split.
        unfold groundTerm. unfold groundBaseTerms. split. reflexivity. reflexivity. reflexivity.
        unfold groundFact. unfold groundTerms. split. split.  unfold groundTerm. 
        unfold groundBaseTerms. split. reflexivity. reflexivity. reflexivity. reflexivity. reflexivity.
     - apply R_match. simpl. auto. 
   + apply Run_Stop. 
Qed.


Lemma protocolRunToStop3: run ProtocolRules [] []
              [STATE LtkFact [A; (Bterm (Name (Fresh_P "ltkA")))]; 
               STATE PkFact [A; Func PkName [(Name (Fresh_P "ltkA"))]]; 
               OUT [Func PkName [(Name (Fresh_P "ltkA"))]];
               FR_P (Name (Fresh_P "ltkB"))].
Proof.
  eapply runTransitive with (l1:=[]) (l2:=[]). split. apply protocolRun2Step.
  apply protocolRun2to3Step.
Qed.
  

(*To be continued ... *)

(** ===================== 
  *** 8: Definitions from Chapter 5 of the thesis
 ===================== **)

(* Before defining standard traces we define a relation for running rules in a fixed order
   and a function give us just the logs from a trace *)

(* 'runInOrder as sr f1 t f2' verifies that given a allowed sequences as and set
   up rules sr, facts f1 and trace t, whether it is possible to generate facts f2 
   or not by executing the rules from as in order and any rules from sr? 
 *)

Inductive runInOrder : ruleList -> ruleList -> substitution -> facts -> trace -> facts -> Prop :=
     | Run_Stop_O      : forall f1 rls sigma, runInOrder [] rls sigma f1 [] f1
     | Run_Step_O      : forall r rls rlp sigma f1 t f2 f3 l, (reduceWithGroundRule (applySubRule sigma r) f1 l f2) 
                          -> (runInOrder rlp rls sigma f2 t f3) -> runInOrder  (r::rlp) rls sigma f1 (l::t) f3
     | Run_Step_Silent_O : forall r rls rlp sigma f1 t f2 f3, (reduceWithGroundRule (applySubRule sigma r) f1 emptyLabel f2) 
                          -> (runInOrder rlp rls sigma f2 t f3) -> runInOrder (r::rlp) rls sigma f1 t f3
     | Run_FreshStep_O : forall rls rlp sigma f1 t f2 f3 fn, (reduceWithRule (freshRuleP fn) f1 emptyLabel f2) 
                         -> (runInOrder rlp rls sigma f2 t f3) -> runInOrder rlp rls sigma f1 t f3
     | Run_Step_S      : forall  rls rlp sigma f1 l f2 f3 t, (reduceWithRules rls f1 l f2)
                         -> (runInOrder rlp rls sigma f2 t f3) -> runInOrder  rlp rls sigma f1 (l::t) f3
     | Run_Step_Silent_S : forall rls rlp sigma f1 t f2 f3, (reduceWithRules rls f1  emptyLabel f2)
                         -> (runInOrder rlp rls sigma f2 t f3) -> runInOrder rlp rls sigma f1 t f3
     | Run_FreshStep_S : forall rls rlp sigma f1 t f2 f3 fn, (reduceWithRule (freshRuleS fn) f1 emptyLabel f2) 
                         -> (runInOrder rlp rls sigma f2 t f3) -> runInOrder rlp rls sigma f1 t f3
     | Run_Comm_O      : forall rls rlp sigma f1 t f2 trm, (subList [OUT trm] f1) ->
                            runInOrder rlp rls sigma ((IN trm)::(removeFacts [OUT trm] f1)) t f2 ->
                               runInOrder rlp rls sigma f1 t f2.

 

(* 'runInOrderSigmaProtocol as subs f1 t f2' verifies that given a allowed sequences as,
   facts f1 and trace t, whether it is possible to generate facts f2 
   or not by executing the rules from as in order? 
 *) 


Inductive runInOrderSigmaProtocol : ruleList -> substitutions -> facts -> trace -> facts -> Prop :=
     | Sigma_Run_Stop_P      : forall f1 sigma, runInOrderSigmaProtocol [] sigma f1 [] f1

     | Sigma_Run_Step_P      : forall r rlp sigmaNow sigmaPrev f1 t f2 f3 l,
                                  groundRule (applySubRule sigmaNow r) 
                                    -> reduceWithGroundRule (applySubRule sigmaNow r) f1 l f2
                                      -> (runInOrderSigmaProtocol rlp sigmaPrev f2 t f3) 
                                        -> runInOrderSigmaProtocol (r::rlp) (sigmaNow::sigmaPrev) f1 (l::t) f3

     | Sigma_Run_Step_Silent_P : forall r rlp sigmaNow sigmaPrev f1 t f2 f3, 
                                    groundRule (applySubRule sigmaNow r) 
                                      -> reduceWithGroundRule (applySubRule sigmaNow r) f1 emptyLabel f2
                                        -> (runInOrderSigmaProtocol rlp sigmaPrev f2 t f3) 
                                          -> runInOrderSigmaProtocol (r::rlp) (sigmaNow::sigmaPrev)f1 t f3

     | Sigma_Run_Comm_P      : forall rlp sigmaPrev f1 t f2 trm, (subList [OUT trm] f1) ->
                            runInOrderSigmaProtocol rlp  sigmaPrev ((IN trm)::(removeFacts [OUT trm] f1)) t f2 ->
                               runInOrderSigmaProtocol rlp sigmaPrev f1 t f2.



(* runInOrderSigma executes multiple iterations of setup rules in any order followed by protocol rule execution once
in the order mandated by any of the allowed sequences .
Before passing the tist of facts (fsMid), produced by the setup rule list execution, to  runInOrderSigmaProtocol, 
all the OUT and IN facts are removed from fsMid *)

Fixpoint runInOrderSigma (rlProto:ruleList) (rlSetup:ruleList) (sigmaAll:substitutions) (fsInitial:facts) (tr:trace) (fsFinal:facts) : Prop :=
forall fsMid trSetup trProto, 
  run rlSetup  fsInitial trSetup fsMid 
  /\   runInOrderSigmaProtocol rlProto sigmaAll (removeOutInfromFactList fsMid) tr fsFinal
        /\ (eq_trace tr (appendAny trSetup trProto)).



Lemma noOutputsMeansNoOutputs: forall factslist trm, noOutputs factslist -> member (OUT trm) factslist -> False.
Proof.
 intros;
 induction factslist.
+ inversion H0.
+ inversion H0.
  - rewrite <- H1 in H. inversion H.
  - apply IHfactslist; auto. destruct a; auto. inversion H.
Qed. 

(* Unused *)
Lemma singleOutputEquals : forall trm1 trm2 factsList,
  (member (OUT trm1) factsList) ->  (member (OUT trm2) factsList) 
       ->  oneOutput factsList -> trm1 = trm2.
Proof.
  intros. induction factsList.
  - inversion H1.
  - destruct a. 
    + inversion H. inversion H2. inversion H0. inversion H3. apply IHfactsList; assumption.
    + destruct ( terms_dec trm1 t);  destruct ( terms_dec trm2 t).
      * rewrite e. rewrite e0. reflexivity.
      * inversion H0. inversion H2. unfold not in n0. apply n0 in H4. inversion H4.
        unfold oneOutput in H1. apply noOutputsMeansNoOutputs with (trm:=trm2) in H1. inversion H1. apply H2.
      * inversion H. inversion H2. unfold not in n0. apply n0 in H4. inversion H4.
        unfold oneOutput in H1. apply noOutputsMeansNoOutputs with (trm:=trm1) in H1. inversion H1. apply H2.
      * inversion H. inversion H2. unfold not in n0. apply n0 in H4. inversion H4.
        unfold oneOutput in H1. apply noOutputsMeansNoOutputs with (trm:=trm1) in H1. inversion H1. apply H2.
     + inversion H. inversion H2. inversion H0. inversion H3. apply IHfactsList; assumption.
     + inversion H. inversion H2. inversion H0. inversion H3. apply IHfactsList; assumption.
     + inversion H. inversion H2. inversion H0. inversion H3. apply IHfactsList; assumption.
Qed.



(* TOM: This is my work space for props I need from Prop 1. 
        We will need to put these all in the right place later.
        We could do with a very clear, more detailed table of contents
        and a clearer structure for this file *)


Lemma memberOneOrOther : forall {T:Type} (e:T) (l1:list T) (l2:list T),
  member e (appendAny l1 l2)  -> not (member e l2) -> (member e l1).
Proof.
  intros. induction l1.
  + simpl in H. unfold not in H0. apply H0 in H. inversion H.
  + simpl.  simpl in H. inversion H. left. apply H1.
    right. apply IHl1. assumption.
Qed.



 
Lemma memberAfterRemoveOne: forall fac1 fac2 facs,
  member fac1 (removeFact fac2 facs) ->  member fac1 facs.
Proof.
  intros. induction facs.
  + inversion H. 
  + simpl. unfold removeFact in H. simpl in H. destruct ( fact_dec a fac2) in H.  
    - right. assumption.
    - simpl in H. inversion H.
     * left. assumption.
     * right. apply IHfacs. unfold removeFact. apply H0.
Qed.


Lemma memberAfterRemove : forall fac facts1 facts2, member fac (removeFacts facts1 facts2) -> member fac facts2.
Proof.
  intros. induction facts1.
  + simpl in H. assumption.
  + apply IHfacts1.  simpl in H.  
    apply memberAfterRemoveOne in H.
    assumption.
Qed.


Lemma memberSigmaEquals : forall (fac:fact) (sigma:substitution) (factlist:list fact),
  member fac (applySubFacts sigma factlist) 
    -> exists (facTemplate:fact),  fac = applySubFact sigma facTemplate 
                                         /\ member facTemplate factlist.
Proof.
  intros. induction factlist. inversion H. destruct (fact_dec fac (applySubFact sigma a)).
  - exists a. split. assumption. simpl. left. reflexivity.
  - simpl in H. inversion H. apply n0 in H0. inversion H0.
    apply IHfactlist in H0. inversion H0. exists x0. inversion H1. split;auto. 
    +  unfold member. right. apply H3.
Qed.


(* Unused *)
Lemma factFromReduction : forall sigma redRule f1 f2 l fac, 
   reduceWithRuleSigma redRule sigma f1 l f2
     -> member fac f2 -> not (member fac f1)
       -> exists facTemplate, (  member facTemplate (conclFacts redRule) 
             /\ applySubFact sigma facTemplate = fac).
Proof.
  intros. inversion H. inversion H2. inversion H4. subst. apply memberOneOrOther in H0.

  inversion H2. inversion H6. subst. inversion H8. rewrite <- H9 in H0. destruct redRule.
  simpl. simpl in H0.
  + destruct f0. 
    - inversion H0.
    - apply memberSigmaEquals in H0. inversion H0. exists x1.
      inversion H11. split. assumption. rewrite H12. reflexivity.
  + destruct f0. 
    - inversion H0.
    - apply memberSigmaEquals in H0. inversion H0. exists x1.
      inversion H11. split. assumption. rewrite H12. reflexivity.
  +   unfold not. intros. apply H1. eapply memberAfterRemove. apply H6.
Qed.

(** Rajiv : Added these lemmas *)
(* Unused *)
Lemma noOutputsMeansNoOutputsInFactOrFacts: forall f fs t1, 
          noOutputs (f::fs) -> not (eq_fact (OUT t1) f) /\ noOutputs fs.
Proof.
 intros. 
  + split.
    - unfold not. intros. destruct f; auto.
    - destruct f; auto. inversion H.
Qed.

(* Unused *)
Lemma emptyRuleCantMakeOutput : forall  sigma f1 label f2 , 
         reduceWithRuleSigma (RuleProto [] label []) sigma f1 label f2
               -> noOutputs f1 -> noOutputs f2.
Proof. 
   intros.
   inversion H. inversion H1. inversion H2. inversion H4.
   simpl in H8.  rewrite <- H8 in H3. inversion H3.
   simpl in H14. rewrite <- H14. assumption.
Qed.



(* Lemmas that show a single only adds or removes 0 or 1 inputs and outputs *)

Lemma sigmaNoInputFacts: forall f1 f2 sigma,
 applySubFacts sigma f1 = f2 -> noInputs f2 -> noInputs f1.
Proof.
  intros. generalize dependent f2. induction f1; intros.
  - reflexivity.
  - destruct a; simpl in H; simpl.
    + rewrite <- H in H0. simpl in H0. inversion H0.
    + destruct f2; inversion H. eapply IHf1. apply H3. rewrite <- H2 in H0. auto.
    + destruct f2; inversion H. eapply IHf1. apply H3. rewrite <- H2 in H0. auto.
    + destruct f2; inversion H. eapply IHf1. apply H3. rewrite <- H2 in H0. auto.
    + destruct f2; inversion H. eapply IHf1. apply H3. rewrite <- H2 in H0. auto.
Qed.

Lemma sigmaNoInputFacts2: forall f1 f2 sigma,
 applySubFacts sigma f1 = f2 -> noInputs f1 -> noInputs f2.
Proof.
  intros. generalize dependent f2. induction f1; intros.
  - inversion H. reflexivity.
  - destruct a; intros; simpl in H; simpl; simpl in H0.
    + inversion H0.
    + destruct f2; inversion H. simpl. apply IHf1. apply H0. reflexivity.
    + destruct f2; inversion H. simpl. apply IHf1. apply H0. reflexivity.  
    + destruct f2; inversion H. simpl. apply IHf1. apply H0. reflexivity.
    + destruct f2; inversion H. simpl. apply IHf1. apply H0. reflexivity.
Qed.



Lemma sigmaNoOutputFacts: forall f1 f2 sigma,
 applySubFacts sigma f1 = f2 -> noOutputs f1 -> noOutputs f2.

Proof.
 intros. generalize dependent f2. induction f1; intros.
  - simpl in H. inversion H. auto.
  - destruct a; simpl; simpl in H; simpl in H0; destruct f2; inversion H; simpl.
    + eapply IHf1. apply H0. reflexivity.
    + auto.
    + eapply IHf1. apply H0. reflexivity.
    + eapply IHf1. apply H0. reflexivity.
    + eapply IHf1. apply H0. reflexivity.
Qed.

Lemma sigmaNoOutputFacts2: forall f1 f2 sigma,
 applySubFacts sigma f1 = f2 -> noOutputs f2 -> noOutputs f1.
Proof.
  induction f1; intros.
  - reflexivity. 
  - destruct a; destruct f2; simpl; simpl in H; try inversion H; try rewrite <- H2 in H0;
     try  simpl in H0; try eapply IHf1; try apply H3; try assumption.
Qed.



Lemma sigmaNoInputOrOutputFacts: forall f1 f2 sigma,
 applySubFacts sigma f1 = f2 -> noInputOrOutput f1 -> noInputOrOutput f2.

Proof.
 intros. generalize dependent f2. induction f1; intros.
  - simpl in H. inversion H. auto.
  - destruct a; simpl; simpl in H; simpl in H0; destruct f2; inversion H; simpl.
    + auto.
    + auto. 
    + eapply IHf1. apply H0. reflexivity.
    + eapply IHf1. apply H0. reflexivity.
    + eapply IHf1. apply H0. reflexivity.
Qed.



Lemma sigmaOneInputXorOutputFacts: forall f1 f2 sigma,
 applySubFacts sigma f1 = f2 -> oneInputXorOutput f1 -> oneInputXorOutput f2.

Proof.
  intros. generalize dependent f2. induction f1; intros.
  - simpl in H. inversion H. auto.
  - destruct a; destruct f2; simpl; simpl in H; try inversion H; try rewrite <- H2 in H0;
     try  simpl in H0; try eapply IHf1; try apply H3; try assumption.
    + split. rewrite H3. apply sigmaNoInputFacts2 in H3. auto. inversion H0. auto.
      eapply sigmaNoOutputFacts. reflexivity. inversion H0. apply H4.
    + split. rewrite H3. apply sigmaNoInputFacts2 in H3. auto. inversion H0. auto.
      eapply sigmaNoOutputFacts. reflexivity. inversion H0. apply H4.
    + auto.
    + auto.
    + auto.
Qed.


(*
Lemma sigmaoneOutputXorInputIsFacts: forall f1 f2 sigma trms,
 applySubFacts sigma f1 = f2  
              -> oneOutputXorInputIs f1 trms -> oneOutputXorInputIs f2 trms.
Proof.
  intros. generalize dependent f2. induction f1; intros.
  - inversion H0.
  - destruct trms. destruct a.
      + split. rewrite H3. apply sigmaNoInputFacts2 in H3. auto. inversion H0. auto.
        eapply sigmaNoOutputFacts. reflexivity. inversion H0. apply H4.
        
+ simpl in H0. apply IHf1. simpl in H.

a; destruct f2; simpl; simpl in H; try inversion H; try rewrite <- H2 in H0;
     try  simpl in H0; try eapply IHf1; try apply H3; try assumption.
    + rewrite H2. apply sigmaNoInputFacts2 in H3. auto. inversion H0. auto.
      eapply sigmaNoOutputFacts. reflexivity. inversion H0. apply H4.
    + split. rewrite H3. apply sigmaNoInputFacts2 in H3. auto. inversion H0. auto.
      eapply sigmaNoOutputFacts. reflexivity. inversion H0. apply H4.
    + auto.
    + auto.
    + auto.


  intros. induction f2. induction f1; intros.
  - inversion H0.
  - destruct a; inversion H.
  - destruct a. 3:{
      + simpl. eapply IHf2. simpl in H.<- H. ion H0. eapply sigmaNoInputFacts2. apply H3.  auto. 
        eapply sigmaNoOutputFacts. apply H3. inversion H0.  auto.
      + split. simpl in H0. inversion H0. eapply sigmaNoInputFacts2. apply H3.  auto. 
        eapply sigmaNoOutputFacts. apply H3. inversion H0.  auto.
      + eapply IHf1. apply H0. apply H3.
      + eapply IHf1. apply H0. apply H3.
      + eapply IHf1. apply H0. apply H3.
Qed.
 *)

Axiom sigmaoneOutputXorInputIsFacts: forall f1 f2 sigma trms,
 applySubFacts sigma f1 = f2  
              -> oneOutputXorInputIs f1 trms -> oneOutputXorInputIs f2 trms.

(* Unused *)

Lemma sigmaOneInputFact: forall f1 f2 sigma,
 applySubFacts sigma f1 = f2 -> oneInput f2 -> oneInput f1. 

Proof.
  intros. generalize dependent f2. induction f1; intros.
  - simpl in H. rewrite <- H in H0. auto.
  - destruct f2.
    * inversion H0.
    * inversion H. destruct a ; simpl. 
      + eapply sigmaNoInputFacts. apply H3. subst. simpl in H0. assumption.
      + eapply IHf1. apply H3. subst. simpl in H0. assumption.
      + eapply IHf1. apply H3. subst. simpl in H0. assumption.
      + eapply IHf1. apply H3. subst. simpl in H0. assumption.
      + eapply IHf1. apply H3. subst. simpl in H0. assumption.
Qed.


Lemma  sigmaOneInputFact2: forall f1 f2 sigma,
 applySubFacts sigma f1 = f2 -> oneInput f1 -> oneInput f2. 

Proof.
  intros. generalize dependent f2. induction f1; intros.
  - inversion H0.
  - destruct a.
    + destruct f2; inversion H. simpl. rewrite H3. simpl in H0. eapply sigmaNoInputFacts2. apply H3. apply H0.
    + simpl in H0. subst. simpl. apply IHf1.  apply H0. reflexivity.
    + simpl in H0. subst. simpl. apply IHf1.  apply H0. reflexivity.
    + simpl in H0. subst. simpl. apply IHf1.  apply H0. reflexivity.
    + simpl in H0. subst. simpl. apply IHf1.  apply H0. reflexivity.
Qed. 

Lemma sigmaOneOutputFact: forall f1 f2 sigma,
 applySubFacts sigma f1 = f2 -> oneOutput f1 -> oneOutput f2.
Proof.
 intros. generalize dependent f2. induction f1; intros.
  - inversion H0.
  - destruct a; simpl; simpl in H; simpl in H0; destruct f2; inversion H; simpl.
    + eapply IHf1. apply H0. reflexivity.
    + rewrite H3. apply sigmaNoOutputFacts in H3; assumption.
    + eapply IHf1. apply H0. reflexivity.
    + eapply IHf1. apply H0. reflexivity.
    + eapply IHf1. apply H0. reflexivity.
Qed.


Axiom  sigmaoneInputXorOutputFact: forall f1 f2 sigma,
 applySubFacts sigma f1 = f2 -> oneInputXorOutput f1 -> oneInputXorOutput f2.



Lemma sigmaMoreThanOneOutputFact: forall f1 f2 sigma,
 applySubFacts sigma f1 = f2 -> moreThanOneOutput f1 -> moreThanOneOutput f2.
Proof.
 intros. generalize dependent f2. induction f1; intros.
  - inversion H0.
  - destruct a; simpl; simpl in H; simpl in H0; destruct f2; inversion H; simpl.
    + eapply IHf1. apply H0. reflexivity.
    + rewrite H3. apply sigmaOneOutputFact in H3; assumption.
    + eapply IHf1. apply H0. reflexivity.
    + eapply IHf1. apply H0. reflexivity.
    + eapply IHf1. apply H0. reflexivity.
Qed.


(* Unused *)
Lemma ginstWithSigmaNoInputP: forall f1 f2 f3 f4 l1 l2 sigma,
  ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
   -> noInputs f3 -> noInputs f1.
Proof.
  intros. inversion H. subst. inversion H1. simpl in H2.
  inversion H2. rewrite H5. eapply sigmaNoInputFacts2. apply H5. assumption.
Qed.

(* Unused *)
Lemma ginstWithSigmaOneInputP: forall f1 f2 f3 f4 l1 l2 sigma,
  ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
   -> oneInput f3 -> oneInput f1.
Proof.
  intros. inversion H. subst. inversion H1. simpl in H2.
  inversion H2. rewrite H5. eapply sigmaOneInputFact2. apply H5. assumption.
Qed.

(* Unused *)
Lemma ginstWithSigmaNoOutputC: forall f1 f2 f3 f4 l1 l2 sigma,
  ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
   -> noOutputs f4 -> noOutputs f2.
Proof.
  intros. inversion H. subst. inversion H1. simpl in H2.
  inversion H2. rewrite H7. apply sigmaNoOutputFacts in H7; assumption.
Qed.

Lemma ginstWithSigmaNoOutputP: forall f1 f2 f3 f4 l1 l2 sigma,
  ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
   -> noOutputs f3 -> noOutputs f1.
Proof. 
  intros. inversion H. subst. inversion H1. simpl in H2.
  inversion H2. rewrite H5.  apply sigmaNoOutputFacts in H5 ; assumption.
Qed.

Lemma ginstWithSigmaOneOutputC: forall f1 f2 f3 f4 l1 l2 sigma,
  ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
   -> oneOutput f4 -> oneOutput f2.
Proof.
  intros. inversion H. subst. inversion H1. simpl in H2.
  inversion H2. rewrite H7. apply sigmaOneOutputFact in H7; assumption.
Qed.



Lemma ginstWithSigmaMoreThanOneOutputC: forall f1 f2 f3 f4 l1 l2 sigma,
  ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
   -> moreThanOneOutput f4 -> moreThanOneOutput f2.
Proof.
  intros. inversion H. subst. inversion H1. simpl in H2.
  inversion H2. rewrite H7. apply sigmaMoreThanOneOutputFact in H7; assumption.
Qed.


Lemma ginstWithSigmaNoInputOutputC: forall f1 f2 f3 f4 l1 l2 sigma,
  ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
   -> noInputOrOutput f4 -> noInputOrOutput f2.
Proof. 
  intros. inversion H. subst. inversion H1. simpl in H2.
  inversion H2. rewrite H7. apply sigmaNoInputOrOutputFacts in H7; assumption.
Qed.


(* Unused *) 
Lemma ginstWithSigmaNoInputOutputP: forall f1 f2 f3 f4 l1 l2 sigma,
  ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
   -> noInputOrOutput f3 -> noInputOrOutput f1.
Proof. 
  intros. inversion H. subst. inversion H1. simpl in H2.
  inversion H2. rewrite H5. apply sigmaNoInputOrOutputFacts in H5; assumption.
Qed.


Lemma ginstWithSigmaOneInputXorOutputC: forall f1 f2 f3 f4 l1 l2 sigma,
  ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
   -> oneInputXorOutput f4 -> oneInputXorOutput f2.
Proof. 
  intros. inversion H. subst. inversion H1. simpl in H2.
  inversion H2. rewrite H7. apply sigmaOneInputXorOutputFacts in H7; assumption.
Qed.

(* Unused *) 
Lemma ginstWithSigmaOneInputXorOutputP: forall f1 f2 f3 f4 l1 l2 sigma,
  ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
   -> oneInputXorOutput f3 -> oneInputXorOutput f1.
Proof. 
  intros. inversion H. subst. inversion H1. simpl in H2.
  inversion H2. rewrite H5. apply sigmaOneInputXorOutputFacts in H5; assumption.
Qed.

Lemma ginstWithSigmaoneOutputXorInputIsC : forall f1 f2 f3 f4 l1 l2 sigma trms,
  ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
   -> oneOutputXorInputIs f4 trms -> oneOutputXorInputIs f2 trms.
Proof. 
  intros. inversion H. subst. inversion H1. simpl in H2.
  inversion H2. rewrite H7. eapply sigmaoneOutputXorInputIsFacts in H7. apply H7. apply H0. 
Qed.


Lemma ginstWithSigmaoneOutputXorInputIsP : forall f1 f2 f3 f4 l1 l2 sigma trms,
  ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
   -> oneOutputXorInputIs f3 trms -> oneOutputXorInputIs f1 trms.
Proof. 
  intros. inversion H. subst. inversion H1. simpl in H2.
  inversion H2. rewrite H5. eapply sigmaoneOutputXorInputIsFacts in H5. apply H5. apply H0. 
Qed.


Lemma noOutputsTail : forall f fs,
  noOutputs (f::fs) -> noOutputs fs.
Proof.
  intros.  destruct f; try simpl in H; try assumption. inversion H.
Qed.


Lemma noInputsTail : forall f fs,
  noInputs (f::fs) -> noInputs fs.
Proof.
  intros.  destruct f; try simpl in H; try assumption. inversion H.
Qed.


Lemma noInputOrOutputTail : forall f fs,
  noInputOrOutput (f::fs) -> noInputOrOutput fs.
Proof.
  intros.  destruct f; try simpl in H; try assumption.
    + inversion H.
    + inversion H.
Qed.


Lemma noOutputsAcrossRemoveFact : forall f fs,
  noOutputs fs -> noOutputs (removeFact f fs).
Proof.
  intros. induction fs.
  + reflexivity.
  + unfold removeFact. simpl. destruct ( fact_dec a f).
    - apply  noOutputsTail in H. assumption.
    - destruct a; simpl; try apply IHfs; try eapply noOutputsTail; apply H.
Qed.


Lemma noOutputsAcrossRemove : forall f1 f2,
  noOutputs f2 -> noOutputs (removeFacts f1 f2).
Proof.
  intros. induction f1.
    + simpl. assumption.
    + simpl. apply noOutputsAcrossRemoveFact.  assumption.
Qed. 


Axiom oneOutputsAcrossRemove : forall f1 f2,
  oneOutput f2 -> noOutputs f1 -> oneOutput (removeFacts f1 f2).


Axiom oneInputXorOutputAcrossRemove : forall f1 f2,
  oneInputXorOutput f2 -> noInputOrOutput f1 -> oneInputXorOutput (removeFacts f1 f2).


Lemma noInputsAcrossRemoveFact : forall f fs,
  noInputs fs -> noInputs (removeFact f fs).
Proof.
  intros. induction fs.
  + reflexivity.
  + unfold removeFact. simpl. destruct ( fact_dec a f).
    - apply  noInputsTail in H. assumption.
    - destruct a; simpl; try apply IHfs; try eapply noInputsTail; apply H.
Qed. 


Lemma noInputOrOutputAcrossRemoveFact : forall f fs,
  noInputOrOutput fs -> noInputOrOutput (removeFact f fs).
Proof.
  intros. induction fs.
  + reflexivity.
  + unfold removeFact. simpl. destruct ( fact_dec a f).
    - apply  noInputOrOutputTail in H. assumption.
    - destruct a; simpl; try apply IHfs; try eapply noInputOrOutputTail; apply H.
Qed. 


Lemma noInputsAcrossRemove : forall f1 f2,
  noInputs f2 -> noInputs (removeFacts f1 f2).
Proof.
  intros. induction f1.
    + simpl. assumption.
    + simpl. apply noInputsAcrossRemoveFact.  assumption.
Qed.


Lemma noInputOrOutputAcrossRemove : forall f1 f2,
  noInputOrOutput f2 -> noInputOrOutput (removeFacts f1 f2).
Proof.
  intros. induction f1.
    + simpl. assumption.
    + simpl. apply noInputOrOutputAcrossRemoveFact.  assumption.
Qed. 


Lemma AppendNoOutputs : forall f1 f2,
  noOutputs f1 -> noOutputs f2 -> noOutputs (appendAny f1 f2).
Proof.
  intros. induction f1. induction f2.
    + reflexivity.
    + simpl appendAny. apply H0.
    + induction a.
      - simpl. apply IHf1. simpl in H. auto.
      - simpl. simpl in H. auto.
      - simpl. apply IHf1. simpl in H. auto.
      - simpl. apply IHf1. simpl in H. auto.
      - simpl. apply IHf1. simpl in H. auto.
Qed.


Lemma AppendNoInputs : forall f1 f2,
  noInputs f1 -> noInputs f2 -> noInputs (appendAny f1 f2).
Proof.
  intros. induction f1. induction f2.
    + reflexivity.
    + simpl appendAny. apply H0.
    + induction a.
      - simpl. simpl in H. auto.
      - simpl. simpl in H. auto.
      - simpl. apply IHf1. simpl in H. auto.
      - simpl. apply IHf1. simpl in H. auto.
      - simpl. apply IHf1. simpl in H. auto.
Qed.

Lemma AppendSingleOutput : forall f1 f2,
  oneOutput f1 -> noOutputs f2 -> oneOutput (appendAny f1 f2).
Proof.
  intros. induction f1. induction f2.
    + inversion H.
    + simpl in H. inversion H.
    + induction a.
      - simpl. apply IHf1. simpl in H. auto.
      - simpl. simpl in H. apply AppendNoOutputs.
        * auto.
        * auto.
      - simpl. apply IHf1. simpl in H. auto.
      - simpl. apply IHf1. simpl in H. auto.
      - simpl. apply IHf1. simpl in H. auto.
Qed.

Lemma AppendSingleOutput2 : forall f1 f2,
  oneOutput f2 -> noOutputs f1 -> oneOutput (appendAny f1 f2).
Proof.  
  induction f1; intros. 
    + simpl. assumption.
    + destruct a; simpl; simpl in H0; try apply IHf1; try assumption.
      inversion H0.
Qed.


Lemma AppendMinOneOutput : forall f1 f2,
  minOneOutput f1 -> noOutputs f2 -> minOneOutput (appendAny f1 f2).
Proof.
  intros. induction f1. induction f2.
    + inversion H.
    + simpl in H. inversion H.
    + induction a.
      - simpl. apply IHf1. simpl in H. auto.
      - simpl. simpl in H. auto.
      - simpl. apply IHf1. simpl in H. auto.
      - simpl. apply IHf1. simpl in H. auto.
      - simpl. apply IHf1. simpl in H. auto.
Qed.


Lemma AppendMoreThanOneOutput : forall f1 f2,
  moreThanOneOutput f1 -> noOutputs f2 -> moreThanOneOutput (appendAny f1 f2).
Proof.
  intros. induction f1. induction f2.
    + inversion H.
    + simpl in H. inversion H.
    + induction a.
      - simpl. apply IHf1. simpl in H. auto.
      - simpl. simpl in H. apply AppendSingleOutput. auto. auto.
      - simpl. apply IHf1. simpl in H. auto.
      - simpl. apply IHf1. simpl in H. auto.
      - simpl. apply IHf1. simpl in H. auto.
Qed.



(* Unused *)
Lemma AppendSingleInput : forall f1 f2,
  oneInput f1 -> noInputs f2 -> oneInput (appendAny f1 f2).
Proof.
  intros. induction f1. induction f2.
    + inversion H.
    + simpl in H. inversion H.
    + induction a.
      - simpl. simpl in H. apply AppendNoInputs.
        * auto.
        * auto.
      - simpl. apply IHf1. simpl in H. auto.
      - simpl. apply IHf1. simpl in H. auto.
      - simpl. apply IHf1. simpl in H. auto.
      - simpl. apply IHf1. simpl in H. auto.
Qed. 


Lemma AppendNoInputOrOutput : forall f1 f2,
  noInputOrOutput f1 -> noInputOrOutput f2 -> noInputOrOutput (appendAny f1 f2).
Proof.
  intros. induction f1. induction f2.
    + reflexivity.
    + simpl appendAny. apply H0.
    + induction a.
      - simpl. simpl in H. auto.
      - simpl. simpl in H. auto.
      - simpl. apply IHf1. simpl in H. auto.
      - simpl. apply IHf1. simpl in H. auto.
      - simpl. apply IHf1. simpl in H. auto.
Qed.

(* Unused *)
Lemma SplitNoInputOrOutput : forall f1 f2,
  noInputOrOutput (appendAny f1 f2) -> noInputOrOutput f1 -> noInputOrOutput f2.
Proof.
  intros. induction f1. induction f2.
    + reflexivity.
    + auto. 
    + induction a.
      - simpl. inversion H.
      - simpl. inversion H.
      - simpl. simpl in H. auto.
      - simpl. simpl in H. auto.
      - simpl. simpl in H. auto.
Qed.

(* These lemmas expands meaning of input output Props *)
(* Unused *)
Lemma noInputOrOutputMeansNoInputsAndNoOutputs: forall fs,
  noInputOrOutput fs ->  noInputs fs -> noOutputs fs.
Proof.
  intros. induction fs.
    + auto.
    + destruct a.
      - inversion H.
      - inversion H.
      - simpl. simpl in H. apply IHfs. auto. auto.
      - simpl. simpl in H. apply IHfs. auto. auto.
      - simpl. simpl in H. apply IHfs. auto. auto.
Qed.

(* Unused *)
Lemma noInputOrOutputMeansNoInputsAndNoOutputs2: forall fs,
  noInputs fs -> noOutputs fs -> noInputOrOutput fs.
Proof.
  intros. induction fs.
    + auto.
    + destruct a.
      - inversion H.
      - simpl. auto.
      - simpl. simpl in H. apply IHfs. auto. auto.
      - simpl. simpl in H. apply IHfs. auto. auto.
      - simpl. simpl in H. apply IHfs. auto. auto.
Qed.


Lemma noInputOrOutputMeansNoInputsAndNoOutputs3: forall fs,
  noInputs fs /\ noOutputs fs -> noInputOrOutput fs.
Proof.
  intros. induction fs.
    + inversion H. auto.
    + destruct a.
      - inversion H. auto.
      - simpl. inversion H. apply H1.
      - simpl. simpl in H. apply IHfs. auto. 
      - simpl. simpl in H. apply IHfs. auto. 
      - simpl. simpl in H. apply IHfs. auto. 
Qed.


Lemma noInputOrOutputMeansNoInputsAndNoOutputs4: forall fs,
  noInputOrOutput fs -> noInputs fs /\ noOutputs fs.
Proof.
  intros. induction fs.
    + inversion H. auto.
    + destruct a.
      - inversion H.
      - simpl. inversion H.
      - simpl. simpl in H. apply IHfs. auto. 
      - simpl. simpl in H. apply IHfs. auto. 
      - simpl. simpl in H. apply IHfs. auto. 
Qed.



Lemma AppendOneInputXorOutput : forall f1 f2,
  oneInputXorOutput f1 -> noInputOrOutput f2 -> oneInputXorOutput (appendAny f1 f2).
Proof.
  intros. induction f1. induction f2.
    + simpl. simpl in H0. auto.
    + simpl appendAny. destruct a.
      - simpl. simpl in H. inversion H.
      - simpl. simpl in H. inversion H.
      - simpl. simpl in H. inversion H.
      - simpl. simpl in H. inversion H.
      - simpl. simpl in H. inversion H.
    + simpl appendAny. destruct a. 
      - simpl in H. simpl. inversion H. split. 
        * apply AppendNoInputs. auto.
          eapply noInputOrOutputMeansNoInputsAndNoOutputs4. auto.
        * apply AppendNoOutputs. auto.
          eapply noInputOrOutputMeansNoInputsAndNoOutputs4. auto.
     - simpl in H. simpl. inversion H. split. 
        * apply AppendNoInputs. auto.
          eapply noInputOrOutputMeansNoInputsAndNoOutputs4. auto.
        * apply AppendNoOutputs. auto.
          eapply noInputOrOutputMeansNoInputsAndNoOutputs4. auto.
      - simpl. simpl in H. apply IHf1. auto. 
      - simpl. simpl in H. apply IHf1. auto. 
      - simpl. simpl in H. apply IHf1. auto.  
Qed. 
 

Lemma AppendOneInputXorOutput2 : forall f1 f2,
  noInputOrOutput f1 -> oneInputXorOutput f2 -> oneInputXorOutput (appendAny f1 f2).
Proof.
  intros. induction f1. induction f2.
    + simpl. simpl in H0. auto.
    + simpl appendAny. destruct a.
      - simpl. split. 
        * simpl in H0. inversion H0. apply H1.
        * simpl in H0. inversion H0. apply H2.
      - simpl. split. 
        * simpl in H0. inversion H0. apply H1.
        * simpl in H0. inversion H0. apply H2.
      - simpl in H0. simpl. auto.
      - simpl in H0. simpl. auto.
      - simpl in H0. simpl. auto.
    + simpl appendAny. destruct a.
      - simpl in H. inversion H.
      - simpl in H. inversion H.
      - simpl. apply IHf1. auto.
      - simpl. apply IHf1. auto.
      - simpl. apply IHf1. auto.
Qed. 

(* Unused *)
Lemma oneInputAndNoOutputsMeaning: forall fs,
  oneInputAndNoOutputs fs ->  oneInput fs -> noOutputs fs.
Proof.
  intros. induction fs.
    + auto. inversion H.
    + destruct a.
      - inversion H. simpl. auto.
      - inversion H.
      - simpl. simpl in H. apply IHfs. auto. auto.
      - simpl. simpl in H. apply IHfs. auto. auto.
      - simpl. simpl in H. apply IHfs. auto. auto.
Qed.


Lemma oneInputAndNoOutputsMeaning2: forall fs,
  oneInputAndNoOutputs fs ->  (oneInput fs /\ noOutputs fs).
Proof.
  intros. induction fs.
    + inversion H.
    + destruct a. 
      - simpl in H. simpl. auto.
      - simpl in H. simpl. inversion H.
      - simpl. simpl in H. apply IHfs. auto.
      - simpl. simpl in H. apply IHfs. auto.
      - simpl. simpl in H. apply IHfs. auto.
Qed.

Lemma oneInputAndNoOutputsMeaning3: forall fs,
  (oneInput fs /\ noOutputs fs) ->  oneInputAndNoOutputs fs.
Proof.
  intros. induction fs.
    + inversion H. auto.
    + destruct a. 
      - simpl in H. simpl. auto.
      - simpl in H. simpl. inversion H. auto.
      - simpl. simpl in H. apply IHfs. auto.
      - simpl. simpl in H. apply IHfs. auto.
      - simpl. simpl in H. apply IHfs. auto.
Qed.

(* Unused *)
Lemma noOutputsInputMeansNoInputs: forall fs,
  noInputOrOutput fs -> noInputs fs.
Proof.
  intros. induction fs.
    + auto.
    + destruct a.
      - inversion H.
      - inversion H.
      - simpl. simpl in H. apply IHfs. auto.
      - simpl. simpl in H. apply IHfs. auto.
      - simpl. simpl in H. apply IHfs. auto.
Qed.

 
Lemma noOutputsInputMeansNoOutputs: forall fs,
  noInputOrOutput fs -> noOutputs fs.
Proof.
  intros. induction fs.
    + auto.
    + destruct a.
      - inversion H.
      - inversion H.
      - simpl. simpl in H. apply IHfs. auto.
      - simpl. simpl in H. apply IHfs. auto.
      - simpl. simpl in H. apply IHfs. auto.
Qed.


Lemma noInputDoesNotMeanOneInput : forall fs,
     noInputs fs /\ oneInput fs -> False.
Proof.
  intros. induction fs. inversion H. inversion H1. apply IHfs. destruct a; simpl in H.
    + inversion H. inversion H0.
    + auto.
    + auto.
    + auto.
    + auto.
Qed.


Lemma noOutputDoesNotMeanOneOutput : forall fs,
     noOutputs fs /\ oneOutput fs -> False.
Proof.
  intros. induction fs. inversion H. inversion H1. apply IHfs. destruct a; simpl in H.
    + auto.
    + inversion H. inversion H0.
    + auto.
    + auto.
    + auto.
Qed.


Lemma noInputDoesNotMeanOneInput1 : forall fs,
     noInputs fs -> oneInput fs -> False.
Proof.
  intros. induction fs. inversion H0. apply IHfs. destruct a; simpl in H; simpl in H0.
    + auto.
    + auto.
    + auto.
    + auto.
    + auto.
    + destruct a.
      - inversion H.
      - simpl in H0. auto.
      - simpl in H0. auto.
      - simpl in H0. auto.
      - simpl in H0. auto.
Qed. 



Lemma  oneOrOtherXorIn : forall fs,
  oneInputXorOutput fs -> oneInput fs ->  noOutputs fs.
Proof.
  intros. induction fs.
    + inversion H0.
    + destruct a. 
      - simpl in H. inversion H. auto.
      - simpl in H0. simpl in H. simpl. eapply noInputDoesNotMeanOneInput. split. inversion H. apply H1. apply H0. 
      - simpl. apply IHfs. simpl in H. auto. simpl in H0. auto. 
      - simpl. apply IHfs. simpl in H. auto. simpl in H0. auto. 
      - simpl. apply IHfs. simpl in H. auto. simpl in H0. auto. 
Qed.
 

Lemma  oneOrOtherXorOut : forall fs,
  oneInputXorOutput fs -> oneOutput fs ->  noInputs fs.
Proof.
  intros. induction fs.
    + inversion H0.
    + destruct a. 
      - simpl in H0. simpl in H. simpl. eapply noOutputDoesNotMeanOneOutput. split. inversion H. apply H2. apply H0. 
      - simpl in H. inversion H. auto.
      - simpl. apply IHfs. simpl in H. auto. simpl in H0. auto. 
      - simpl. apply IHfs. simpl in H. auto. simpl in H0. auto. 
      - simpl. apply IHfs. simpl in H. auto. simpl in H0. auto. 
Qed.

 

Lemma noOutOneInIsOneInXorOut : forall fs,
      oneInput fs /\ noOutputs fs -> oneInputXorOutput fs.

Proof.
  intros. induction fs. inversion H. inversion H0. destruct a; simpl in H.
    + simpl. auto.
    + inversion H. inversion H1.
    + auto.
    + auto.
    + auto.
Qed.



Lemma noInImpliesHasInIsFalse : forall fs,
     noInputs fs -> hasInput fs -> False.

Proof.
  intros. induction fs.
    + auto.
    + apply IHfs.
      - destruct a.
        * inversion H.
        * auto. 
        * auto.
        * auto.
        * auto.
      - destruct a.
        * simpl in H. inversion H. 
        * auto. 
        * auto. 
        * auto. 
        * auto. 
Qed.


Lemma noOutImpliesHasOutIsFalse : forall fs,
     noOutputs fs -> hasOutput fs -> False.

Proof.
  intros. induction fs.
    + auto.
    + apply IHfs.
      - destruct a.
        * auto.
        * inversion H. 
        * auto.
        * auto.
        * auto.
      - destruct a.
        * auto. 
        * inversion H.  
        * auto. 
        * auto. 
        * auto. 
Qed.


Lemma  maxOneInputXor : forall fs,
  oneInputXorOutput fs -> hasInput fs -> oneInput fs.
Proof.
 intros. induction fs.
    + inversion H0.
    + destruct a. 
      - simpl in H0. simpl in H. simpl. inversion H. auto.
      - simpl. apply IHfs. simpl in H. apply noOutOneInIsOneInXorOut. inversion H.
        apply noInImpliesHasInIsFalse in H1. inversion H1. auto. auto.
      - simpl in H0. simpl in H. simpl. auto.
      - simpl in H0. simpl in H. simpl. auto.
      - simpl in H0. simpl in H. simpl. auto.
Qed. 


Lemma noInAndHasInIsFalse : forall fs,
     noInputs fs /\ hasInput fs -> False.
Proof.
    intros. induction fs.
      + inversion H. inversion H1.
      + destruct a. 
          - simpl in H. inversion H. auto.
          - simpl. apply IHfs. simpl in H. auto.
          - simpl in H. auto.
          - simpl in H. auto.
          - simpl in H. auto.
Qed.


Lemma  maxOneInputIfNoOutput : forall fs,
  oneInputXorOutput fs -> hasInput fs -> oneInputAndNoOutputs fs.
Proof.
 intros. induction fs.
    + inversion H0.
    + destruct a. 
      - auto.
      - simpl. simpl in H. simpl in H0. auto. eapply noInAndHasInIsFalse. split.
        inversion H. apply H1. apply H0.
      - auto.
      - auto.
      - auto.
Qed. 



Lemma  maxOneOutputXor : forall fs,
  oneInputXorOutput fs -> hasOutput fs -> oneOutput fs.
Proof.
 intros. induction fs.
    + inversion H0.
    + destruct a. 
      - simpl in H0. simpl in H. simpl. inversion H. 
        apply noOutImpliesHasOutIsFalse in H2.
        * inversion H2.
        * auto.
      - simpl in H0. simpl in H. simpl. inversion H. auto.
      - simpl in H0. simpl in H. simpl. apply IHfs. auto. auto.
      - simpl in H0. simpl in H. simpl. apply IHfs. auto. auto.
      - simpl in H0. simpl in H. simpl. apply IHfs. auto. auto.
Qed.



(* Unused *)
Lemma noOutputsMeansOneOrNo: forall fs,
   noOutputs fs -> oneOrNoOutput fs.
Proof.
  intros. induction fs.
    + reflexivity.
    + destruct a; simpl in H; simpl; try apply IHfs; try assumption.
      - inversion H.
Qed.



Lemma oneOutputsInputMeansOneOrNo: forall fs,
  oneInputXorOutput fs -> oneOrNoInputXorOutput fs.
Proof.
  intros. induction fs.
    + reflexivity.
    + destruct a; simpl in H; simpl; try apply IHfs; try assumption.
Qed.


Lemma noOutputsInputMeansOneOrNo: forall fs,
  noInputOrOutput fs -> oneOrNoInputXorOutput fs.
Proof.
  intros. induction fs.
    + reflexivity.
    + destruct a; simpl in H; simpl; try apply IHfs; try assumption;
       inversion H.
Qed.



(* Unused *)
Lemma oneOutputsMeansOneOrNo: forall fs,
   oneOutput fs -> oneOrNoOutput fs.
Proof.
  intros. induction fs.
    + reflexivity.
    + destruct a; simpl in H; simpl; try apply IHfs; try assumption.
Qed.

Axiom outIsNotIn: forall trm t, IN t = OUT trm -> False.

Lemma outIsNotAsubListOfIn: forall trm t, subList [OUT trm] [IN t] -> False.
Proof.
  intros. inversion H. simpl in H0. inversion H0. apply outIsNotIn in H2. auto. auto. 

Qed.

(* Rajiv : Tried proof
Lemma subListSimplifiedIn: forall trm t fs, subList [OUT trm] (IN t :: fs) -> subList [OUT trm] fs.
Proof.
  intros. induction fs.
    + apply outIsNotAsubListOfIn in H. simpl. split. auto. auto.
    + destruct a.
      - simpl. split. 
          * left. simpl in H. inversion H. destruct H0. eapply outIsNotIn in H0. inversion H0.             destruct H0. eapply outIsNotIn in H0. inversion H0. destruct H0.
          * destruct H0. eapply outIsNotIn in H0. inversion H0.

Qed. *)



Axiom subListSimplifiedIn: forall trm t fs, subList [OUT trm] (IN t :: fs) -> subList [OUT trm] fs.


Axiom subListSimplifiedK: forall trm t fs, subList [OUT trm] (K t :: fs) -> subList [OUT trm] fs.

Axiom subListSimplifiedFr: forall trm t fs, subList [OUT trm] (FR_P t :: fs) -> subList [OUT trm] fs.

Axiom subListSimplifiedState: forall trm n t fs, subList [OUT trm] (STATE n t :: fs) -> subList [OUT trm] fs.

Axiom noOutputsSimplified : forall f t trm fs,
noOutputs (removeFact (OUT trm) (f :: fs)) /\ not (eq_fact f (OUT t)) ->
noOutputs (removeFact (OUT trm) fs).

(* Tried proof 
Lemma  removeOneOutputOut : forall fs trm,
  oneInputXorOutput fs -> (subList [OUT trm] fs) -> noOutputs (removeFact (OUT trm) fs).
Proof.
  intros. induction fs.
    + simpl. auto.
    + destruct a. 
      - eapply noOutputsAcrossRemoveFact with (f:=OUT trm) (fs:= (IN t :: fs)). simpl in H; simpl; try apply IHfs. inversion H. auto.
      - eapply noOutputsAcrossRemoveFact with (f:=OUT trm) (fs:= (OUT t :: fs)). simpl. simpl in H.  simpl; try apply IHfs. auto.
      - apply noOutOneInIsOneInXorOut. split. apply noInputOrOutputMeansNoInputsAndNoOutputs3 in H. inversion H1. 2:{ auto. } inversion H2.

  2:{
      - apply subListSimplified in H0. auto. } 2:{
      - destruct H. simpl. apply IHfs. in H0. 
        *
Qed.
 *)

Axiom removeOneOutputOut : forall fs trm,
  oneInputXorOutput fs -> (subList [OUT trm] fs) -> noOutputs (removeFact (OUT trm) fs).

Axiom removeOneOutputIn : forall fs trm,
  oneInputXorOutput fs -> (subList [OUT trm] fs) -> noInputs (removeFact (OUT trm) fs).

(* The following Axiom seems incorrect. Should be this lemma 

Lemma InputInSublist : forall f1 f2,
  subList f1 f2 -> oneInput f1 -> minOneInput f2.
Proof.
  intros. induction f1. induction f2.
    + auto.
    + inversion H0.
    + apply IHf1. destruct a. 
      - simpl in H. inversion H. simpl in H1.

Qed.
 
*)

Axiom InputInSublist : forall f1 f2,
  subList f1 f2 -> oneInput f1 -> oneInput f2. 

Lemma oneInputHasInput : forall f1,
  oneInput f1 -> hasInput f1.
Proof.
  intros. induction f1.
    + auto.
    + destruct a; simpl in H.
      - simpl. auto.
      - simpl. auto.
      - simpl. auto.
      - simpl. auto.
      - simpl. auto.
Qed.


Lemma noInputSubst : forall f sigma, 
 noInputs f -> noInputs (applySubFacts sigma f).
Proof.
  intros. induction f.
    + auto.
    + destruct a. simpl in H. inversion H. 
      - simpl in H; simpl; apply IHf; auto.
      - simpl in H; simpl; apply IHf; auto.
      - simpl in H; simpl; apply IHf; auto.
      - simpl in H; simpl; apply IHf; auto.
Qed.


Lemma oneInputSubst : forall f sigma, 
 oneInput f -> oneInput (applySubFacts sigma f).
Proof.
  intros. induction f.
    + auto.
    + destruct a. simpl in H.
      - simpl. eapply noInputSubst. auto. 
      - simpl.  apply IHf. auto.
      - simpl.  apply IHf. auto.
      - simpl.  apply IHf. auto.
      - simpl.  apply IHf. auto.
Qed.


(* This Axiom was incorrect, 
  the correct one should have noInputs also, changed in Lemma below 

Axiom oneOutIsOneXorNo : forall fs,
  oneOutput fs -> oneInputXorOutput fs.
*)


Lemma oneOutIsOneXorNo : forall fs,
  oneOutput fs -> noInputs fs -> oneInputXorOutput fs.
Proof.
  intros. induction fs.
    + inversion H.
    + destruct a.
      - inversion H0.
      - simpl in H. simpl in H0. simpl. split. auto. auto.
      - simpl in H. simpl in H0. simpl. apply IHfs. auto. auto.
      - simpl in H. simpl in H0. simpl. apply IHfs. auto. auto.
      - simpl in H. simpl in H0. simpl. apply IHfs. auto. auto.
Qed.


Lemma subListToHasOutput : forall trm fs,
   subList [OUT trm] fs -> hasOutput fs.
Proof.
  intros. induction fs.
    + inversion H.
    + destruct a.
      - simpl. apply IHfs. apply subListSimplifiedIn in H. auto.
      - simpl. auto.
      - simpl. apply IHfs. apply subListSimplifiedK in H. auto.
      - simpl. apply IHfs. apply subListSimplifiedState in H. auto.
      - simpl. apply IHfs. apply subListSimplifiedFr in H. auto.
Qed.


Axiom destructReduceSigma : forall r f1 l f2 sigma,
  groundRule (applySubRule sigma r) -> 
    reduceWithGroundRule (applySubRule sigma r) f1 l f2 ->
      reduceWithRuleSigma r sigma f1 l f2.


Axiom subListOneOrOther : forall f1 f fs,
  subList [f1] (f::fs) -> not (eq_fact  f1 f)  -> subList [f1] fs.


Lemma noOutMeansNoOutSubList : forall f1 trm,
 subList [OUT trm] f1 -> noInputOrOutput f1 -> False.
Proof.
  intros. induction f1.
    + simpl in H0. inversion H.
    + apply IHf1. destruct a; simpl in H0.
      - inversion H0.
      - inversion H0.
      - apply subListOneOrOther in H. 
          * auto.
          * simpl. unfold not. auto. 
      - apply subListOneOrOther in H. 
          * auto.
          * simpl. unfold not. auto. 
     - apply subListOneOrOther in H. 
          * auto.
          * simpl. unfold not. auto. 
      - apply noInputOrOutputTail in H0. auto.
Qed.



(*==============================================================*)
(* These rules verify that each type of rule works keep the right 
   number of inputs and outputs *)
(*==============================================================*)


 
Lemma InputToOutputMustHaveInput : forall f1 f2 sigma r l,
  reduceWithGroundRule (applySubRule sigma r) f1 l f2 
  -> InputToOutputProtocolRule r -> hasInput f1.
Proof.
  intros.  destruct r.
  + inversion H0.
  + inversion H0. inversion H2. inversion H4. inversion H.
    subst. simpl in H7. simpl in H. 
    apply InputInSublist in H7. apply oneInputHasInput. assumption.
    apply oneInputSubst. assumption.
Qed.



Lemma StateToOutputNoOutputRule : forall  r sigma f1 l f2,
  noOutputs f1 -> StateToOutputProtocolRule r ->
    reduceWithRuleSigma r sigma f1 l f2
      -> oneOutput f2.
Proof.
  intros. destruct r.
  + inversion H0.
  + unfold reduceWithRuleSigma in H1. inversion H1. inversion H2. destruct x0.
    - inversion H3. simpl in H5. inversion H5. inversion H9.
    - inversion H0. inversion H6. inversion H8.
      inversion H4. simpl.  subst. 
      assert (HA := ginstWithSigmaOneOutputC H3). apply HA in H10.
      apply AppendSingleOutput. assumption.
      apply noOutputsAcrossRemove. assumption.
Qed.


Axiom StateToStateoneOutputXorInputIs : forall  r sigma f1 l f2 trms,
  oneOutputXorInputIs f1 trms   -> StateToStateProtocolRule r ->
    reduceWithRuleSigma r sigma f1 l f2
      ->  oneOutputXorInputIs f2 trms.
(* 
Proof.
  intros. induction r.
    + inversion H0.
    + unfold reduceWithRuleSigma in H1. inversion H1. inversion H2. destruct x0.
       - inversion H3. simpl in H5. inversion H5. inversion H9.
Qed.
 *)


Lemma  StateToStateNoOutputRule : forall  r sigma f1 l f2,
  noInputOrOutput f1 -> StateToStateProtocolRule r ->
    reduceWithRuleSigma r sigma f1 l f2
      -> noInputOrOutput f2.
Proof.
  intros. destruct r.
    + inversion H0.
    + unfold reduceWithRuleSigma in H1. inversion H1. inversion H2. destruct x0.
       - inversion H3. simpl in H5. inversion H5. inversion H9.
       -  inversion H0. inversion H6. inversion H8.
            inversion H4. simpl.  subst. 
            assert (HA := ginstWithSigmaNoInputOutputC H3).
            apply AppendNoInputOrOutput. apply HA.
            apply noInputOrOutputMeansNoInputsAndNoOutputs3 in H8. auto.
            apply noInputOrOutputAcrossRemove. assumption. 
Qed.


Lemma noInputOutputImpliesOneOutputIsTrue: forall fs,
      noInputOrOutput fs -> oneOutput fs -> True.
Proof.
  intros. induction fs.
    + inversion H0.
    + destruct a.
      - inversion H.
      - inversion H.
      - apply IHfs. simpl in H. simpl in H0. auto. auto.
      - apply IHfs. simpl in H. simpl in H0. auto. auto.
      - apply IHfs. simpl in H. simpl in H0. auto. auto.
Qed.


Lemma oneOutputImpliesnoInputOutputIsFalse: forall fs,
      oneOutput fs -> noInputOrOutput fs -> False.
Proof.
  intros. induction fs.
    + simpl in H. apply H.
    + destruct a.
      - inversion H0.
      - inversion H0.
      - apply IHfs. simpl in H. simpl in H0. auto. auto.
      - apply IHfs. simpl in H. simpl in H0. auto. auto.
      - apply IHfs. simpl in H. simpl in H0. auto. auto.
Qed.


Lemma StateToStateOneOutRule : forall  r sigma f1 l f2,
  oneOutput f1 -> StateToStateProtocolRule r ->
    reduceWithRuleSigma r sigma f1 l f2
      -> oneOutput f2.
Proof.
  intros. destruct r.
    + inversion H0.
    + unfold reduceWithRuleSigma in H1. inversion H1. inversion H2. destruct x0.
       - inversion H3. simpl in H5. inversion H5. inversion H9.
       - inversion H0. inversion H6. inversion H8. 
         inversion H4. simpl. subst.
         assert (HA := ginstWithSigmaNoOutputP H3).
         apply HA in H7. apply AppendSingleOutput2.
         apply oneOutputsAcrossRemove; assumption.
         eapply ginstWithSigmaNoOutputC. apply H3. assumption.
Qed. 


Lemma StateToStateXorOutRule : forall  r sigma f1 l f2,
   oneInputXorOutput f1  -> StateToStateProtocolRule r ->
    reduceWithRuleSigma r sigma f1 l f2
      -> oneInputXorOutput f2.
Proof.
  intros. destruct r.
    + inversion H0.
    + unfold reduceWithRuleSigma in H1. inversion H1. inversion H2. destruct x0.
       - inversion H3. simpl in H5. inversion H5. inversion H9.
       - inversion H0. inversion H6. inversion H8. 
         inversion H4. simpl. simpl in H15.  subst.  
         assert (HA := ginstWithSigmaNoInputOutputC H3).
         apply noInputOrOutputMeansNoInputsAndNoOutputs3 in H8.
         apply AppendOneInputXorOutput2.
         apply HA. apply H8.
         apply oneInputXorOutputAcrossRemove. apply H.
         assert (HA1 := ginstWithSigmaNoInputOutputP H3).
         apply HA1. eapply noInputOrOutputMeansNoInputsAndNoOutputs3. split.
        auto. auto.
Qed. 


(* Changed oneInput in this Axiom to oneInputAndNoOutputs and 
proved Lemma InputToOutputOneOutRuleNew below *)
(* No longer using this
Axiom InputToOutputOneOutRule : forall  r sigma f1 l f2,
  oneInput f1 -> InputToOutputProtocolRule r ->
    reduceWithRuleSigma r sigma f1 l f2
      -> oneOutput f2.
 *)

Lemma InputToOutputOneOutRule : forall  r sigma f1 l f2,
  oneInputAndNoOutputs f1 -> InputToOutputProtocolRule r ->
    reduceWithRuleSigma r sigma f1 l f2
      -> oneOutput f2.
Proof.
  intros. destruct r.
    + inversion H0.
    + unfold reduceWithRuleSigma in H1. inversion H1. inversion H2. destruct x0.
       - inversion H3. simpl in H5. inversion H5. inversion H9.
       -  inversion H0. inversion H6. inversion H8.
            inversion H4. simpl.  subst. 
            assert (HA := ginstWithSigmaOneOutputC H3).
            apply AppendSingleOutput. apply HA. inversion H8. auto.
            apply noOutputsAcrossRemove. 
            apply oneInputAndNoOutputsMeaning2 in H. inversion H. assumption.
Qed.

(* Rajiv : Tried proof
Lemma InputToOutputRemovesInput : forall  r sigma f1 l f2,
  oneInputXorOutput f1 -> InputToOutputProtocolRule r ->
    reduceWithRuleSigma r sigma f1 l f2
      -> noInputs f2.
Proof.
  intros. destruct r.
    + inversion H0.
    + unfold reduceWithRuleSigma in H1. inversion H1. inversion H2. destruct x0.
       - inversion H3. simpl in H5. inversion H5. inversion H9.
       - inversion H0. inversion H6. inversion H8. 
         inversion H4. simpl.  subst. eapply AppendOneInputXorOutput in H.
         assert (HA := ginstWithSigmaOneInputXorOutputC H3).
         apply oneOrOtherXorIn in H. apply AppendNoInputs. 2:{
        apply noInputsAcrossRemove. assumption.
 
Qed.
*)

Axiom InputToOutputRemovesInput : forall  r sigma f1 l f2,
  oneInputXorOutput f1 -> InputToOutputProtocolRule r ->
    reduceWithRuleSigma r sigma f1 l f2
      -> noInputs f2.

(* 
Lemma StateToOutputDoesNotAddInput : forall  r sigma f1 l f2,
  noInputOrOutput f1 -> StateToOutputProtocolRule r ->
    reduceWithRuleSigma r sigma f1 l f2
      -> noInputs f2.
Proof.
  intros. destruct r.
    + inversion H0.
    + unfold reduceWithRuleSigma in H1. inversion H1. inversion H2. destruct x0.
       - inversion H3. simpl in H5. inversion H5. inversion H9.
       - inversion H0. inversion H6. inversion H8.
         inversion H4. simpl.  subst. assert (HA := ginstWithSigmaOneOutputC H3).
Qed. *)
  

Axiom StateToOutputDoesNotAddInput : forall  r sigma f1 l f2,
  noInputOrOutput f1 -> StateToOutputProtocolRule r ->
    reduceWithRuleSigma r sigma f1 l f2
      -> noInputs f2.


(* Rajiv : Tried proof
Lemma InputToStateOneOutRule : forall  r sigma f1 l f2,
  oneInput f1 -> noOutputs f1 -> InputToStateProtocolRule r ->
    reduceWithRuleSigma r sigma f1 l f2
      -> noInputOrOutput f2.
Proof.
  intros. destruct r.
  + inversion H1.
  + unfold reduceWithRuleSigma in H2. inversion H2. inversion H3. destruct x0.
       - inversion H4. inversion H6. inversion H10.
       - inversion H1. inversion H7. inversion H9. 
         inversion H4. inversion H12.  subst. 
        eapply ginstWithSigmaNoInputOutputC. 2:{
         apply noInputOrOutputMeansNoInputsAndNoOutputs3 in H9. apply H9. }

 *)

Axiom InputToStateOneOutRule : forall  r sigma f1 l f2,
  oneInput f1 -> noOutputs f1 -> InputToStateProtocolRule r ->
    reduceWithRuleSigma r sigma f1 l f2
      -> noInputOrOutput f2.


Lemma InputToStateMustHaveInput : forall f1 f2 sigma r l,
  reduceWithGroundRule (applySubRule sigma r) f1 l f2 
  -> InputToStateProtocolRule r -> hasInput f1.
Proof.
  intros. destruct r. 
   - simpl in H0.  inversion H0. 
   - simpl in H0.  inversion H0.  inversion H2.  inversion H4. 
     inversion H. subst. simpl in H7. simpl in H.
     apply InputInSublist in H7. apply oneInputHasInput. assumption.
     apply oneInputSubst. assumption.
Qed.

Axiom FreshRuleNoOutputToNoOutput : forall f1 f2 fn sigma, 
  reduceWithRuleSigma (freshRuleP fn) sigma f1 emptyLabel f2
    -> noInputOrOutput f1 -> noInputOrOutput f2.


Axiom FreshRuleOneOutputToOneOutput : forall f1 f2 fn sigma, 
  reduceWithRuleSigma (freshRuleP fn) sigma f1 emptyLabel f2
    -> oneInputXorOutput f1 -> oneInputXorOutput f2.


Axiom FreshRuleDoesNotChangeOutputs : forall f1 f2 fn sigma, 
  reduceWithRuleSigma (freshRuleP fn) sigma f1 emptyLabel f2
    -> oneOrNoOutput f1 -> oneOrNoOutput f2.


Lemma OneOrNoOutputsFromOutState : forall rlProto sigmas fs1 l fs2,
  runInOrderSigmaProtocol rlProto sigmas fs1 l fs2
    -> (oneInputXorOutput fs1 -> wellFormedProtoRuleFromInOut rlProto -> oneOrNoInputXorOutput fs2)
       /\ (noInputOrOutput fs1 -> wellFormedProtoRuleNoInOut rlProto -> oneOrNoInputXorOutput fs2).
Proof.
  intros. induction H; split; intros.
   (*Sigma_Run_Stop_P*) + apply oneOutputsInputMeansOneOrNo. assumption.
   (*Sigma_Run_Stop_P*) + apply noOutputsInputMeansOneOrNo. assumption.
   (*Sigma_Run_Step_P from one output*)
   + inversion IHrunInOrderSigmaProtocol. simpl in H3. inversion H3.
      - (* InputToStateProtocolRule *) inversion H6.  apply H5; try assumption.
        apply InputToStateOneOutRule with (r:=r) (sigma:=sigmaNow) (l:=l) (f1:=f1).
        * apply InputToStateMustHaveInput in H0. apply maxOneInputXor; assumption.
          assumption.
        * apply InputToStateMustHaveInput in H0; try assumption.
          apply oneOrOtherXorIn. assumption. apply maxOneInputXor; assumption.
        * apply H7.
        * apply destructReduceSigma; assumption.
      - inversion H6.
         * (* StateToStateProtocolRule r *) inversion H7. apply H4; try assumption.
            eapply StateToStateXorOutRule. apply H2. apply H8. 
            unfold reduceWithRuleSigma.
          exists (applySubRule sigmaNow r). split.
          apply GinstSigma. split.  reflexivity. assumption. apply H0.
         * (* InputToOutputProtocolRule r *) inversion H7. apply H4; try assumption.
           apply oneOutIsOneXorNo. eapply InputToOutputOneOutRule.
          apply maxOneInputIfNoOutput.  apply H2. eapply InputToOutputMustHaveInput.
          apply H0. assumption. apply H8. apply destructReduceSigma. apply H. apply H0.
          eapply InputToOutputRemovesInput. apply H2. apply H8. apply destructReduceSigma.
          apply H. apply H0. 
    (*Sigma_Run_Step_P from no output*)
    + inversion IHrunInOrderSigmaProtocol. simpl in H3. inversion H3.
      - (* StateToOutputProtocolRule *) inversion H6. apply H4; try assumption.
        apply oneOutIsOneXorNo. eapply StateToOutputNoOutputRule.
        apply noOutputsInputMeansNoOutputs. apply H2. apply H7. 
        apply destructReduceSigma. apply H. apply H0.
         eapply StateToOutputDoesNotAddInput. apply H2. apply H7. apply destructReduceSigma.
          apply H. apply H0. 
      - (* StateToStateProtocolRule *) inversion H6. apply H5; try assumption.
        eapply StateToStateNoOutputRule.
        * apply H2.
        * apply H7.
        * apply destructReduceSigma. apply H. apply H0.
    (* Sigma_Run_Step_Silent_P from one output *)
    + inversion IHrunInOrderSigmaProtocol. simpl in H3. inversion H3.
      - (* InputToStateProtocolRule *) inversion H6.  apply H5; try assumption.
        apply InputToStateOneOutRule with (r:=r) (sigma:=sigmaNow) (l:=emptyLabel) (f1:=f1).
        * apply InputToStateMustHaveInput in H0. apply maxOneInputXor; assumption.
          assumption.
        * apply InputToStateMustHaveInput in H0; try assumption.
          apply oneOrOtherXorIn. assumption. apply maxOneInputXor; assumption.
        * apply H7.
        * apply destructReduceSigma; assumption.
      - inversion H6.
         * (* StateToStateProtocolRule r *) inversion H7. apply H4; try assumption.
            eapply StateToStateXorOutRule. apply H2. apply H8. 
            unfold reduceWithRuleSigma.
          exists (applySubRule sigmaNow r). split.
          apply GinstSigma. split.  reflexivity. assumption. apply H0.
         * (* InputToOutputProtocolRule r *) inversion H7. apply H4; try assumption.
           apply oneOutIsOneXorNo. eapply InputToOutputOneOutRule.
          apply maxOneInputIfNoOutput.  apply H2. eapply InputToOutputMustHaveInput.
          apply H0. assumption. apply H8. apply destructReduceSigma. apply H. apply H0.
          eapply InputToOutputRemovesInput. apply H2. apply H8. apply destructReduceSigma.
          apply H. apply H0.
    (*Sigma_Run_Step_Silent_P from no output*)
    + inversion IHrunInOrderSigmaProtocol. simpl in H3. inversion H3.
      - (* StateToOutputProtocolRule *) inversion H6. apply H4; try assumption.
        apply oneOutIsOneXorNo. eapply StateToOutputNoOutputRule.
        apply noOutputsInputMeansNoOutputs. apply H2. apply H7. 
        apply destructReduceSigma. apply H. apply H0.
        eapply StateToOutputDoesNotAddInput. apply H2. apply H7. apply destructReduceSigma.
          apply H. apply H0.
      - (* StateToStateProtocolRule *) inversion H6. apply H5; try assumption.
        eapply StateToStateNoOutputRule.
        * apply H2.
        * apply H7.
        * apply destructReduceSigma. apply H. apply H0.
    (* Sigma_Run_Comm_P from one input *)
    + inversion IHrunInOrderSigmaProtocol. apply H3; try assumption. simpl. split.
      * apply removeOneOutputIn; assumption.
      * apply removeOneOutputOut; assumption.
    (* Sigma_Run_Comm_P from one input (contradiction) *)
    + apply noOutMeansNoOutSubList in H. inversion H. apply H1.
Qed.



Axiom SetupRuleNoInOutDoesNotAddInOut : forall  r  f1 l f2,
  noInputOrOutput f1 -> wellFormedSetupRuleNoInOut r ->
    reduceWithRules r f1 l f2
      -> noInputOrOutput f2.


Axiom SetupRuleFromInOutDoesNotChangeInOut : forall  r  f1 l f2,
  oneInputXorOutput f1 -> wellFormedSetupRuleFromInOut r ->
    reduceWithRules r f1 l f2
      -> oneInputXorOutput f2.


Axiom FreshRuleNoOutputToNoOutput1 : forall f1 f2 fn , 
  reduceWithRule (freshRuleP fn)  f1 emptyLabel f2
    -> noInputOrOutput f1 -> noInputOrOutput f2.


Axiom FreshRuleOneOutputToOneOutput1 : forall f1 f2 fn , 
  reduceWithRule (freshRuleP fn)  f1 emptyLabel f2
    -> oneInputXorOutput f1 -> oneInputXorOutput f2.


Axiom FreshRuleDoesNotChangeOutputs1 : forall f1 f2 fn , 
  reduceWithRule (freshRuleP fn)  f1 emptyLabel f2
    -> oneOrNoOutput f1 -> oneOrNoOutput f2.

Lemma OneOrNoOutputsFromOutStateSetup : forall rlSetup fs1 l fs2,
  run rlSetup fs1 l fs2
    -> (oneInputXorOutput fs1 -> wellFormedSetupRuleFromInOut rlSetup -> oneOrNoInputXorOutput fs2)
       /\ (noInputOrOutput fs1 -> wellFormedSetupRuleNoInOut rlSetup -> oneOrNoInputXorOutput fs2).
Proof.
 intros. induction H; split; intros. 
   + apply oneOutputsInputMeansOneOrNo. assumption.
   + apply noOutputsInputMeansOneOrNo. assumption. 
    + inversion IHrun. apply H3. eapply SetupRuleFromInOutDoesNotChangeInOut. 
      apply H1. apply H2. apply H. apply H2.
    + inversion IHrun. apply H4. eapply SetupRuleNoInOutDoesNotAddInOut. 
      apply H1. apply H2. apply H. apply H2.  
    + inversion IHrun. apply H3. eapply SetupRuleFromInOutDoesNotChangeInOut. 
      apply H1. apply H2. apply H. apply H2.  
    + inversion IHrun. apply H4. eapply SetupRuleNoInOutDoesNotAddInOut. 
      apply H1. apply H2. apply H. apply H2.
    + inversion IHrun. apply H3. eapply FreshRuleOneOutputToOneOutput1. 
      apply H. apply H1. apply H2. 
    + inversion IHrun. apply H4. eapply FreshRuleNoOutputToNoOutput1. 
      apply H. apply H1. apply H2. 
Qed.

(* Rajiv : Tried Proof 

Lemma OneOrNoOutputsFromOutStateStdRun : forall rlProto rlSetup sigmas fs1 l fs2,
  runInOrderSigma rlProto rlSetup sigmas fs1 l fs2
    -> (oneInputXorOutput fs1 -> wellFormedProtoRuleFromInOut rlProto -> oneOrNoInputXorOutput fs2)
       /\ (noInputOrOutput fs1 -> wellFormedProtoRuleNoInOut rlProto -> oneOrNoInputXorOutput fs2).
Proof.
  intros. induction H; split; intros. 
   + inversion H. apply OneOrNoOutputsFromOutStateSetup in H2. inversion H2. inversion H3. 
     apply OneOrNoOutputsFromOutState in H6. inversion H6. apply H8. apply oneOutputsInputMeansOneOrNo.  destruct fsMid.
      - simpl. 
   
*)

Axiom OneOrNoOutputsFromOutStateStdRun : forall rlProto rlSetup sigmas fs1 l fs2,
  runInOrderSigma rlProto rlSetup sigmas fs1 l fs2
    -> (oneInputXorOutput fs1 -> wellFormedProtoRuleFromInOut rlProto -> oneOrNoInputXorOutput fs2)
       /\ (noInputOrOutput fs1 -> wellFormedProtoRuleNoInOut rlProto -> oneOrNoInputXorOutput fs2).


Axiom OneOrNoOutputsFromOutStateSingle : forall sigma r1 rs f1 l f2,
  groundRule (applySubRule sigma r1)
    -> reduceWithGroundRule (applySubRule sigma r1) f1 l f2
      -> wellformedRulesFromState f1 (r1::rs)
        -> oneInputXorOutput f2.

(* ========== *)
(* We have a problem here, that runInOrderSigmaProtocol does not require rule to be ground *)
(* ========== *)

(*
Lemma ruleWihoutOutputCantMakeOutput : forall rule sigma f1 label f2 , 
         reduceWithRuleSigma rule sigma f1 label f2
           -> noOutputs f1 -> (noOutputs (conclFacts rule)) -> noOutputs f2.
Proof. intros. inversion H. inversion H2.  inversion H3. inversion H5. 
        induction f1. induction f2.
        + reflexivity.
        + simpl. destruct a; simpl in H4; auto.
            - apply IHf2.
              * simpl in H4. inversion H. simpl in H0. auto.
  

Lemma emptyRuleListCantMakeOutput : forall  sigmas f1 t f2,
   wellFormedProtoRules [] ->
    runInOrderSigmaProtocol  [] sigmas f1 t f2 ->
      noOutputs f1 -> noOutputs f2.
Proof. intros. induction f2. induction f1.
        + inversion H. auto.
        + inversion H. auto.
        + destruct a. 
            -  simpl. apply IHf2. inversion H0. 
              * rewrite <- H6 in H0. assumption. inversion IHf2. H1. eapply IHf2 in H1. rewrite H6. simpl.  destruct H. simpl in H0. apply IHrunInOrderSigmaProtocol. 
            - simpl in H. destruct H. destruct H. apply H4.
            - inversion H0. rewrite <- H7 in H0. 
*)




(* 

Lemma ruleCanMakeOutput : forall rule sigma f1 label f2 , reduceWithRuleSigma rule sigma f1 label f2
-> noOutputs f1 -> (oneOutput (conclFacts rule)) -> oneOutput f2.
Proof.
      intros. inversion H. inversion H2. 
      inversion H3. inversion H5. 
      induction rule0.
        +
          simpl in H9. rewrite <- H9 in H4. inversion H4. simpl in H15. simpl.  
 *)


Axiom ruleCanMakeOutput : forall rule sigma f1 label f2 , reduceWithRuleSigma rule sigma f1 label f2
-> noOutputs f1 -> (oneOutput (conclFacts rule)) -> oneOutput f2.


(*
Axiom outputWillMatchRule : forall rule sigma f1 label f2 trms1 trms2, 
  reduceWithRuleSigma rule sigma f1 label f2 -> noOutputs f1 -> 
      oneOutputIs f2 (OUT trms1) -> (oneOutputIs (conclFacts rule) (OUT trms2) -> (applySubTerms sigma trms2) = trms1).
*)



(* NEW AXIOM *)
Axiom outputInRuleWillMatchRule : forall rule1 rules sigma f1 l f2 vars,
  reduceWithGroundRule (applySubRule sigma rule1) f1 l f2
    -> groundRule (applySubRule sigma rule1) 
      -> wellformedRulesFromState f1 (rule1::rules)
        -> oneOutputAndNoInputIs (conclFacts rule1) (OUT vars)
          -> member (OUT (applySubTerms sigma vars)) f2.


(* NEW AXIOM *)

Axiom inputsWillMatch : forall rule1 rules sigma f1 l f2 vars,
  reduceWithGroundRule (applySubRule sigma rule1) f1 l f2
    -> groundRule (applySubRule sigma rule1) 
      -> wellformedRulesFromState f1 (rule1::rules)
        -> oneInputAndNoOutputIs (premiseFacts rule1) (IN vars)
          -> member (IN (applySubTerms sigma vars)) f1.


(* NEW AXIOM *)

Axiom outputWillMatchFollowingInput :  forall rule rs sigma sigmas f1 l f2 vars trms,
runInOrderSigmaProtocol (rule::rs) (sigma::sigmas) f1 l f2
 -> oneInputXorOutput f1 ->  member (OUT trms) f1
   -> oneInputAndNoOutputIs (premiseFacts rule) (IN vars)
-> eq_terms trms (applySubTerms sigma vars).

Axiom outputIOruleWillMatchRule : forall f1 l f2 rule sigma,
  oneInputXorOutput f1 -> InputToOutputProtocolRule rule
    -> reduceWithGroundRule (applySubRule sigma rule) f1 l f2
      -> exists var, member (OUT var) (conclFacts rule) /\ member (OUT (applySubTerms sigma var)) f2.


Axiom OutputInRuleWillMatch : forall r sigma f1 t f2 trms,
  runInOrderSigmaProtocol [r] [sigma] f1 t f2
    -> wellformedRulesFromState f1 [r]
      -> oneOutputAndNoInputIs (conclFacts r) (OUT trms)
        -> oneOutputAndNoInputIs f2 (OUT (applySubTerms sigma trms)). 


Axiom outputMatchesNextInput : forall r1 r2 sigma1 sigma2 trms1 trms2 f1 trace f3 ,
    runInOrderSigmaProtocol [r1;r2] [sigma1;sigma2] f1 trace f3
      -> oneOutputAndNoInputIs (conclFacts r1) (OUT trms1) 
        -> oneOutputAndNoInputIs (premiseFacts r2) (IN trms2)
          -> eq_terms (applySubTerms sigma1 trms1) (applySubTerms sigma2 trms2).



Axiom outputMatchesNextInputEnd : forall r1 r2 sigma1 sigma2 trms1 trms2 f1 trace f3 sigmaList rulesList setuprules,
    runInOrderSigma (appendAny rulesList [r1;r2]) setuprules (appendAny sigmaList [sigma1;sigma2]) f1 trace f3
      -> oneOutputAndNoInputIs (conclFacts r1) (OUT trms1) 
        -> oneOutputAndNoInputIs (premiseFacts r2) (IN trms2)
          -> eq_terms (applySubTerms sigma1 trms1) (applySubTerms sigma2 trms2).



(* I wrongly defined wellformedRulesFromState as a fixpoint and not a defintion 
   meaning it did not unwind, this is now fixed, so this lemma is not needed 
Axiom HelperwellformedRulesFromState : forall fs rs, 
wellformedRulesFromState fs rs -> 
        (oneInputXorOutput fs /\ wellFormedProtoRuleFromInOut rs) \/
        (noInputOrOutput fs /\ wellFormedProtoRuleNoInOut rs).
*)

(*
f2 has output that matchs sigma out in rule
no input
*)

(*TOM: From some reason I can't seen to unwind wellformedRulesFromState, hence I'm using the above axiom
       which just restates the definition. Please look into this and see if you can fix it *)

Lemma outputMatchesNextInputEndProtocol : forall r1 r2 sigma1 sigma2 trms1 trms2 f1 trace f3 ,
    runInOrderSigmaProtocol ( [r1;r2]) ([sigma1;sigma2]) f1 trace f3
      -> wellformedRulesFromState f1 [r1;r2] 
      -> oneOutputAndNoInputIs (conclFacts r1) (OUT trms1) -> oneInputAndNoOutputIs (premiseFacts r2) (IN trms2)
          -> eq_terms (applySubTerms sigma1 trms1) (applySubTerms sigma2 trms2).
Proof.
  intros.
remember [r1; r2] as rules in H. remember [sigma1; sigma2] as sigmas in H.
 induction H. 
   + inversion Heqrules.
   + (* Sigma_Run_Step_P *) inversion Heqrules. inversion Heqsigmas. subst. assert (HA :=  H).
     apply OneOrNoOutputsFromOutStateSingle with (sigma:=sigma1) (rs:=[r2]) (f1:=f1) (l:= l) (f2:=f2) in HA; try assumption.
     inversion H0; inversion H5; subst.
     - (* oneInputXorOutput f1 *) 
       apply outputInRuleWillMatchRule with (rules := [r2]) (vars := trms1) (f1:=f1) (l:=l) (f2:=f2) in H; try assumption.
       eapply outputWillMatchFollowingInput.  apply H4.
       assumption. assumption. assumption.
     - (* noInputOrOutput f1 *) 
       eapply outputInRuleWillMatchRule with (rules := [r2]) (vars := trms1) (f1:=f1) (l:=l) (f2:=f2) in H; try assumption.
       eapply outputWillMatchFollowingInput.  apply H4.
       assumption. assumption. assumption.
  + (* Sigma_Run_Step_Silent_P *)
     inversion Heqrules. inversion Heqsigmas. subst. (* Sigma_Run_Step_P *) assert (HA :=  H).
     apply OneOrNoOutputsFromOutStateSingle with (sigma:=sigma1) (rs:=[r2]) (f1:=f1) (l:= emptyLabel) (f2:=f2) in HA; try assumption.
     inversion H0; inversion H5; subst.
     - (* oneInputXorOutput f1 *) 
       eapply outputInRuleWillMatchRule with (rules := [r2]) (vars := trms1) (f1:=f1) (l:=emptyLabel) (f2:=f2) in H; try assumption.
       eapply outputWillMatchFollowingInput.  apply H4.
       apply HA. assumption. assumption.
     - (* noInputOrOutput f1 *) 
       eapply outputInRuleWillMatchRule with (rules := [r2]) (vars := trms1) (f1:=f1) (l:=emptyLabel) (f2:=f2) in H; try assumption.
       eapply outputWillMatchFollowingInput.  apply H4.
       apply HA. assumption. assumption.
   + (* Sigma_Run_Comm_P *)
     apply IHrunInOrderSigmaProtocol; try assumption.
     unfold  wellformedRulesFromState. left.  inversion H0. inversion H4.
     - split; try assumption. simpl. split. apply removeOneOutputIn; assumption.
       apply removeOneOutputOut;  assumption.
     - inversion H4. apply noOutMeansNoOutSubList in H. inversion H. assumption.
Qed.



Axiom InputMatchesFactsProtocol : forall r1 r2 sigma1 sigma2 trms1 trms2 f1 trace f2 ,
  runInOrderSigmaProtocol [r1] [sigma1] f1 trace f2
    -> wellformedRulesFromState f1 [r1] 
      -> oneOutputXorInputIs f1 trms1 -> oneInputAndNoOutputIs (premiseFacts r2) (IN trms2)
        -> eq_terms trms1 (applySubTerms sigma2 trms2).


Fixpoint StateToStateRules (rs:list rule) : Prop :=
  match rs with 
    | [] => True
    | r::rs => StateToStateProtocolRule r /\ StateToStateRules rs
  end.


Fixpoint lastOutputNoInput (trms:terms) (rules:list rule) : Prop :=
match rules with
  | r::rs => (oneOutputAndNoInputIs  (conclFacts r) (OUT trms) /\ StateToStateRules rs)
                           \/ lastOutputNoInput trms rs
  | [] => False
 end.

Fixpoint lastOutputNoInputAndSigma (trms:terms) (sigma:substitution) (rules:list rule) (sigmas:substitutions) : Prop :=
match rules, sigmas with
  | r::rs, sig::sigs => (oneOutputAndNoInputIs  (conclFacts r) (OUT trms) /\ StateToStateRules rs /\ sig=sigma)
                           \/ lastOutputNoInputAndSigma trms sigma rs sigs
  | _,_ => False
 end.


Axiom lastOutputNoInputHasSigma: forall trms (rules:list rule) (f1:facts) rules sigmas f1 trace f2,
  lastOutputNoInput trms rules 
    ->  runInOrderSigmaProtocol rules sigmas f1 trace f2
      -> exists sigma, member sigma sigmas /\ lastOutputNoInputAndSigma trms sigma rules sigmas.


Axiom lastOutputNoInputStdRunHasSigma: forall trms (rlProto:list rule) (rlSetup:list rule) (f1:facts) rlProto rlSetup sigmas f1 trace f2,
  lastOutputNoInput trms rlProto 
    ->  runInOrderSigma rlProto rlSetup sigmas f1 trace f2
      -> exists sigma, member sigma sigmas /\ lastOutputNoInputAndSigma trms sigma rlProto sigmas.


Axiom wellformednessPreserved : forall f1 r rs sigma l f2,
  wellformedRulesFromState f1 (r :: rs)
    -> reduceWithGroundRule (applySubRule sigma r) f1 l f2
      -> wellformedRulesFromState f2 rs.

Axiom OutputInputUnchangedByStoSrule : forall f1 r sigma l f2 trms,
  reduceWithGroundRule (applySubRule sigma r) f1 l f2
    -> StateToStateProtocolRule r -> oneOutputXorInputIs f1 trms 
      -> oneOutputXorInputIs f2 trms.

Axiom OutXorInAndOutMeansNoIn : forall trms f1,
subList [OUT trms] f1 -> oneOutputXorInputIs f1 trms -> noInputs f1.

Axiom OneOutRemovedMeansNone : forall trms f1,
subList [OUT trms] f1 -> oneOutputXorInputIs f1 trms -> noOutputs (removeFacts [OUT trms] f1).


Axiom OnlyOneOutputInOxI : forall f1 trms1 trms2,
  oneOutputXorInputIs f1 trms1 -> subList [OUT trms2] f1 -> trms1=trms2.



Lemma OutputInputUnchangedByStoSrules : forall rules sigmas f1 trace f2 trms,
  runInOrderSigmaProtocol rules sigmas f1 trace f2
    -> wellformedRulesFromState f1 rules -> StateToStateRules rules
      -> oneOutputXorInputIs f1 trms -> oneOutputXorInputIs f2 trms.
Proof.
  intros. induction H.
    + assumption.
    + apply IHrunInOrderSigmaProtocol.
      - eapply wellformednessPreserved. apply H0. apply H3.
      - inversion H1. assumption.
      - eapply OutputInputUnchangedByStoSrule. apply H3. inversion H1. assumption. assumption.
    + apply IHrunInOrderSigmaProtocol.
      - eapply wellformednessPreserved. apply H0. apply H3.
      - inversion H1. assumption.
      - eapply OutputInputUnchangedByStoSrule. apply H3. inversion H1. assumption. assumption.
    + apply IHrunInOrderSigmaProtocol.
      -  assert (HA := H2). apply OnlyOneOutputInOxI with (trms2:=trm) in HA. subst.
         unfold wellformedRulesFromState. left. split.
        * unfold oneInputXorOutput. split.
          apply noInputsAcrossRemove. eapply OutXorInAndOutMeansNoIn. apply H. 
          apply H2. apply OneOutRemovedMeansNone; try assumption.
        * inversion H0. inversion H4. assumption. inversion H4. 
          apply noOutMeansNoOutSubList in H. inversion H. assumption.
        *  assumption.
     - destruct rlp. reflexivity. simpl in H1. inversion H1. assumption.
     - simpl.  assert (HA := H2). apply OnlyOneOutputInOxI with (trms2:=trm) in HA. rewrite HA. reflexivity. assumption.
Qed.


Axiom runInOrderSigmaProtocolTail: forall  r rules sigma sigmas f1 trace1 f3,
  runInOrderSigmaProtocol (r :: rules) (sigma :: sigmas) f1 trace1 f3
    -> wellformedRulesFromState f1 (r :: rules)
      -> exists f2 trace2 trace3, (runInOrderSigmaProtocol [r] [sigma] f1 trace2 f2
                              /\ runInOrderSigmaProtocol rules sigmas f2 trace3 f3
                                 /\ wellformedRulesFromState f2 rules).

Axiom wellformedHead : forall f1 r rules, 
  wellformedRulesFromState f1 (r :: rules) -> wellformedRulesFromState f1 [r].

Lemma lastOutputInFacts : forall rules sigmas f1 trace f2 trms sigma,
 runInOrderSigmaProtocol rules sigmas f1 trace f2
    -> wellformedRulesFromState f1 rules 
      -> lastOutputNoInputAndSigma trms sigma rules sigmas
        -> oneOutputXorInputIs f2 (applySubTerms sigma trms).
Proof.
  intros. generalize dependent sigmas. generalize dependent f1. generalize dependent trace0. induction rules; intros.
  + destruct sigmas eqn:E. inversion H1. inversion H1.
  + destruct sigmas eqn:E.
    - inversion H1.
    - subst. inversion H1.
      * inversion H2. inversion H4. subst.
        apply runInOrderSigmaProtocolTail in H; try assumption. inversion H. inversion H6. inversion H7. inversion H8. inversion H10.
        eapply OutputInputUnchangedByStoSrules. apply H11. assumption. assumption.
        apply oneOutAndNoInIsOneInOrOutIs .
        eapply OutputInRuleWillMatch. 
        apply H9. apply wellformedHead in H0. assumption. assumption.
      * apply runInOrderSigmaProtocolTail in H; try assumption. inversion H. inversion H3. inversion H4. inversion H5. inversion H7.
        eapply IHrules. apply H9. apply H8. assumption.
Qed. 




Lemma outputMatchesNextInputProtocol : forall rules sigmas f1 trace1 f2 ruleLast sigmaLast trace2 f3 trms1 trms2 outSigma,
  runInOrderSigmaProtocol rules sigmas f1 trace1 f2 
    -> runInOrderSigmaProtocol [ruleLast] [sigmaLast] f2 trace2 f3 
      -> wellformedRulesFromState f1 rules  -> wellformedRulesFromState f2 [ruleLast] 
        -> lastOutputNoInputAndSigma trms1 outSigma rules sigmas -> oneInputAndNoOutputIs (premiseFacts ruleLast) (IN trms2)
          -> eq_terms (applySubTerms outSigma trms1) (applySubTerms sigmaLast trms2).
Proof.
  intros.
  eapply lastOutputInFacts in H; try assumption.
  eapply InputMatchesFactsProtocol. apply H0. assumption.
  apply H. apply H4. assumption.
Qed.


(**=================================================================**)
(**Rajiv : Working on converting this for Std Run : Check the Axioms**)
(**==================================================================**)



Axiom OutputInRuleWillMatchStdRun : forall r rlSetup sigma f1 t f2 trms,
  runInOrderSigma [r] rlSetup [sigma] f1 t f2
    -> wellformedRulesFromState f1 [r]
      -> oneOutputAndNoInputIs (conclFacts r) (OUT trms)
        -> oneOutputAndNoInputIs f2 (OUT (applySubTerms sigma trms)). 

Axiom OutputInputUnchangedByStoSrulesStdRun : forall protocolRules setupRules sigmas f1 trace f2 trms,
  runInOrderSigma protocolRules setupRules sigmas f1 trace f2
    -> wellformedRulesFromState f1 protocolRules -> StateToStateRules protocolRules
      -> oneOutputXorInputIs f1 trms -> oneOutputXorInputIs f2 trms.



Axiom runInOrderSigmaTail: forall  r rlProto rlSetup sigma sigmas f1 trace1 f3,
  runInOrderSigma (r :: rlProto) rlSetup (sigma :: sigmas) f1 trace1 f3
    -> wellformedRulesFromState f1 (r :: rlProto)
      -> exists f2 trace2 trace3, (runInOrderSigma [r] rlSetup [sigma] f1 trace2 f2
                              /\ runInOrderSigma rlProto rlSetup sigmas f2 trace3 f3
                                 /\ wellformedRulesFromState f2 rlProto).


Lemma lastOutputInFactsStdRun : forall protocolRules setupRules sigmas f1 trace f2 trms sigma,
 runInOrderSigma  protocolRules setupRules sigmas f1 trace f2 
    -> wellformedRulesFromState f1 protocolRules 
      -> lastOutputNoInputAndSigma trms sigma protocolRules sigmas
        -> oneOutputXorInputIs f2 (applySubTerms sigma trms).
Proof.
  intros. generalize dependent sigmas. generalize dependent f1. generalize dependent trace0. induction protocolRules; intros.
  + destruct sigmas eqn:E. inversion H1. inversion H1.
  + destruct sigmas eqn:E.
    - inversion H1.
    - subst. inversion H1.
      * inversion H2. inversion H4. subst.
        apply runInOrderSigmaTail in H; try assumption. inversion H. inversion H6. inversion H7. inversion H8. inversion H10.
        eapply OutputInputUnchangedByStoSrulesStdRun. apply H11. assumption. assumption.
        apply oneOutAndNoInIsOneInOrOutIs .
        eapply OutputInRuleWillMatchStdRun. 
        apply H9. apply wellformedHead in H0. assumption. assumption.
      * apply runInOrderSigmaTail in H; try assumption. inversion H. inversion H3. inversion H4. inversion H5. inversion H7.
        eapply IHprotocolRules. apply H9. eapply H8. assumption.
Qed. 


Axiom InputMatchesFactsStdRun : forall r1 r2 setupRules sigma1 sigma2 trms1 trms2 f1 trace f2 ,
  runInOrderSigma [r1] setupRules [sigma1] f1 trace f2
    -> wellformedRulesFromState f1 [r1] 
      -> oneOutputXorInputIs f1 trms1 -> oneInputAndNoOutputIs (premiseFacts r2) (IN trms2)
        -> eq_terms trms1 (applySubTerms sigma2 trms2).


Lemma outputMatchesNextInputStdRun : forall protocolRules setupRules sigmas f1 trace1 f2 ruleLast sigmaLast trace2 f3 trms1 trms2 outSigma,
  runInOrderSigma  protocolRules setupRules sigmas f1 trace1 f2 
    -> runInOrderSigma [ruleLast] setupRules [sigmaLast] f2 trace2 f3 
      -> wellformedRulesFromState f1 protocolRules  -> wellformedRulesFromState f2 [ruleLast] 
        -> lastOutputNoInputAndSigma trms1 outSigma protocolRules sigmas -> oneInputAndNoOutputIs (premiseFacts ruleLast) (IN trms2)
          -> eq_terms (applySubTerms outSigma trms1) (applySubTerms sigmaLast trms2).
Proof.
  intros.
  eapply lastOutputInFactsStdRun in H; try assumption.
  eapply InputMatchesFactsStdRun. apply H0. assumption.
  eapply H. eapply H4. assumption.
Qed.
(*===============================================*) 


Definition variableDirectlyLinkedInputOutput (x:variable) (newRule:rule) (pastRules: list rule) : Prop :=
  exists trms1 trms2, (member (IN trms1) (premiseFacts newRule))
    /\ lastOutputNoInput trms2 pastRules 
    /\ baseTermAtSamePosTerms (Var x) trms1 trms2.


(**================================================**)
(**==Added new Axioms to prove the following Lemma *)
(**===================================================**)

Axiom equalTermsIfbaseTermAtSamePosFunc: forall sigma1 sigma2 trms1 trms2 f l x0,
baseTermAtSamePosTerms (Var x0) (Func f l :: trms2)
       trms1
-> eq_terms (applySubTerms sigma1 trms1)
      (applySubTerms sigma2 (Func f l :: trms2))
-> eq_terms (applySubTerms sigma1 trms1)
  (applySubTerms sigma2 trms2). 

Axiom baseTermAtSamePosTermsFunc: forall f l  x0 trms1 trms2,
baseTermAtSamePosTerms (Var x0) (Func f l :: trms2)
       trms1
->  baseTermAtSamePosTerms (Var x0) trms2 trms1.


Axiom equalTermsIfbaseTermAtSamePosBTerm: forall sigma1 sigma2 trms1 trms2 b x0,
baseTermAtSamePosTerms (Var x0) (Bterm b :: trms2)
       trms1
-> eq_terms (applySubTerms sigma1 trms1)
      (applySubTerms sigma2 (Bterm b :: trms2))
-> eq_terms (applySubTerms sigma1 trms1)
  (applySubTerms sigma2 trms2). 

Axiom baseTermAtSamePosTermsBTerm: forall b  x0 trms1 trms2,
baseTermAtSamePosTerms (Var x0) (Bterm b :: trms2)
       trms1
->  baseTermAtSamePosTerms (Var x0) trms2 trms1.

(* Rajiv : Added this  proof *)
Lemma equalTermsMeansEqualVars : forall trms1 sigma1 trms2 sigma2 x,
 eq_terms (applySubTerms sigma1 trms1) (applySubTerms sigma2 trms2)
-> baseTermAtSamePosTerms (Var x) trms2 trms1
 -> sigma1 x = sigma2 x.
Proof. 
  intros.  induction trms2. induction trms1.
    + simpl in H. simpl in H0. inversion H0.
    + destruct a.
      - simpl in H. apply IHtrms1. inversion H. inversion H0.
      - simpl in H. apply IHtrms1. inversion H. inversion H0.
    + destruct a.
      - simpl in H. apply IHtrms2. eapply equalTermsIfbaseTermAtSamePosFunc.
        apply H0. apply H. eapply baseTermAtSamePosTermsFunc. apply H0.
      - simpl in H. apply IHtrms2. eapply equalTermsIfbaseTermAtSamePosBTerm.
        apply H0. apply H. eapply baseTermAtSamePosTermsBTerm. apply H0.
Qed.



Axiom InputFactsEqualMeansEqualTerms: forall t1 t2,
  IN t1 = IN t2 -> t1 = t2.

Axiom oneInputInFactsMeansEqualTerms: forall fs t trms,
member (IN trms) fs ->  oneInput (IN t :: fs) -> t = trms.


Lemma InputInFactIsoneInput1 : forall fs trms,
  member (IN trms) fs -> oneInput fs -> noOutputs fs -> oneInputAndNoOutputIs fs (IN trms).
Proof.
  intros. induction fs.
    + inversion H.
    +  destruct a. 
      - simpl. split. simpl in H. destruct H.
        * inversion H. reflexivity.
        * eapply oneInputInFactsMeansEqualTerms. apply H. apply H0.
        * split. simpl in H0. auto. auto.
        - simpl. simpl in H1. auto. 
        - simpl. apply IHfs; simpl in H; simpl in H0; simpl in H1. destruct H. 
          inversion H. auto. auto. auto.
        - simpl. apply IHfs; simpl in H; simpl in H0; simpl in H1. destruct H. 
          inversion H. auto. auto. auto.
        - simpl. apply IHfs; simpl in H; simpl in H0; simpl in H1. destruct H. 
          inversion H. auto. auto. auto.
Qed. 


Axiom InputInFactIsoneInputAndNoOutput : forall fs,
  member (IN []) fs -> oneInput fs -> noOutputs fs -> oneInputAndNoOutputIs fs (IN []).


Axiom InputInFactIsoneInputAndNoOutputTerms : forall fs trms,
  member (IN trms) fs -> oneInput fs -> noOutputs fs -> oneInputAndNoOutputIs fs (IN trms).

Axiom InputInFactIsoneInput : forall fs,
  member (IN []) fs -> noOutputs fs -> oneInputIs fs (IN []).


Axiom inputAsMemberIsTheInput : forall f t,
    member (IN t) f -> oneInput f -> oneInputIs f (IN t).

Axiom InputToStateProtoRuleDoesNotAddOut: forall f1 l f2 trms,
member (IN trms) f1 -> InputToStateProtocolRule (RuleProto f1 l f2) -> oneInputAndNoOutputIs f1 (IN trms).


 
Axiom noInputsMeanNoInFacts : forall trms f,
  member (IN trms) f -> noInputs f -> False.


Lemma oneInputOnlyWellFormedRule : forall trms rule fs rs,
member (IN trms) (premiseFacts rule)
 -> wellformedRulesFromState fs (rule::rs)
 -> oneInputAndNoOutputIs (premiseFacts rule) (IN trms). 
Proof.
  intros. destruct rule0; simpl; simpl in H; 
  inversion H0; inversion H1; inversion H3; inversion H4; 
  try inversion H5; try inversion H6; try inversion H8; try inversion H9; try inversion H10.
  + apply InputInFactIsoneInput1; assumption.
  + apply noInputsMeanNoInFacts in H. inversion H. assumption.
  + apply InputInFactIsoneInput1; assumption.
  + apply noInputsMeanNoInFacts in H. inversion H. assumption.
  + apply noInputsMeanNoInFacts in H. inversion H. assumption.
Qed.




Lemma DirectlyLinkedInOutVarsMatchProtocolRules : forall rules sigmas f1 trace1 f2 ruleLast sigmaLast trace2 f3  x,
  runInOrderSigmaProtocol rules sigmas f1 trace1 f2 
    -> runInOrderSigmaProtocol [ruleLast] [sigmaLast] f2 trace2 f3 
      -> wellformedRulesFromState f1 rules  -> wellformedRulesFromState f2 [ruleLast] 
        -> variableDirectlyLinkedInputOutput x ruleLast rules
          -> exists sigma, member sigma sigmas /\  (sigma x) = (sigmaLast x).
Proof.
  intros. inversion H3. inversion H4 as [trms2]. inversion H5. inversion H7. 
  apply lastOutputNoInputHasSigma with (sigmas:=sigmas) (f2:=f1) (trace:=trace1) (f3:=f2) in H8; try assumption. 
  inversion H8 as [sigmaOut]. inversion H10.
  exists sigmaOut. split.
  - assumption.
  - apply equalTermsMeansEqualVars with (trms1:=trms2) (trms2:=x1) ; try assumption.
    apply outputMatchesNextInputProtocol with (ruleLast:=ruleLast) (sigmaLast:=sigmaLast) (trace2:=trace2) (f3:=f3) (trms1:=trms2) (trms2:=x1) (outSigma:=sigmaOut) in H; try assumption. 
    apply oneInputOnlyWellFormedRule with (fs:=f2) (rs:=[]) ; assumption.
Qed.


Lemma DirectlyLinkedInOutVarsMatchStdRun : forall rlProto rlSetup sigmas f1 trace1 f2 ruleLast sigmaLast trace2 f3  x,
  runInOrderSigma rlProto rlSetup sigmas f1 trace1 f2 
    -> runInOrderSigma [ruleLast] rlSetup [sigmaLast] f2 trace2 f3 
      -> wellformedRulesFromState f1 rlProto  -> wellformedRulesFromState f2 [ruleLast] 
        -> variableDirectlyLinkedInputOutput x ruleLast rlProto
          -> exists sigma, member sigma sigmas /\  (sigma x) = (sigmaLast x).
Proof.
  intros. inversion H3. inversion H4 as [trms2]. inversion H5. inversion H7. 
  eapply lastOutputNoInputStdRunHasSigma with (sigmas:=sigmas) (f2:=f1) (trace:=trace1) (f3:=f2) in H8; try assumption. 
  inversion H8 as [sigmaOut]. inversion H10.
  exists sigmaOut. split.
  - assumption.
  - apply equalTermsMeansEqualVars with (trms1:=trms2) (trms2:=x1) ; try assumption.
    apply outputMatchesNextInputStdRun with (ruleLast:=ruleLast) (sigmaLast:=sigmaLast) (trace2:=trace2) (f3:=f3) (trms1:=trms2) (trms2:=x1) (outSigma:=sigmaOut) in H; try assumption. 
    apply oneInputOnlyWellFormedRule with (fs:=f2) (rs:=[]) ; assumption.
  - apply H.
Qed.

(*===============================================*)

Fixpoint memberAtSamePos {T1:Type} {T2:Type} (e1:T1) (e2:T2) (list1: list T1) (list2: list T2) : Prop :=
  match list1 with
    | []      => False
    | h1::ts1 => match list2 with
                   | [] => False
                   | h2::ts2 => (e1=h1 /\ e2=h2) \/ memberAtSamePos e1 e2 ts1 ts2
                  end
   end.


Lemma factFromRule : forall fac (f1:facts) protocolRules  sigmas f1 t f2,
 runInOrderSigmaProtocol protocolRules sigmas f1 t f2 -> member fac f2 -> not(member fac f1)
      -> exists r sigma facTemplate, memberAtSamePos r sigma protocolRules sigmas  
             /\ member facTemplate (conclFacts r) /\ applySubFact sigma facTemplate = fac.

(*Proof.
  intros. induction H.
    - unfold not in H1.  apply H1 in H0. inversion H0.
    - exists r. exists sigmaNow. subst. rewrite <- H2 in H. inversion H. simpl.
*)


Lemma reverseHeadList : forall  (h:rule) (ts:list rule), exists listPart last, (h::ts) = appendAny listPart [last].
Proof. intros.
   induction (ts).
   + exists []. exists h. reflexivity.
   + inversion IHl. inversion H. destruct x0.
     - unfold appendAny in H0. inversion H0. exists [x1].  exists a. reflexivity.
     - exists (r::a::x0). exists x1.  simpl.  inversion H0. reflexivity.
Qed.


Lemma appendAnyAppendAny: forall {T:Type} (x1:T) x0 r,
(appendAny (appendAny x0 [x1]) [r]) = (appendAny x0 [x1;r]).
Proof.
  intros. induction x0. reflexivity. simpl. rewrite IHx0. reflexivity.
Qed.


(* This are our new definitions from our paper*)

(* Defining allowed sequences *)

(* This is definition of Allowed Sequences from the paper *)
Inductive Def2_1_Valid_AllowSequences : (list ruleList) -> ruleList -> Prop := 
  | Empty_AS : forall rs, Def2_1_Valid_AllowSequences [] rs
  | Step_AllowSeq : forall rl rlsHead rlsTail, 
              orderedSubList rlsHead rl /\ Def2_1_Valid_AllowSequences rlsTail rl
                              -> Def2_1_Valid_AllowSequences (rlsHead::rlsTail) rl.

(* A useful lemma, tells us we can extend the rulelist without problems: *)
Lemma canExtendAllowSeq : forall rl rls r, Def2_1_Valid_AllowSequences rls rl 
                                                   -> Def2_1_Valid_AllowSequences rls (r::rl).
Proof.
  intros. induction rls. 
  - apply Empty_AS.
  - apply Step_AllowSeq. inversion H. inversion H3. split.  
     + destruct a. apply Empty_O_SubList. apply Next_O_SubList. assumption.
     + apply IHrls. assumption.
Qed.


(* As examples of allowed sequences, we may use the list itself, all prefixes of the list. 
   We now prove that these are Allowed Sequences *)
Lemma idIsAllowSeq : forall rl, Def2_1_Valid_AllowSequences [rl] rl.
Proof.
  intros. apply Step_AllowSeq. split. induction rl. apply Empty_O_SubList. apply Same_O_SubList. assumption.
  apply Empty_AS.
Qed.

Fixpoint allPrefixs (rl:ruleList) : list ruleList := 
  match rl with
    | [] => []
    | h::ts => (h::ts):: (allPrefixs ts)
  end.

Lemma prefixIsAllowSeq : forall rl:ruleList, Def2_1_Valid_AllowSequences (allPrefixs rl) rl.
Proof.
  induction rl.
  + apply Empty_AS.
  + simpl. apply Step_AllowSeq. split. 
    - apply idIsOrderedSublist. 
    - apply canExtendAllowSeq. assumption.
Qed.


(* All list of rule lists are an allowed Sequence for some rulelist. Therefore we may just consider an
   arbitary list of rulelists in the following definitions *)

Lemma allListsAllowedSeq : forall rll:(list ruleList), exists rl:ruleList, Def2_1_Valid_AllowSequences rll rl.
Proof.
  induction rll.
  + exists []. apply Empty_AS.
  + inversion IHrll. exists (appendAny a x0). apply Step_AllowSeq. split.
    - induction a. apply Empty_O_SubList. apply Same_O_SubList. apply IHa.
    - induction a. assumption. apply canExtendAllowSeq. assumption. 
Qed. 


Lemma ginstSplit : forall rl1 rl2 r, ginsts r rl2 -> ginsts r (appendAny rl1 rl2).
Proof.
  intros.
  induction rl1.
  + simpl. assumption.
  + simpl. apply GinstTail. assumption.
Qed.

Inductive Def_Standard_Trace : list ruleList -> ruleList -> substitutions-> trace -> Prop := 
  | StandRun_Head : forall rl rls t f2 setupRules sigmas, (runInOrderSigma rl setupRules sigmas [] t f2 ) -> Def_Standard_Trace (rl::rls) setupRules sigmas t
  | StandRun_Tail : forall rl rls t setupRules sigmas, Def_Standard_Trace rls setupRules sigmas t -> Def_Standard_Trace (rl::rls) setupRules sigmas t.


(*True implies a standard trace as per Def 3.1  
If the first rule rl (with empty facts) is in order and generating trace 't', then every rulelist with rl as head will also generate 't' as a standard trace.
Similarly,
If a rullist rls generates a standard trace 't', then every rulelist such as (rl::rls) will also generate 't' as a standard trace.
*)

Definition Def5_7_Standard_Trace(allowSeq:list ruleList) (setupRules: ruleList) (sigmas : substitutions) (thisTr:trace) : Prop :=
                      (Def_Standard_Trace allowSeq setupRules sigmas thisTr).


Inductive Subset_of_Standard_Traces : list ruleList -> ruleList -> substitutions -> list trace -> Prop := 
  | StandTraces_Empty : forall rlp setupRules sigmas, Subset_of_Standard_Traces rlp setupRules sigmas []
  | StandTraces_Next  : forall rlp setupRules t ts sigmas, Def5_7_Standard_Trace rlp setupRules sigmas t /\ Subset_of_Standard_Traces rlp setupRules sigmas ts -> Subset_of_Standard_Traces rlp setupRules sigmas (t::ts).

Inductive mergeTrace : trace -> trace -> trace -> Prop :=
  | PMerge_nil : mergeTrace [] [] []
  | PMerge_left : forall x l l1 l2 , mergeTrace l1 l2 l -> mergeTrace (x::l1) l2 (x::l)
  | PMerge_right : forall x l l1 l2, mergeTrace l1 l2 l -> mergeTrace l1 (x::l2) (x::l).


Inductive merge : list trace -> trace -> Prop :=
  | PMerge_Base  : forall lstTR TR, In TR lstTR -> merge lstTR TR
  | PMerge_Step  : forall lst1 tr1 tr2 trnew, (merge lst1 tr1 /\ In tr2 lst1 /\ mergeTrace tr1 tr2 trnew) 
                                                                              ->  merge lst1 trnew.

Fixpoint applySubRuleListWise (sigmas : list substitution) (rl:ruleList) : ruleList := 
match sigmas, rl with
  | sig1::sigs, r1::rs  => (applySubRule sig1 r1)::(applySubRuleListWise sigs rs)
  | _, _              => []
end.


Fixpoint Def5_5_freshInRL (rl: ruleList) : list freshNameProto := 
  match rl with
    | [] => []
    | rl1::rls => appendAny (getFrNamesPremise (getFrFactProtoRule rl1)) (Def5_5_freshInRL rls)
  end.



Definition Def5_6_FreshFromRL_In_Trace (sigmas:substitutions) (rl:ruleList) (tr: trace) : list freshNameProto  := 
          commonFreshNames (Def5_5_freshInRL (applySubRuleListWise sigmas rl)) (getFreshProtoNamesinTrace tr).



Definition  ConditionOnFreshNames (sigmas:substitutions) (allowSeq:list ruleList) (logFromTraces:list trace) : Prop := 
forall tr_i tr_j rl_i rl_j, noCommonElements (Def5_6_FreshFromRL_In_Trace sigmas rl_i tr_i) 
                                              (Def5_6_FreshFromRL_In_Trace sigmas rl_j tr_j)
                                     /\ (member rl_i allowSeq) 
                                      /\ (member rl_j allowSeq)
                                       /\ (member tr_i logFromTraces) 
                                         /\ (member tr_j logFromTraces)
                                          /\ not (eq tr_i tr_j).


Definition Def5_7_Standard_Looking_Trace  (allowSeq:list ruleList) (setupRules:ruleList) (testTrace:trace) : Prop :=
 exists sigmas sometraces, (Subset_of_Standard_Traces allowSeq setupRules sigmas sometraces) 
                       /\ (merge (map getLogTrace sometraces) (getLogTrace testTrace))
                         /\ ConditionOnFreshNames sigmas allowSeq  (map getLogTrace sometraces).  

Definition Def5_8_Attack_Trace (attackTrace:trace) : Prop := True.

Definition Def5_9_Stealth_Attack (allowSeq:list ruleList) (setupRules:ruleList) (testTrace:trace) : Prop :=
            Def5_7_Standard_Looking_Trace allowSeq setupRules testTrace /\  Def5_8_Attack_Trace testTrace.


(** ============================================ 
  *** 9: Definitions from Chapter 6 of the thesis
 =============================================== **)

Definition StdTemplateForRuleList : ruleList -> trace :=  getLogRL.


Definition Def_StdTemplates : (list ruleList) -> (list trace) := map getLogRL.

Definition Def6_10_StdTemplate (allowSeq:list ruleList) (thisTemp:trace) : Prop :=
                   (In thisTemp (Def_StdTemplates allowSeq)).

(* DO WE NEED THE TRACE TO BE GROUNDED???? Tom *)
Fixpoint StdTracesfromTemplates (sigma:substitution) (allowSeq: list ruleList) : list trace :=
         applySubTraces sigma (Def_StdTemplates  allowSeq). 

Definition StdTracefromTemplate (sigma:substitution) (allRules:list ruleList) (thisTrace:trace) : Prop :=
           (In thisTrace (StdTracesfromTemplates sigma allRules)).

Definition SID : baseTerm := (Var "sid").

(* "updateLabel l1" adds session ID 'sid' to front of action label parameters in every logged label. *)

Fixpoint updateLabel (l1 : label ) : label :=
  match l1 with
    | (LoggedSIDLabel t al lb)  => (LoggedSIDLabel t al lb)
    | (LoggedLabel al lb)       => (LoggedSIDLabel SID al lb) 
    | (BasicLabel als)          => (BasicLabel als)
  end.

(** While annotating rules, annotation of first rule modifies all three parts of 
   a rule while with other rules only the premise and labels are modified
 *)

Fixpoint annotateFirstRule (firstRule : rule) : rule :=
  match firstRule with
  |  RuleProto f1 lbl f2  => RuleProto (FR_P SID::f1) (updateLabel lbl) ((OUT [Bterm SID])::f2)
  |  RuleSetup f1 lbl f2  => RuleSetup f1 lbl f2
  end.

Fixpoint annotateOtherRules (rl : ruleList) : ruleList :=
  match rl with
  | (RuleSetup f1 lbl f2)::rls    => (RuleSetup f1 lbl f2) :: (annotateOtherRules rls)
  | (RuleProto  ppat lbl cpat)::t => (RuleProto ((IN [(Bterm SID)])::ppat)
                                               (updateLabel lbl) ((OUT [(Bterm SID)])::cpat))::(annotateOtherRules t)
  | []                            => []
  end.

(** "annotateRules rl " add the session IDs to the ruleList rl **)

Fixpoint annotateRules (rl : ruleList) : ruleList :=
  match rl with
  | [] => []
  |  r::t => (annotateFirstRule r) ::(annotateOtherRules t)
  end.

Definition AddSID :(list ruleList) -> (list ruleList) := map annotateRules.

Definition Def6_11_SessionsRL (allowSeq:list ruleList) : (list trace) := 
           Def_StdTemplates (AddSID allowSeq).

Definition Def6_12_StdSessionTemplate (allowSeq:list ruleList) (thisTemp:trace) : Prop :=
                   (In thisTemp (Def6_11_SessionsRL allowSeq)).

Fixpoint subTrace_genFrom_Template (sigma:substitution) (tr:trace) (StdTmp:trace) : Prop  :=
  match tr, StdTmp with
  | [],[] => True
  | t1::ts, o1::os  => eq_label t1 (applySubLabel sigma o1)
                       /\
                       (subTrace_genFrom_Template sigma ts os)
  | _,_  =>  False
  end.

(** Remove the session IDs from a trace **)

Fixpoint RemoveSIDfromLabel (l1 : label) : label :=
  match l1 with
    | (LoggedSIDLabel t al lb)  => (LoggedLabel al lb)
    | (LoggedLabel al lb)       => (LoggedLabel al lb)
    | (BasicLabel als)          => (BasicLabel als)
  end.

Definition RemoveSID : trace -> trace := map RemoveSIDfromLabel.
(** "sameSID t1 t2" verifies if terms "t1" and "t2" contain the same SID **)

Fixpoint sameSID (tm1:terms) (tm2:terms): Prop :=
  match tm1, tm2 with
     | sid1::pars1, sid2::pars2 =>  eq_term sid1 sid2
     | _,_                      =>  False
  end.


(** "al_Only_OnceNMAL al Tstd" verifies if every "al"  present
            in template "tm", is present only once.**)

Fixpoint al_Only_OnceNMAL (al:actionLabel) (Tstd:trace) : Prop :=
 match Tstd with
    |  nil  => False
    |  lbl1:: lbls => ((inLabelwithName al lbl1) /\ not (ALinTemplatewithName al lbls)) 
                      \/ 
                      (not (inLabelwithName al lbl1) /\ al_Only_OnceNMAL al lbls)
  end.

(** "everyLogUniqueinTemplate Tstd" holds only if every "al"  present
in template is present only once.**)

Definition  everyLogUniqueinTemplate (Tstd:trace) : Prop :=
  forall al, (al_in_Trace al Tstd) ->
                    al_Only_OnceNMAL al Tstd.

(* "WellFormedTemplate Tstd " verifies that there are no repeated log names in any of the templates *)
Fixpoint  WellFormedTemplate (Tstd:list trace) : Prop:=
  match Tstd with
  | tm1::tmRestList  =>  (everyLogUniqueinTemplate tm1)
                          /\
                         (WellFormedTemplate tmRestList)
  | []              =>  True
  end.

Lemma emptyLabelsLemma : forall sigma l, applySubLabel sigma l = emptyLabel -> l = emptyLabel.
Proof.
  intros. destruct l; inversion H; destruct l.
  - reflexivity.
  - inversion H1.
Qed. 

Lemma emptyReduceGround : forall r f1 f2, reduceWithGroundRule r f1 emptyLabel f2 
                                    -> (labelR r) = emptyLabel.
Proof.
  intros. destruct r.
  + inversion H. reflexivity.
  + inversion H. reflexivity.
Qed.

Lemma emptyReduce : forall r f1 f2, reduceWithRule r f1 emptyLabel f2 
                                    -> (labelR r) = emptyLabel.
Proof.
  intros. destruct r.
  + simpl. inversion H. inversion H0. 
    inversion H1. subst. inversion H3. inversion H4.  unfold applySubRule in H6.
    inversion H2. rewrite H7. rewrite <- H6 in H7. simpl in H7. destruct l. 
    apply emptyLabelsLemma in H7. rewrite H7. reflexivity.
    inversion H7. inversion H7.
  + simpl. inversion H. inversion H0. 
    inversion H1. subst. inversion H3. inversion H4.  unfold applySubRule in H6.
    inversion H2. rewrite H7. rewrite <- H6 in H7. simpl in H7. destruct l. 
    apply emptyLabelsLemma in H7. rewrite H7. reflexivity.
    inversion H7. inversion H7.
Qed.

Lemma LoggedLabelGroundReduce : forall r f1 f2 lg1 l1, reduceWithGroundRule r f1 (LoggedLabel lg1 l1) f2 
                                    -> exists lg2 l2, (labelR r) = (LoggedLabel lg2 l2).
Proof.
  intros. destruct r; inversion H; subst; exists lg1; exists l1; reflexivity.
Qed.

Lemma LoggedSIDLabelGroundReduce : forall r f1 f2 lg1 l1 t, reduceWithGroundRule r f1 (LoggedSIDLabel t lg1 l1) f2 
                                    -> exists lg2 l2 t, (labelR r) = (LoggedSIDLabel t lg2 l2).
Proof.
  intros. destruct r; inversion H; subst; exists lg1; exists l1; exists t; reflexivity.
Qed.

Lemma LoggedLabelReduce : forall r f1 f2 lg1 l1, reduceWithRule r f1 (LoggedLabel lg1 l1) f2 
                                    -> exists lg2 l2, (labelR r) = (LoggedLabel lg2 l2).
Proof.
  intros. destruct r.
  + simpl. inversion H. inversion H0. apply LoggedLabelGroundReduce in H2.
    inversion H2. inversion H3. inversion H1. subst. inversion H5. inversion H6.
    destruct l. 
   - subst. simpl in H4. inversion H4.
   - exists a. exists l. reflexivity.
   - subst. simpl in H4. inversion H4.
  + simpl. inversion H. inversion H0. apply LoggedLabelGroundReduce in H2.
    inversion H2. inversion H3. inversion H1. subst. inversion H5. inversion H6.
    destruct l. 
   - subst. simpl in H4. inversion H4.
   - exists a. exists l. reflexivity.
   - subst. simpl in H4. inversion H4.
Qed.

Lemma emptyLabelSigmaEq : forall sigma l, ((applySubLabel sigma  l) = emptyLabel) -> (l = emptyLabel).
Proof.
  intros. destruct l; unfold applySubLabel in H; inversion H.
  destruct l. 
    - reflexivity.
    - inversion H1.
Qed.

Lemma setupRulesBasicLabels : forall rls f1 l f2, 
wellFormedSetupRules rls -> reduceWithRules rls f1 l f2 -> exists al, l = BasicLabel al.
Proof.
  intros. inversion H0. inversion H1. induction H2. destruct l.
   - exists l. reflexivity.
   -  apply LoggedLabelGroundReduce in H3. inversion H3. inversion H4. inversion H2. subst.
      inversion H6. inversion H7. destruct r2; destruct r1.
     + simpl in H9. inversion H9. simpl in H5. rewrite H5 in H12. destruct l0.
       * inversion H12.
       * inversion H. inversion H10. inversion H15. inversion H18.
       * inversion H12.
     + inversion H9.
     + inversion H9.
     + simpl in H9. inversion H9. simpl in H5. rewrite H5 in H12. destruct l0.
       * inversion H12.
       * inversion H. inversion H10.
       * inversion H12.
   - apply LoggedSIDLabelGroundReduce in H3. inversion H3. inversion H4. inversion H5.
     inversion H2. subst. inversion H7. inversion H8.
        destruct r1; destruct r2.
     + simpl in H6. simpl in H10. inversion H10. rewrite H6 in H13. destruct l1.
       * inversion H13.
       * inversion H13.
       * inversion H.  inversion H11. inversion H16. inversion H19.
     + inversion H10.
     + inversion H10.
     + simpl in H6. simpl in H10. inversion H10. rewrite H6 in H13. destruct l1.
       * inversion H13.
       * inversion H13.
       * inversion H. inversion H11.
   - apply wellFormedTail in H. apply IHginsts in H.
     + assumption.
     + unfold reduceWithRules. exists r1. split. assumption. assumption.
     + split; assumption.
     + assumption.
Qed.

Lemma StdTracesHaveTemplates : forall t allowSequence sigma setupRules f1 f2,
        wellFormedSetupRules setupRules 
          -> runInOrder allowSequence setupRules sigma f1 t f2 
            -> (getLogTrace t) =
                       (applySubTrace sigma (StdTemplateForRuleList allowSequence)).
Proof.
  intros.
  induction H0; intros.
  + (* Run_Stop_O *) reflexivity. 
  + (* Run_Step_O *) apply IHrunInOrder in H. clear IHrunInOrder. 

    inversion_clear H0. destruct r; destruct l0; simpl; try assumption.
    - apply listEqHead. assumption.
    - apply listEqHead. assumption.
  + (* Run_Step_Silent_O *) apply IHrunInOrder in H. clear IHrunInOrder.
    apply emptyReduceGround in H0. destruct r; simpl in H0; apply emptyLabelSigmaEq in H0; subst; assumption.
  + (* Run_FreshStep_O *) apply IHrunInOrder in H. assumption.
  + (* Run_Step_S *)  destruct l. 
    - simpl. apply IHrunInOrder in H. assumption.
    - apply setupRulesBasicLabels with (f1:=f1) (l:=LoggedLabel a l) (f2:=f2) in H. 
       * inversion H. inversion H2.
       * assumption.
    - apply setupRulesBasicLabels with (f1:=f1) (l:=LoggedSIDLabel b a l) (f2:=f2) in H. 
       * inversion H. inversion H2.
       * assumption.
   + (* Run_Step_Silent_S *) apply IHrunInOrder. assumption.
   + (* Run_FreshStep_S *) apply IHrunInOrder. assumption.
   + (* Run_Comm_O *) apply IHrunInOrder in H. assumption.
Qed.

 
(**=======================================================
**** 10: Definitions and Proofs from Chapter 6 and 7
==========================================================**)

(* 

Setup rules only produce single unique state facts or non unique facts that have unique parameters (or outputs which we ignore). 

    Setup Rule facts :
                * All Non unique facts must have a unique construction, unique for a principal name

    Definition of a Step in a Path :
                * A step exists if :
                   - from a variable that appears in a particular position in an input to the same position in the previous output 
                   - from a variable that appears in a position in a unique state fact to the a variable in same position in a previous occurence of that unique fact.
                   - from a variable in any fact in a rule to the same variable to another fact in that rule.

    A path is zero or more steps.
*)


(*
    New validity conditions for a variable in Protocol ruleList :
    A variable in a protocol ruleList is valid, if this variable x
                * is a new variable in any rule.
                * while appearing in a unique state has a path from this variable back to a constant or a variable and
                  a previous path for another occurence of this variable also leads to the same constant or a variable.
                * while appearing in a non unique state fact F, it is paired with another variable that has a path to a value v then
                  there exists a previous non unique state fact F which has variable in the same position as x which also has a path to v, 
                  and is paired with a variable of the same name. 
 *)


(* Handling Public and Private keys in a model 
 A Public key has two different nomenclatures in a Tamarin file :
!Pk($A, pk(~ltkA))
and
!Pk($A, pkA)


For their equivalence, we can add a restriction stating 
Given !Pk(X, pk(ltkX)) AND !Pk(Y, pkY)

EQ(X,Y) -> EQ(PkX,pkY)

i.e.
Given
STATE PkFact [B; Func PkName [ltkB_var]] and STATE PkFact [B; pkB]
EQ(Func PkName [ltkB_var], pkB) is true


It flows from the fact that the setup rules generate a fresh key for each Principal which is unique


Any rule can consist of one of the following facts :
* Fresh fact -
         Fr() is for new variable so it is always valid. Fr() is not allowed more to exist
          more than once for any variable i.e. Each instance of Fr() must use a new variable.
* Input/Output fact - 
        Any input via In() is required to match all the varibales used herein 
        with the variables used in previous output Out(). Variables are matched by position 
        and in the case of different names, they are treated as equal.

* Unique state fact (appears only once)
         - Appears in pair at conclusion of previous rule and premise of the current rule.
          Every variable and their corresponding positions are matched.

* Non-unique state fact (appears multiple times but uniquely for a Principal)
          - such as "STATE PkFact [B; Func PkName [ltkB_var]]"
            and "STATE PkFact [B; pkB]" are matched based on their 
            occurrence in  the outputs and inputs.
            Values such as "Func PkName [ltkB_var]" and "pkB"
            are considered same if there exists a set of output and input
             that is supposed to match on account of them being equal.
                      e.g. If   "aenc{'1', ~ni, $I}pkR"  and  "aenc{'1', ni, I}pk(ltkR)" 
                          appear in output and inputrespectively

                            =>
                            "pkR" and "pk(ltkR)" are equal.
*)


(**=================================================
  10A: Types of Facts allowed in the system
  ================================================== *)

(* We define a uniqueStateFact as one that is only product in one rule. 
   This is useful to us because if a fact is uniquely produced then we 
   can be sure that every rule that uses this fact as an input will get 
   the same values *)


Fixpoint uniqueStateFact (f:fact) (rl:list rule) : Prop :=
  match rl, f with
    | r::rlt, STATE n ts =>    ( stateAppearsOnce f (conclFacts r) /\ NameDoesNotAppearInFacts n (allConclFacts rlt) )
                            \/ ( NameDoesNotAppearInFacts n (conclFacts r) /\ uniqueStateFact f rlt )
    | _ , _              => False
  end.

(* This requires that the unique fact is used with all vars the same, however this could 
   be weaken to only requiring that variable in question is the same *)

Fixpoint variableInUniqueStateFact (v:variable) (newRule:rule) (pastRules: list rule) : Prop := 
  exists n ts, (uniqueStateFact (STATE n ts) pastRules) /\ (member (STATE n ts) (premiseFacts newRule))
                    /\  member v (variablesInTerms ts).



(* We also define a uniqueArugmentsFact as one that can be product in many places
    but always has different arguments. Often this will be for setting up principals key
    e.g. Fact('C', key).

    For two occurences of such a fact, if we can show that if one of the argument terms 
    match then we can conclude that the other terms must *)



(* A term in OK as a unique state argument if it is fresh, or if it is a constant that 
   no other states with a the same name use *)
Fixpoint uniqueTermsForRule (ts:terms) (n:name) (r:rule) (rs:list rule) : Prop :=
  match ts with
    | []      => True
    | th::tst => ( termIsOnlyConstant th n rs \/ termIsFresh th r ) /\ (uniqueTermsForRule tst n r rs)
  end.

(* Constant must also not appear in other places*)
Fixpoint uniqueArgumentsFact (f:fact) (r: rule) (rs:list rule) : Prop :=
  match f with 
   | STATE n ts => (uniqueTermsForRule ts n r rs)
   | _ => False
  end.
(*Rajiv:How to model UAF_gen and UAF_used?*)

Fixpoint collectUniqueStateFacts (fls:facts) (rlst:ruleList) : facts :=
  match fls  with
  | f1::fs  =>  match (uniqueStateFact f1 rlst) with 
                | True  => (f1 :: (collectUniqueStateFacts fs rlst)) 
                end
  | []        => []
  end.


Fixpoint collectUniqueArgFacts (fls:facts) (r:rule) (rls:ruleList) : facts :=
  match fls  with
  | f1::fs  =>  match (uniqueArgumentsFact f1 r rls) with 
                | True  => (f1 :: (collectUniqueArgFacts fs r rls)) 
                end
  | []        => []
  end.

Fixpoint   PresentInSamePositionUniqueStateFact (RL:list rule) (t1:term) (t2:term) : Prop :=
    CheckFactsInUSF (collectUniqueStateFacts (collectStateFacts RL) RL) t1 t2.
  


Fixpoint   PresentInSamePositionUAF (RL:list rule) (t1:term) (t2:term) : Prop := 
  match RL with
  | r::rs =>   ((CheckFactsInUAF (collectUniqueArgFacts (collectStateFacts RL) r rs) t1 t2)
                  /\
                    PresentInSamePositionUAF rs t1 t2)
  | []    =>  True
  end.


(* TOM: This is an update to the model that allows any number of steps between 
        an input and an output for variables linked by input and outputs *)
Fixpoint varMatchInLastOutput (x:variable) (ts:terms) (revRules: list rule) : Prop := 
  match revRules with
    | [] => False
    | r::rs => member (OUT ts) (conclFacts r) 
                 \/ ((noOutputRule r) /\ varMatchInLastOutput x ts rs)
   end.

Fixpoint variableLinkedInputOutput (x:variable) (newRule:rule) (pastRules: list rule) : Prop :=
  exists ts, (member (IN ts) (premiseFacts newRule)) 
    /\ varMatchInLastOutput x ts (rev pastRules).




Definition Def6_4_allowedFactType (f:fact) (r: rule) (rs:list rule) : Prop :=
  (exists t, (member (FR_P t) (premiseFacts r)) /\ (eq_fact f (FR_P t)))
    \/
     (exists ts, (member (IN ts) (premiseFacts r) /\ (eq_fact f (IN ts))
        \/
           (member (OUT ts) (conclFacts r)) /\  (eq_fact f (OUT ts)))) 
             \/
               (uniqueStateFact f (r::rs)) 
                 \/ 
                   (uniqueArgumentsFact f r rs).


Definition Def6_5_variableDirectlyLinked (var: variable) (newRule:rule) (pastRules: list rule) : Prop :=
   (variableLinkedInputOutput var newRule pastRules) 
       \/ (variableInUniqueStateFact var newRule pastRules).


Fixpoint Def6_6_variableIndirectlyLinked (v:variable) (newRule:rule) (pastRules: list rule) : Prop := 
  exists n ts, uniqueArgumentsFact (STATE n ts) newRule pastRules 
                /\ member (STATE n ts) (premiseFacts newRule)
                  /\ (exists RuleA, member (STATE n ts) (conclFacts RuleA) /\ (member RuleA pastRules))
                   /\ member  v (variablesInTerms ts)
                      /\ (exists t, member  t (variablesInTerms ts) 
                              /\ Def6_5_variableDirectlyLinked t newRule pastRules)
                                /\ (exists c, member  c (constantsInTerms ts)).



Definition variableIsNew (var:variable) (pastRules: list rule) : Prop := 
   trueForAll (fun x => (NotIn var (variablesInRule x))) pastRules.

Definition Def6_7_validVariable  (newRule:rule) (pastRules: list rule) (var: variable) : Prop :=
   (variableIsNew var pastRules) \/ (Def6_5_variableDirectlyLinked var newRule pastRules)
        \/ (Def6_6_variableIndirectlyLinked var newRule pastRules).


Fixpoint Def6_7_validVariables (newRule:rule) (pastRules: list rule) (vs:variables) : Prop :=
  trueForAll (Def6_7_validVariable newRule pastRules) vs.


Definition Def6_8_validRule (newRule:rule) (pastRules: list rule): Prop :=
    (forall f, (member f (allFactsRL (appendAny pastRules [newRule])))
               /\ (Def6_4_allowedFactType f newRule pastRules))
                  /\ (forall vs, trueForAll (Def6_7_validVariable newRule pastRules) vs).



Fixpoint Def6_9_validRuleList (rs : list rule) : Prop :=
  match rs with
    | [] => True
    | r::rst => (Def6_9_validRuleList rst) /\ (Def6_7_validVariables r rst (variablesInRule r))
  end.


Fixpoint Def6_9_validRuleLists (allowSeq : list ruleList) : Prop := trueForAll Def6_9_validRuleList allowSeq.


(* Proposition 1 Given a valid rule list  RL=[R1,..,R_j]  and 
a normal run of the protocol with rules  using  sigma_1, .., sigma_j  as substitutions
for the reductions in each step of the run. If the variable  v  is directly linked 
as per Def6_5_variableDirectlyLinked in the rule  R_j  w.r.t.  [R_1,..,R_{j-1}]  
then either  v  does not appear in    [R_1,..,R_{j-1}]  
or "there exists some  sigma_i  such that   sigma_i(v)=sigma_j(v)  and  not (i=j)"
i.e., sigma_j is the last element and sigma_i is present in the list of sigmas anywhere but at the end.
*)


Lemma Prop1_DirectlyLinkedVariablesHaveSameValues : forall fs1 fs2 sigma_j tr v r rlProto rlSetup SigmaList,
        ((Def6_9_validRuleList (appendAny rlProto [r]) 
              /\ runInOrderSigma (appendAny rlProto [r]) rlSetup (appendAny SigmaList [sigma_j]) fs1 tr fs2))                               

          -> ((Def6_5_variableDirectlyLinked v r rlProto)
                ->     (variableIsNew v rlProto)  
                        \/                   
                         (exists sigma_i, (eq_name (sigma_i v) (sigma_j v))  
                                   /\ ((member sigma_i SigmaList)))
                          ).
(* 
Proof.
  intros.
  inversion H0.
  - destruct rlProto. 
    + inversion H1.
    + destruct reverseHeadList with (h:=r0) (ts:=rlProto). inversion H2.
      rewrite H3. unfold variableInInputAndOutput in H1.
      inversion H1. inversion H4. inversion H5. inversion H7.
      right. exists ( lastElement subs_empty  SigmaList). split.
      * apply termsEqDiffSigma with (trms1:=x2) (trms2:=x3). split. 
        eapply outputMatchesNextInputEnd with (rulesList := x0). inversion H. rewrite H3 in H11. 
        rewrite appendAnyAppendAny in H11. apply H11.
       unfold appendAny in H11.  apply H11.   
  
 *)

(* Proposition 2 Given a valid rule list  RL=[R_1,..,R_j]  and 
a normal run of the protocol with rules  


using  sigma_1, .., sigma_j  as substitutions
for the reductions in each step of the run. If the variable  v  is directly linked 
as per Def6_6_variableIndirectlyLinked in the rule  R_j  w.r.t.  [R_1,..,R_{j-1}]  
then either  v  does not appear in    [R_1,..,R_{j-1}]  
or there exists some  sigma_i such that  sigma_i(v)=sigma_j(v) and not (i=j). 
*)


Lemma Prop2_IndirectlyLinkedVariablesHaveSameValues : forall fs1 fs2 sigma_j tr v r rlProto rlSetup SigmaList,
        ((Def6_9_validRuleList (appendAny rlProto [r]) 
              /\ runInOrderSigma (appendAny rlProto [r]) rlSetup (appendAny SigmaList [sigma_j]) fs1 tr fs2))                               
          -> ((Def6_6_variableIndirectlyLinked v r rlProto)
                ->     (variableIsNew v rlProto)  
                        \/                   
                         (exists sigma_i, (eq_name (sigma_i v) (sigma_j v))  
                                   /\ ((member sigma_i SigmaList)))
                          ).


(* Proposition 3 Given a valid rule list RL and a normal run of the protocol let
sigma_1,..sigma_n be the substitutions used for the reductions in each step of the run, then
there exists a substitution sigma such for all sigma_i and v in domain(sigma_i); 
sigma(v) = sigma_i(v).*)

Lemma Prop3_AllSigmasCanBeReplacedbyASingleSigma : forall fs1 fs2 tr r rlProto rlSetup SigmaList,
        (Def6_9_validRuleList (appendAny rlProto [r]) 
               /\  runInOrderSigma (appendAny rlProto [r]) rlSetup SigmaList fs1 tr fs2)
                   -> (exists sigma, forall v sigma_i, (Def6_7_validVariable r rlProto v) 
                          /\ (member sigma_i SigmaList)
                        ->   (eq_name (sigma_i v) (sigma v))
                        ).


Lemma Prop5_ExistsTraceAndSigmaForTemplate : forall  allowSeq rlSetup rlp tr_temp, 
        (Def6_9_validRuleList rlp /\ Def2_1_Valid_AllowSequences allowSeq rlp)
          -> exists tr_log sigma SigmaList, Def5_7_Standard_Trace allowSeq rlSetup SigmaList tr_log
                ->    (Def6_10_StdTemplate allowSeq [tr_temp])
                                  /\ (eq (applySubTrace sigma [tr_temp]) tr_log)
                                      /\ (member sigma SigmaList).


(* Theorem 1 Given a valid rule list RL, for every standard trace with logs
tr_log, there exists a template tr_template of RL and a substitution sigma such as
sigma(tr_template) = tr_log. *)
Theorem Thm_7_1_ExistsTemplateAndSigmaForTrace : forall  allowSeq rlSetup rlp tr_log, 
        (Def6_9_validRuleList rlp /\ Def2_1_Valid_AllowSequences allowSeq rlp)
          -> exists tr_template sigma SigmaList, Def5_7_Standard_Trace allowSeq rlSetup SigmaList tr_log
                ->     (Def6_10_StdTemplate allowSeq tr_template)
                                  /\ (eq (applySubTrace sigma tr_template) tr_log)
                                      /\ (member sigma SigmaList).


(** Def 8 Equivalent (n1,n2) **)

Inductive Def6_13_Equivalent : ruleList -> term  -> term -> Prop :=
     | Def613_IO          : forall newRule pastRules ts1 ts2 t1 t2,  
                           (member (IN ts1) (premiseFacts newRule))
                              /\ lastOutputNoInput ts2 pastRules
                                /\ TermsInSamePosition ts1 ts2 t1 t2  ->
                                      Def6_13_Equivalent (newRule::pastRules) t1 t2
     | Def613_SamePosUSF  : forall RL t1 t2,  
                            (PresentInSamePositionUniqueStateFact RL t1 t2) -> 
                                      Def6_13_Equivalent RL t1 t2
     | Def613_SamePosUAF  : forall RL t1 t2,  
                            ((PresentInSamePositionUAF RL t1 t2)
                             /\
                             ((exists t3 t4, (Def6_13_Equivalent RL t3 t4)
                              /\
                               (not ((eq_term t1 t3) \/ (eq_term t1 t4) 
                                        \/ (eq_term t2 t3)\/ (eq_term t2 t4)))))) ->
                                       Def6_13_Equivalent RL t1 t2
     | Def613_EmptyFunc   : forall RL fn ,  
                          (Def6_13_Equivalent RL (Func fn []) (Func fn []))

     | Def613_FuncList      : forall RL fn t1 t2 t3 t4,  
                          (Def6_13_Equivalent RL (Func fn (t1::t3)) (Func fn (t2::t4))) ->
                            Def6_13_Equivalent RL (Bterm t1) (Bterm t2) ->
                              Def6_13_Equivalent RL (Func fn t3) (Func fn t4). 
                          
Fixpoint isEquivalent (rl:ruleList) (t1:term) (t2:term) : bool :=
  match (Def6_13_Equivalent rl t1 t2) with
      | True    =>  true
  end.

(* A helper definition for Def 9 to return one equivalent term for t1 *)
Fixpoint DefequivalentTerm (rl:ruleList) (t1:term) (t2:term) : term :=
  match (isEquivalent rl t1 t2) with
    | true    => t2 
    | false   => t1
  end.

(*How to collect all values returned by earlier def?*)
Inductive Def6_15_EquivalenceClass: ruleList -> term -> terms -> Prop :=  
  | Eqv_base  : forall rl t1, Def6_15_EquivalenceClass rl t1 [t1]
  | Eqv_step  : forall rl t1 t2 ts, Def6_13_Equivalent rl t1 t2 -> Def6_15_EquivalenceClass rl t1 ts 
                                -> not (member t2 ts) -> Def6_15_EquivalenceClass rl t1 (t2::ts).

Fixpoint isEquivalenceClass (rl:ruleList) (t1:term) (ts:terms) : bool :=
  match (Def6_15_EquivalenceClass rl t1 ts) with
      | True    =>  true
  end.


Lemma equivalentClassProperty : forall rl t ts t1 t2 f1 f2 l1 l2,
    Def6_9_validRuleList rl -> 
        Def6_15_EquivalenceClass rl t ts ->
          (member t1 ts) /\ (member t2 ts) -> 
            ((eq_term t1 (Bterm (Name (Pub n))) -> ((eq_term t1 t2) \/ (eq_term t2 (Bterm (Var x)))))
            \/ ((eq_term t1 (Func f1 l1 )) -> ((eq_term t2 (Func f2 l2 )) \/ (eq_term t2 (Bterm (Var x)))))).

Lemma Lemma_sigmaOfTermsSameForEquivalenceClass : forall rl rlSetup fs1 tr fs2 sigmaList sigma t t1 t2 ts,
    Def6_9_validRuleList rl -> 
          runInOrderSigma rl rlSetup sigmaList fs1 tr fs2 ->
              Def6_15_EquivalenceClass rl t ts ->
                (member t1 ts) /\ (member t2 ts) /\ (member sigma sigmaList) ->
                          (eq_term (applySubTerm sigma t1) (applySubTerm sigma t2)).



Fixpoint termAppearsInFacts (fs: facts) (tm:term) : Prop := 
  match fs with
    | f1::fss => (match f1 with 
                        | IN   ts => member tm ts 
                        | OUT  ts => member tm ts
                        | K    ts => member tm ts
                        | STATE n ts => member tm ts
                        | FR_P bt => eq_term (Bterm bt) tm 
                  end ) \/ termAppearsInFacts fss tm
    | []      => False 
  end.


Fixpoint termAppearsInRuleList (rl: ruleList) (tm:term) : Prop := 
  termAppearsInFacts (appendAny (allPremiseFacts rl) (allConclFacts rl)) tm.

Fixpoint termsFromFacts (fs: facts): list term  := 
  match fs with
    | f1::fss => appendAny (match f1 with 
                        | IN   ts => ts 
                        | OUT  ts => ts
                        | K    ts => ts
                        | STATE n ts => ts
                        | FR_P bt => [Bterm bt]
                  end ) (termsFromFacts fss) 
    | []      => []
  end.


Fixpoint AllTermsFromRuleList (rl: ruleList) : list term := 
  uniqueTerms (termsFromFacts (appendAny (allPremiseFacts rl) (allConclFacts rl))).


Fixpoint Def_ListArgs (uaf:fact) (r:rule) : terms :=
match (Def6_8_validRule r []) /\ (uniqueArgumentsFact uaf r []) with
    | True    =>   match uaf with 
                   | STATE n ts =>  ts
                   | _          => []
                   end
end.

Definition Def6_16_LinkedEqClasses (rl:ruleList) (e1:terms) (e2:terms) : Prop :=
    forall t1 t2,
        Def6_9_validRuleList rl /\ 
           Def6_15_EquivalenceClass rl t1 e1 /\
              Def6_15_EquivalenceClass rl t2 e2 
                ->
                  exists uaf a1 a2 r, 
                            (member a1 e1) /\ 
                            (member a2 e2) /\
                            (uniqueArgumentsFact uaf r rl) /\
                            (member a1 (Def_ListArgs uaf r)) /\
                            (member a2 (Def_ListArgs uaf r)) /\
                            (member r rl).

Definition termEqTogether (rl:ruleList) (t:term) (t1:term) : terms :=
    if (isEquivalent rl t t1) then uniqueTerms (appendAny [t] [t1]) else  [t1].
  

Fixpoint termsEqTogether (rl:ruleList) (t:term) (ts:terms) : terms :=
 match ts with
    | ts1::tss   => uniqueTerms (appendAny (termEqTogether rl t ts1) ( termsEqTogether rl t tss))
    | []        =>  []
  end.

(*Eq class for one term*)
Fixpoint singleEqClass (rl:ruleList) (t:term)  : terms := 
      termsEqTogether rl  t (AllTermsFromRuleList rl) .

(*Eq classes for all terms*)
Fixpoint EqClassesTogether (rl:ruleList) (ts:terms) : list terms :=
 match ts with
    | ts1::tss   =>  (singleEqClass rl ts1)::( EqClassesTogether rl tss)
    | []        =>  []
  end.

(*Eq classes for all terms*)
Fixpoint SetofEqClasses (rl:ruleList)  : list terms :=
    EqClassesTogether rl (AllTermsFromRuleList rl).

Definition Def_MinEqSet (rl:ruleList) (EqOfEq:list terms) : Prop :=
    forall EqSet eq1 eq2,
        Def6_9_validRuleList rl /\ 
           eq  EqSet (SetofEqClasses rl) 
                ->
                 member eq1 (SetofEqClasses rl) /\
                    member eq2 EqOfEq /\
                      Def6_16_LinkedEqClasses rl eq1 eq2.


Definition Def6_18_ProtocolUAFs (rl:ruleList) (EqOfEq:list terms) (uafList:facts): Prop :=
    forall r uaf eqClass,      
                Def6_9_validRuleList rl /\ 
                  Def_MinEqSet rl EqOfEq /\
                    (someCommonElements (Def_ListArgs uaf r) eqClass) /\
                      (member r rl) /\ (member eqClass EqOfEq) /\ (member uaf uafList).


Fixpoint UAFfromSetup (uaf1:fact) (uaf2:fact) : fact :=
 match uaf1, uaf2 with 
  | STATE n1 ts, STATE n2 tr  => if (beq_name n1 n2) then STATE n2 tr else STATE n1 ts
  | _,_                     =>  uaf1
  end.

Definition UAFsFromSetup (uafListProto:facts) (uafListSetup:facts) (matchedSetupUAFs:list facts) := True.

Definition Def6_19_MatchingSetupUAFs (rl:ruleList) (EqOfEq:list terms) (SetupUAFList:list facts): Prop :=
    forall   uafList r rlSetup rlProto uafListSetup,      
                Def6_9_validRuleList rl /\ 
                  eq rl (appendAny [r] (appendAny rlSetup rlProto)) /\
                  eq rl (appendAny rlSetup rlProto) /\
                  Def_MinEqSet rl EqOfEq /\
                    Def6_18_ProtocolUAFs rl EqOfEq uafList /\
                    eq (collectUniqueArgFacts (collectStateFacts (r::rlSetup)) r rlSetup) uafListSetup /\
                      (* Is it necessary to replace all UAFs in rlProto by UAFs from rlSetup and then replace argument
                        or just replacing arguments should be enough?     *)
                    (UAFsFromSetup uafList uafListSetup SetupUAFList).