Load Sec10_Chap6Defs.



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


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


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

Axiom Prop4_ExistsTraceAndSigmaForTemplate : forall allowSeq rlSetup rlp tr_temp,
        (Def6_9_validRuleList rlp /\ Def5_3_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 Thm_6_1_ExistsTemplateAndSigmaForTrace : forall allowSeq rlSetup rlp tr_log,
        (Def6_9_validRuleList rlp /\ Def5_3_Valid_AllowSequences allowSeq rlp)
          -> exists SigmaList, Def5_7_Standard_Trace allowSeq rlSetup SigmaList tr_log
                -> exists tr_template sigma, (Def6_10_StdTemplate allowSeq tr_template)
                                  /\ (eq (applySubTrace sigma tr_template) tr_log)
                                      /\ (member sigma SigmaList).

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 usf t1 t2,
                            (PresentInSamePositionUSF RL usf t1 t2) ->
                                      Def6_13_Equivalent RL t1 t2
     | Def613_SamePosUAF : forall RL t1 t2 uaf,
                            ((PresentInSamePositionUAF RL uaf t1 t2)
                             /\
                             (exists t3 t4, (PresentInSamePositionUAF RL uaf t3 t4)
                              /\
                                   (not ((eq_term t1 t3) \/ (eq_term t1 t4)
                                        \/ (eq_term t2 t3)\/ (eq_term t2 t4)))
                                /\ (not (PresentInSamePositionUAF RL uaf t1 t3))
                                /\ (not (PresentInSamePositionUAF RL uaf t2 t4))
                                /\ Def6_13_Equivalent RL t3 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)
     | Def613_Reflexive : forall RL n1 ,
                          (Def6_13_Equivalent RL n1 n1)

     | Def613_Symmetric : forall RL n1 n2 ,
                          (Def6_13_Equivalent RL n1 n2) ->
                                          (Def6_13_Equivalent RL n2 n1)
     | Def613_Transitive : forall RL n1 n2 n3 ,
                            (Def6_13_Equivalent RL n1 n2)
                                    /\ (Def6_13_Equivalent RL n2 n3) ->
                                                (Def6_13_Equivalent RL n1 n3).


Fixpoint isEquivalent (rl:ruleList) (t1:term) (t2:term) : bool :=
  match (Def6_13_Equivalent rl t1 t2) with
      | True => true
  end.

Fixpoint DefequivalentTerm (rl:ruleList) (t1:term) (t2:term) : term :=
  match (isEquivalent rl t1 t2) with
    | true => t2
    | false => t1
  end.

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.

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

Axiom Prop5_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.

Fixpoint singleEqClass (rl:ruleList) (t:term) : terms :=
      termsEqTogether rl t (AllTermsFromRuleList rl) .

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

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.

Fixpoint SetupUAFsFromRL (RL:ruleList): list fact :=
  match RL with
    | (RuleSetup f1 l1 f2)::rs => appendAny (collectUniqueArgFacts f1 (RuleSetup f1 l1 f2) rs)
                                                 (SetupUAFsFromRL rs)
    | (RuleProto _ _ _)::rs => SetupUAFsFromRL rs
    | [] => []
  end.

Fixpoint ProtocolUAFsFromRL (RL:ruleList): list fact :=
  match RL with
    | (RuleProto f1 l1 f2)::rs => appendAny (collectUniqueArgFacts f1 (RuleSetup f1 l1 f2) rs)
                                                 (ProtocolUAFsFromRL rs)
    | (RuleSetup _ _ _)::rs => ProtocolUAFsFromRL rs
    | [] => []
  end.

Fixpoint TermsFromUAFs (ft:facts): list term :=
  match ft with
    | (STATE nm tm)::fs => appendAny tm (TermsFromUAFs fs)
    | _::fs => TermsFromUAFs fs
    | [] => []
  end.

Fixpoint AllBaseTerms (btm:list baseTerm) : list term :=
  match btm with
    | bt1::bts => (Bterm bt1) :: (AllBaseTerms bts)
    | [] => []
  end.

Fixpoint subTermsFromTerms (tm:list term) : list term :=
    match tm with
      | t1::ts => match t1 with
                          | Bterm _ => t1::(subTermsFromTerms ts)
                          | Func nm bts => appendAny (AllBaseTerms bts) (subTermsFromTerms ts)
                    end
      | [] => []
    end.

Fixpoint termsFromActionLabel (al:actionLabel) : list term :=
    match al with
      | ActLabel nm ll => subTermsFromTerms ll
    end.

Definition termsFromActionLabels : (list actionLabel) -> list term := mapListFunction termsFromActionLabel.

Fixpoint termsFromLabel (lb:label) : list term :=
    match lb with
      | BasicLabel ll => termsFromActionLabels ll
      | LoggedLabel lg ll => appendAny (termsFromActionLabel lg) (termsFromActionLabels ll)
      | LoggedSIDLabel t lg ll => appendAny (termsFromActionLabel lg) (termsFromActionLabels ll)
    end.

Fixpoint termsFromTemplate (tmp:trace) : list term :=
    match tmp with
      | l1::ls => appendAny (termsFromLabel l1) (termsFromTemplate ls)
      | [] => []
    end.

Fixpoint rewriteBaseTerm (bt:baseTerm) (t1:term) (t2:term) : baseTerm :=
   match t1, t2 with
      | Bterm told, Bterm tnew => if (beq_baseTerm bt told) then tnew else bt
      | _, _ => bt
  end.

Fixpoint rewriteBaseTerms (lbt:baseTerms) (t1:term) (t2:term) : baseTerms :=
   match lbt with
      | bt1::bts => (rewriteBaseTerm bt1 t1 t2)::(rewriteBaseTerms bts t1 t2)
      | [] => []
  end.


Fixpoint rewriteTerms (tm:terms) (t1:term) (t2:term) : terms :=
   match tm with
      | tm1::tms => match tm1 with
                        | Func fn lbt => if (beq_term tm1 t1) then ((Func fn (rewriteBaseTerms lbt t1 t2))::(rewriteTerms tms t1 t2))
                                  else (tm1::(rewriteTerms tms t1 t2))

                        | Bterm bt => if (beq_term tm1 t1) then (t2::(rewriteTerms tms t1 t2))
                                  else (tm1::(rewriteTerms tms t1 t2))
                      end
      | [] => []
   end.

Fixpoint rewriteTermsInActionLabel (al:actionLabel) (t1:term) (t2:term) :=
  match al with
      | ActLabel nm ll => ActLabel nm (rewriteTerms ll t1 t2)
    end.

Fixpoint rewriteTermsInActionLabels (als:list actionLabel) (t1:term) (t2:term) :=
  match als with
      | al1::alss => (rewriteTermsInActionLabel al1 t1 t2)::( rewriteTermsInActionLabels alss t1 t2)
      | [] => []
    end.

Fixpoint rewriteTermsInLabel (lbl:label) (t1:term) (t2:term) :=
  match lbl with
      | BasicLabel ll => BasicLabel (rewriteTermsInActionLabels ll t1 t2)
      | LoggedLabel lg ll => LoggedLabel (rewriteTermsInActionLabel lg t1 t2) (rewriteTermsInActionLabels ll t1 t2)
      | LoggedSIDLabel t lg ll => LoggedSIDLabel t (rewriteTermsInActionLabel lg t1 t2) (rewriteTermsInActionLabels ll t1 t2)
    end.


Fixpoint funPresent (ft:term) (eqtrms:terms) : term :=
  match eqtrms with
    | eq1::eqs => match eq1 with
                        | Func _ _ => eq1
                        | _ => funPresent ft eqs
                      end
    | [] => ft
  end.

Fixpoint termIsFunc (ft:term) : Prop :=
  match ft with
    | Func _ _ => True
    | _ => False
  end.

Fixpoint b_termIsFunc (ft:term) : bool :=
  match ft with
    | Func _ _ => true
    | _ => false
  end.

Fixpoint b_pubTerm (ts:baseTerm) : bool :=
  match ts with
    | Name n => true
    | _ => false
  end.

Definition b_pubTerms : baseTerms -> bool := btrueForOne b_pubTerm.


Fixpoint pubPresent (pb:term) (eqtrms:terms) : term :=
  match eqtrms with
    | eq1::eqs => match eq1 with
                        | Bterm (Name nm1) => eq1
                        | _ => pubPresent pb eqs
                      end
    | [] => pb
  end.

Fixpoint termIsPub (t:term) : Prop :=
  match t with
    | Bterm (Name (Pub _)) => True
    | _ => False
  end.

Fixpoint b_termIsPub (t:term) : bool :=
  match t with
    | Bterm (Name (Pub _)) => true
    | _ => false
  end.

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


Fixpoint TermsInSameNameAndPositionUAF (uaf1:fact) (uaf2:fact) (t1:term) (t2:term) : Prop :=
  match uaf1, uaf2 with
   | STATE nm1 tm1, STATE nm2 tm2 => (eq_STATEname uaf1 uaf2) /\ (TermsInSamePosition tm1 tm2 t1 t2)
   | _, _ => False
  end.

Definition TermsMatchSetupAndProtoUAFs (EqOfEq:list terms) (uafPList:facts) (uafSList:facts) : Prop :=
  forall tp1 tp2 ts eqClass uafS uafP1 uafP2,
                          (member tp1 eqClass) /\ (member tp2 eqClass) /\
                            (member eqClass EqOfEq) /\
                                (member tp1 (TermsFromUAFs uafPList)) /\ (member tp2 (TermsFromUAFs uafPList)) /\
                                   (member uafP1 uafPList) /\ (member uafP2 uafPList) /\
                                      (TermsInSameNameAndPositionUAF uafP1 uafP2 tp1 tp2) /\
                                     (member uafS uafSList) ->
                                        (TermsInSameNameAndPositionUAF uafP1 uafS tp1 ts) /\
                                        (TermsInSameNameAndPositionUAF uafP2 uafS tp2 ts).

Definition Def6_19_MatchingSetupUAFs (rl:ruleList) (EqOfEq:list terms) (uafSList:facts): Prop :=
    forall uafPList,
                Def6_9_validRuleList rl /\
                        Def_MinEqSet rl EqOfEq /\
                          Def6_18_ProtocolUAFs rl EqOfEq uafPList /\
                            (eq (SetupUAFsFromRL rl) uafSList) ->
                                  TermsMatchSetupAndProtoUAFs EqOfEq uafPList uafSList.



Fixpoint EqToTerm_CaseA (eq:terms) (t:term): term :=
  match eq with
    | eq1::eqs => if (b_termIsFunc eq1) then eq1 else (EqToTerm_CaseA eqs t)
    | [] => t
  end.

Fixpoint EqToTerm_CaseB (eq:terms) (t:term): term :=
  match eq with
    | eq1::eqs => if (b_termIsPub eq1) then eq1 else (EqToTerm_CaseB eqs t)
    | [] => t
  end.

Fixpoint EqToTerm_CaseC (eq:terms) (t:term) : term :=
  match eq with
    | eq1::eqs => eq1
    | [] => t
  end.

Inductive rewriteWithRules: label -> ruleList -> label -> Prop :=
  | lblcaseA : forall t RL lbl1, ((In t (termsFromLabel lbl1)) /\
                  not (eq_term (EqToTerm_CaseA (singleEqClass RL t) t) t)) ->
                  rewriteWithRules lbl1 RL (rewriteTermsInLabel lbl1 t (EqToTerm_CaseA (singleEqClass RL t) t))


  | lblcaseB : forall t RL lbl1, ((In t (termsFromLabel lbl1)) /\
                  not (eq_term (EqToTerm_CaseB (singleEqClass RL t) t) t)) ->
                  rewriteWithRules lbl1 RL (rewriteTermsInLabel lbl1 t (EqToTerm_CaseB (singleEqClass RL t) t))


  | lblcaseC : forall t RL lbl1, ((In t (termsFromLabel lbl1)) /\
                      (eq_term (EqToTerm_CaseA (singleEqClass RL t) t) t)
                        /\
                        (eq_term (EqToTerm_CaseB (singleEqClass RL t) t) t))
                               ->
                          rewriteWithRules lbl1 RL (rewriteTermsInLabel lbl1 t (EqToTerm_CaseC (singleEqClass RL t) t)).

Definition noOtherEquivalentTermsPresent (t1:term) (tmp:trace) (RL:ruleList) :=
 not (exists t2, (In t2 (termsFromTemplate tmp))
                    /\ (In t2 (singleEqClass RL t1))
                        /\ not (eq_term t1 t2)).

Inductive Def6_20_PreRewriteTemplate: trace -> ruleList -> trace -> Prop :=
   | Case_Base : forall RL , Def6_20_PreRewriteTemplate [] RL []
   | case_Step : forall l1 l2 RL t1 t2, (rewriteWithRules l1 RL l2)
                              -> Def6_20_PreRewriteTemplate t1 RL t2
                                  -> Def6_20_PreRewriteTemplate (l1::t1) RL (l2::t2).


Definition Def_6_20_1_TemplateNormalForm (tmp:trace) (RL:ruleList) :=
forall t1, (In t1 (termsFromTemplate tmp)) -> (noOtherEquivalentTermsPresent t1 tmp RL)

                                                  /\ exists tf,
                                                          (In tf (singleEqClass RL t1)) /\ (termIsFunc tf) ->
                                                               (eq_termFuncName t1 tf)

                                                  /\ exists tp,
                                                          (In tp (singleEqClass RL t1) /\ (termIsPub tp) ->
                                                               (eq_term t1 tp)).


Axiom normalFormExistsForEveryTmp : forall tmp f2 RL,
    Def6_9_validRuleList RL /\
          Def6_2_wellformedRulesFromState f2 RL /\
            Def6_10_StdTemplate [RL] tmp
               -> exists tmp1,
                    Def6_20_PreRewriteTemplate tmp RL tmp1 /\
                                Def_6_20_1_TemplateNormalForm tmp1 RL.

Definition Def_6_20_2_InstantiateTemplate (tmp1:trace) (RL:ruleList) (tmp2:trace): Prop :=
exists sigma, forall uafP,
                  (In uafP (ProtocolUAFsFromRL RL)) ->
                      exists uafS,
                            (In uafS (SetupUAFsFromRL RL)) /\
                              (eq_fact uafS (applySubFact sigma uafP)) /\
                                  eq_trace tmp2 (applySubTrace sigma tmp1).

Definition Def6_20_3_RewriteTemplate (tmp1:trace) (RL:ruleList) (tmp2:trace): Prop :=
  exists tmp, (Def6_20_PreRewriteTemplate tmp1 RL tmp) /\
                  Def_6_20_1_TemplateNormalForm tmp RL /\
                    Def_6_20_2_InstantiateTemplate tmp RL tmp2.


Axiom Lemma6_4_noVariableWithFnEquivInEquivalentClass : forall rl tempT v newT,
        exists fn ft,
        (Def6_13_Equivalent rl (Bterm (Var v)) (Func fn ft)) /\
                            (Def6_20_3_RewriteTemplate tempT rl newT) ->
                                  not (member v (getVarsInTemplate newT)) .


Theorem Thm_6_2_ExistsStdRunForRewrittenTemplate : forall allowSeq rlSetup rlp tr_template sigma f2,
        (Def6_9_validRuleList rlp) /\ (Def6_2_wellformedRulesFromState f2 rlp) /\ (eq allowSeq (allPrefixs rlp))
                    -> exists tr_new tr_log, (Def5_3_Valid_AllowSequences allowSeq rlp)
                          /\ (Def6_10_StdTemplate allowSeq tr_template)
                            /\ (Def6_20_3_RewriteTemplate tr_template rlp tr_new)
                                 /\ (eq (applySubTrace sigma tr_new) tr_log)
                        -> exists sigmaList fs1 fs2,
                                      (runInOrderSigma rlp rlSetup sigmaList fs1 tr_log fs2)
                                        /\ (member sigma sigmaList).
Fixpoint LabelAt {A:Type} (n:nat) (l:list A) (default:A) {struct l} : A :=
    match n, l with
      | O, x :: l' => x
      | O, other => default
      | S m, [] => default
      | S m, x :: t => LabelAt m t default
    end.

Fixpoint indexExists {A:Type} (m:nat) (l:list A) : Prop :=
    match m, l with
      | O, x :: l' => True
      | O, other => False
      | S n, [] => False
      | S n, x :: t => indexExists n t
    end.


Fixpoint subSequenceTrace (t1:trace) (t2:trace): Prop :=
  match t1, t2 with
    | t11::t1s, t21::t2s => ((eq_label t11 t21) /\ (subSequenceTrace t1s t2s))
                                    \/
                                (subSequenceTrace t1s t2)
    | [], _ => True
    | _, [] => False
  end.

Definition Def6_21_Correspondence (tr_temp:trace) (tr_log:trace) (m:nat) (sigma:substitution) : Prop :=
 forall temp_m lbl,
      (subSequenceTrace (applySubTrace sigma tr_temp) tr_log) /\
        (eq_label (lastElement temp_m (applySubTrace sigma tr_temp)) (LabelAt m tr_log lbl)).

Definition Def6_22_CorrespondenceRestriction (RL_proto:ruleList) (allowSeq: list ruleList) (tr_log:trace) (tr_tempsessions: trace) : Prop :=
  forall m, (indexExists m tr_log) /\
             Def6_12_StdSessionTemplate allowSeq tr_tempsessions ->
              exists sigma tr_rewrittenTemp ,
                (Def6_20_3_RewriteTemplate tr_tempsessions RL_proto tr_rewrittenTemp) ->
                  Def6_21_Correspondence tr_rewrittenTemp tr_log m sigma.

Axiom Lemma6_5_CorrespondenceRestrictionHoldsforAllStLookingTraces :
      forall RL_proto allowSeq setupRules tr_tempsessions tr_log ,
            (eq allowSeq (allPrefixs RL_proto)) /\
            Def5_7_Standard_Looking_Trace allowSeq setupRules tr_log /\
             Def6_12_StdSessionTemplate allowSeq tr_tempsessions ->
               Def6_22_CorrespondenceRestriction RL_proto allowSeq tr_log tr_tempsessions.

Axiom Lemma6_6_CorrespondenceRestrictionImpliesTracesAndTemplatesMatch :
      forall RL_proto allowSeq setupRules tr_temp tr_log Log_tr Log_temp sigma,
      (eq allowSeq (allPrefixs RL_proto)) /\
       Def6_22_CorrespondenceRestriction RL_proto (AddSID allowSeq) tr_log tr_temp /\
            Def5_7_Standard_Looking_Trace allowSeq setupRules tr_log /\
             Def6_10_StdTemplate allowSeq (RemoveSID tr_temp) /\
                   (member Log_tr tr_log) /\
                     (member Log_temp tr_temp) ->
                        (eq_label Log_tr (applySubLabel sigma Log_temp)).


Definition Def6_23_UniquenessRestriction (RL_proto:ruleList) (tr_log:trace) : Prop :=
  forall Log_i Log_j x sid_1 sid_2 pars_i pars_j ,
      (member x (Def5_5_freshInRLProto RL_proto))
        /\ (LoggedLbl_in_Trace Log_i tr_log)
        /\ (LoggedLbl_in_Trace Log_j tr_log)
        /\ (getSID Log_i sid_1)
          /\ (getSID Log_j sid_2)
             /\ (getParsFromLog Log_i pars_i)
              /\ (getParsFromLog Log_j pars_j)
                 /\ (member x (commonFreshNames (getFreshProtoNamesinLabel Log_i) (getFreshProtoNamesinLabel Log_j)))
                    -> (eq_baseTerm sid_1 sid_2).

Axiom Lemma6_7_UniquenessRestrictionHoldsforAllStLookingTraces :
      forall RL_proto allowSeq setupRules tr_log ,
            (eq allowSeq (allPrefixs RL_proto)) /\
            Def5_7_Standard_Looking_Trace allowSeq setupRules tr_log ->
               Def6_23_UniquenessRestriction RL_proto tr_log .

Axiom Lemma6_8_TraceAndTemplateMatchImpliesBothRestrictionsHold :
      forall RL_proto allowSeq tr_temp tr_log Log_tr Log_temp sigma,
            (eq allowSeq (allPrefixs RL_proto)) /\
             ((member Log_tr tr_log) /\
                 (member Log_temp tr_temp) /\
                     (eq_label Log_tr (applySubLabel sigma Log_temp))) ->
                        (Def6_22_CorrespondenceRestriction RL_proto allowSeq tr_log tr_temp /\
                           Def6_23_UniquenessRestriction RL_proto tr_log).

Definition noFreshProtoNamesInSetup (rl:ruleList) : Prop :=
            eq (Def5_5_freshInRLProto rl) [].


Definition validSetupRuleList (rl:ruleList) : Prop :=
            onlyBasicLogsInRL rl
            /\ noFreshProtoNamesInSetup rl.


Definition WellFormedAndValidRLSetupProto (rlSetup: ruleList) (rlProto:ruleList) : Prop:=
                         validSetupRuleList rlSetup
                        /\ Def6_9_validRuleList rlProto
                        /\ Def6_2_wellformedRulesFromState [] (appendAny rlSetup rlProto).


Definition WellFormedAndValidRuleList (RL: ruleList) : Prop:=
exists rlSetup rlProto, eq (appendAny rlSetup rlProto) RL
                       /\ WellFormedAndValidRLSetupProto rlSetup rlProto.

Theorem Thm_6_3_StealthAttackImpliesBothRestrictionsOnTraces : forall allowSeq rlSetup attackTrace rlProto,
                (WellFormedAndValidRLSetupProto rlSetup rlProto
            /\ (eq allowSeq (allPrefixs rlProto)))
            ->
            ((Def5_9_Stealth_Attack allowSeq rlSetup (RemoveSID attackTrace))
        <-> exists tmplt_sessions tmplt_Rewritten,
               Def6_12_StdSessionTemplate allowSeq tmplt_sessions /\
               Def6_20_3_RewriteTemplate tmplt_sessions rlProto tmplt_Rewritten /\
               Def6_22_CorrespondenceRestriction rlProto allowSeq tmplt_Rewritten attackTrace
                /\
                Def6_23_UniquenessRestriction rlProto attackTrace).