(** Contents : 0: General House Keeping 1: Syntax definitions 2: Equality, membership and extraction functions for the syntax 2A: Equality functions 2B: Membership functionsflk 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 Sec8_Chap6WellFormedRules. (*** ========================================== *** 9: Some useful lemmas on well formedness ============================================ *) 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. (** 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. 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). 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). 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. 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. 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. 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. Axiom InputToOutputRemovesInput : forall r sigma f1 l f2, oneInputXorOutput f1 -> InputToOutputProtocolRule r -> reduceWithRuleSigma r sigma f1 l f2 -> noInputs f2. Axiom StateToOutputDoesNotAddInput : forall r sigma f1 l f2, noInputOrOutput f1 -> StateToOutputProtocolRule r -> reduceWithRuleSigma r sigma f1 l f2 -> noInputs f2. 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. 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 -> Def6_2_wellformedRulesFromState f1 (r1::rs) -> oneInputXorOutput f2. Axiom ruleCanMakeOutput : forall rule sigma f1 label f2 , reduceWithRuleSigma rule sigma f1 label f2 -> noOutputs f1 -> (oneOutput (conclFacts rule)) -> oneOutput f2. (* NEW AXIOM *) Axiom outputInRuleWillMatchRule : forall rule1 rules sigma f1 l f2 vars, reduceWithGroundRule (applySubRule sigma rule1) f1 l f2 -> groundRule (applySubRule sigma rule1) -> Def6_2_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) -> Def6_2_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 -> Def6_2_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). Lemma outputMatchesNextInputEndProtocol : forall r1 r2 sigma1 sigma2 trms1 trms2 f1 trace f3 , runInOrderSigmaProtocol ( [r1;r2]) ([sigma1;sigma2]) f1 trace f3 -> Def6_2_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 Def6_2_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 -> Def6_2_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, Def6_2_wellformedRulesFromState f1 (r :: rs) -> reduceWithGroundRule (applySubRule sigma r) f1 l f2 -> Def6_2_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 -> Def6_2_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 Def6_2_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 -> Def6_2_wellformedRulesFromState f1 (r :: rules) -> exists f2 trace2 trace3, (runInOrderSigmaProtocol [r] [sigma] f1 trace2 f2 /\ runInOrderSigmaProtocol rules sigmas f2 trace3 f3 /\ Def6_2_wellformedRulesFromState f2 rules). Axiom wellformedHead : forall f1 r rules, Def6_2_wellformedRulesFromState f1 (r :: rules) -> Def6_2_wellformedRulesFromState f1 [r]. Lemma lastOutputInFacts : forall rules sigmas f1 trace f2 trms sigma, runInOrderSigmaProtocol rules sigmas f1 trace f2 -> Def6_2_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 -> Def6_2_wellformedRulesFromState f1 rules -> Def6_2_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. Axiom OutputInRuleWillMatchStdRun : forall r rlSetup sigma f1 t f2 trms, runInOrderSigma [r] rlSetup [sigma] f1 t f2 -> Def6_2_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 -> Def6_2_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 -> Def6_2_wellformedRulesFromState f1 (r :: rlProto) -> exists f2 trace2 trace3, (runInOrderSigma [r] rlSetup [sigma] f1 trace2 f2 /\ runInOrderSigma rlProto rlSetup sigmas f2 trace3 f3 /\ Def6_2_wellformedRulesFromState f2 rlProto). Lemma lastOutputInFactsStdRun : forall protocolRules setupRules sigmas f1 trace f2 trms sigma, runInOrderSigma protocolRules setupRules sigmas f1 trace f2 -> Def6_2_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 -> Def6_2_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 -> Def6_2_wellformedRulesFromState f1 protocolRules -> Def6_2_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) -> Def6_2_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 -> Def6_2_wellformedRulesFromState f1 rules -> Def6_2_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 -> Def6_2_wellformedRulesFromState f1 rlProto -> Def6_2_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.