(** 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: Substitution

   4: Ground terms and rules instances

   5: Tamarin Reduction

   6: Example

   7: Definitions from Chapter 5 of the thesis


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

   10: Definitions from Chapter 6 of the thesis
      10A: Types of Facts allowed in the system  

   11: Props and Theorems from Chapter 6 

**)


Load Sec7_Chap5Defs.


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

(* ===========================================
  8A: 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.
 

 



(** ====================================================================
  8B : 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 eq_STATEname (f1:fact) (f2:fact) : Prop :=
  match f1,f2 with
   | STATE n1 ts1, STATE n2 ts2 => eq_name n1 n2 
   | _, _ => False
  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) (usf:fact) (t1:term) (t2:term) : Prop :=
match fls with
  | f1::fs  =>  (eq_STATEname f1 usf) /\ (CheckTermsUSF f1 fs t1 t2) \/ (CheckFactsInUSF fs usf 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) (uaf:fact) (t1:term) (t2:term) : Prop :=
match fls with
  | f1::fs  =>  (eq_STATEname f1 uaf) /\ (CheckTermsUAF f1 fs t1 t2) \/ (CheckFactsInUAF fs uaf t1 t2)
  | []      =>  False
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. 




(** ================================
***   8C: 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.

(* ====================================================*)
(* 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 Def6_2_wellformedRulesFromState (fs:facts) (rs:ruleList) : Prop :=
  (oneInputXorOutput fs /\ wellFormedProtoRuleFromInOut rs)
    \/ ( noInputOrOutput fs /\ wellFormedProtoRuleNoInOut rs). 


(* ====================================================*)
(* New definition of well formed Setup rule *)
(* ====================================================*)

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

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

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

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

Fixpoint wellFormedSetupRuleInOutState (r:rule) : Prop :=
(InputToOutputSetupRule r ) \/ (InputToStateSetupRule r)
    \/ (StateToOutputSetupRule r) \/ (StateToStateSetupRule r).


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))
                  \/ ((StateToStateSetupRule r) /\ (wellFormedSetupRuleFromInOut rss))
                    \/ ((InputToOutputSetupRule r) /\ (wellFormedSetupRuleFromInOut rss))
   end.


Definition Def6_2_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.