Library Sec9_LemmasOnWellformedness
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.
Lemma noOutputsMeansNoOutputs: forall factslist trm, noOutputs factslist -> member (OUT trm) factslist -> False.
Lemma singleOutputEquals : forall trm1 trm2 factsList,
(member (OUT trm1) factsList) -> (member (OUT trm2) factsList)
-> oneOutput factsList -> trm1 = trm2.
Rajiv : Added these lemmas
Lemma noOutputsMeansNoOutputsInFactOrFacts: forall f fs t1,
noOutputs (f::fs) -> not (eq_fact (OUT t1) f) /\ noOutputs fs.
Lemma emptyRuleCantMakeOutput : forall sigma f1 label f2 ,
reduceWithRuleSigma (RuleProto [] label []) sigma f1 label f2
-> noOutputs f1 -> noOutputs f2.
Lemma sigmaNoInputFacts: forall f1 f2 sigma,
applySubFacts sigma f1 = f2 -> noInputs f2 -> noInputs f1.
Lemma sigmaNoInputFacts2: forall f1 f2 sigma,
applySubFacts sigma f1 = f2 -> noInputs f1 -> noInputs f2.
Lemma sigmaNoOutputFacts: forall f1 f2 sigma,
applySubFacts sigma f1 = f2 -> noOutputs f1 -> noOutputs f2.
Lemma sigmaNoOutputFacts2: forall f1 f2 sigma,
applySubFacts sigma f1 = f2 -> noOutputs f2 -> noOutputs f1.
Lemma sigmaNoInputOrOutputFacts: forall f1 f2 sigma,
applySubFacts sigma f1 = f2 -> noInputOrOutput f1 -> noInputOrOutput f2.
Lemma sigmaOneInputXorOutputFacts: forall f1 f2 sigma,
applySubFacts sigma f1 = f2 -> oneInputXorOutput f1 -> oneInputXorOutput f2.
Axiom sigmaoneOutputXorInputIsFacts: forall f1 f2 sigma trms,
applySubFacts sigma f1 = f2
-> oneOutputXorInputIs f1 trms -> oneOutputXorInputIs f2 trms.
Lemma sigmaOneInputFact: forall f1 f2 sigma,
applySubFacts sigma f1 = f2 -> oneInput f2 -> oneInput f1.
Lemma sigmaOneInputFact2: forall f1 f2 sigma,
applySubFacts sigma f1 = f2 -> oneInput f1 -> oneInput f2.
Lemma sigmaOneOutputFact: forall f1 f2 sigma,
applySubFacts sigma f1 = f2 -> oneOutput f1 -> oneOutput f2.
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.
Lemma ginstWithSigmaNoInputP: forall f1 f2 f3 f4 l1 l2 sigma,
ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
-> noInputs f3 -> noInputs f1.
Lemma ginstWithSigmaOneInputP: forall f1 f2 f3 f4 l1 l2 sigma,
ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
-> oneInput f3 -> oneInput f1.
Lemma ginstWithSigmaNoOutputC: forall f1 f2 f3 f4 l1 l2 sigma,
ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
-> noOutputs f4 -> noOutputs f2.
Lemma ginstWithSigmaNoOutputP: forall f1 f2 f3 f4 l1 l2 sigma,
ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
-> noOutputs f3 -> noOutputs f1.
Lemma ginstWithSigmaOneOutputC: forall f1 f2 f3 f4 l1 l2 sigma,
ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
-> oneOutput f4 -> oneOutput f2.
Lemma ginstWithSigmaMoreThanOneOutputC: forall f1 f2 f3 f4 l1 l2 sigma,
ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
-> moreThanOneOutput f4 -> moreThanOneOutput f2.
Lemma ginstWithSigmaNoInputOutputC: forall f1 f2 f3 f4 l1 l2 sigma,
ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
-> noInputOrOutput f4 -> noInputOrOutput f2.
Lemma ginstWithSigmaNoInputOutputP: forall f1 f2 f3 f4 l1 l2 sigma,
ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
-> noInputOrOutput f3 -> noInputOrOutput f1.
Lemma ginstWithSigmaOneInputXorOutputC: forall f1 f2 f3 f4 l1 l2 sigma,
ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
-> oneInputXorOutput f4 -> oneInputXorOutput f2.
Lemma ginstWithSigmaOneInputXorOutputP: forall f1 f2 f3 f4 l1 l2 sigma,
ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
-> oneInputXorOutput f3 -> oneInputXorOutput f1.
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.
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.
Lemma noOutputsTail : forall f fs,
noOutputs (f::fs) -> noOutputs fs.
Lemma noInputsTail : forall f fs,
noInputs (f::fs) -> noInputs fs.
Lemma noInputOrOutputTail : forall f fs,
noInputOrOutput (f::fs) -> noInputOrOutput fs.
Lemma noOutputsAcrossRemoveFact : forall f fs,
noOutputs fs -> noOutputs (removeFact f fs).
Lemma noOutputsAcrossRemove : forall f1 f2,
noOutputs f2 -> noOutputs (removeFacts f1 f2).
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).
Lemma noInputOrOutputAcrossRemoveFact : forall f fs,
noInputOrOutput fs -> noInputOrOutput (removeFact f fs).
Lemma noInputsAcrossRemove : forall f1 f2,
noInputs f2 -> noInputs (removeFacts f1 f2).
Lemma noInputOrOutputAcrossRemove : forall f1 f2,
noInputOrOutput f2 -> noInputOrOutput (removeFacts f1 f2).
Lemma AppendNoOutputs : forall f1 f2,
noOutputs f1 -> noOutputs f2 -> noOutputs (appendAny f1 f2).
Lemma AppendNoInputs : forall f1 f2,
noInputs f1 -> noInputs f2 -> noInputs (appendAny f1 f2).
Lemma AppendSingleOutput : forall f1 f2,
oneOutput f1 -> noOutputs f2 -> oneOutput (appendAny f1 f2).
Lemma AppendSingleOutput2 : forall f1 f2,
oneOutput f2 -> noOutputs f1 -> oneOutput (appendAny f1 f2).
Lemma AppendMinOneOutput : forall f1 f2,
minOneOutput f1 -> noOutputs f2 -> minOneOutput (appendAny f1 f2).
Lemma AppendMoreThanOneOutput : forall f1 f2,
moreThanOneOutput f1 -> noOutputs f2 -> moreThanOneOutput (appendAny f1 f2).
Lemma AppendSingleInput : forall f1 f2,
oneInput f1 -> noInputs f2 -> oneInput (appendAny f1 f2).
Lemma AppendNoInputOrOutput : forall f1 f2,
noInputOrOutput f1 -> noInputOrOutput f2 -> noInputOrOutput (appendAny f1 f2).
Lemma SplitNoInputOrOutput : forall f1 f2,
noInputOrOutput (appendAny f1 f2) -> noInputOrOutput f1 -> noInputOrOutput f2.
Lemma noInputOrOutputMeansNoInputsAndNoOutputs: forall fs,
noInputOrOutput fs -> noInputs fs -> noOutputs fs.
Lemma noInputOrOutputMeansNoInputsAndNoOutputs2: forall fs,
noInputs fs -> noOutputs fs -> noInputOrOutput fs.
Lemma noInputOrOutputMeansNoInputsAndNoOutputs3: forall fs,
noInputs fs /\ noOutputs fs -> noInputOrOutput fs.
Lemma noInputOrOutputMeansNoInputsAndNoOutputs4: forall fs,
noInputOrOutput fs -> noInputs fs /\ noOutputs fs.
Lemma AppendOneInputXorOutput : forall f1 f2,
oneInputXorOutput f1 -> noInputOrOutput f2 -> oneInputXorOutput (appendAny f1 f2).
Lemma AppendOneInputXorOutput2 : forall f1 f2,
noInputOrOutput f1 -> oneInputXorOutput f2 -> oneInputXorOutput (appendAny f1 f2).
Lemma oneInputAndNoOutputsMeaning: forall fs,
oneInputAndNoOutputs fs -> oneInput fs -> noOutputs fs.
Lemma oneInputAndNoOutputsMeaning2: forall fs,
oneInputAndNoOutputs fs -> (oneInput fs /\ noOutputs fs).
Lemma oneInputAndNoOutputsMeaning3: forall fs,
(oneInput fs /\ noOutputs fs) -> oneInputAndNoOutputs fs.
Lemma noOutputsInputMeansNoInputs: forall fs,
noInputOrOutput fs -> noInputs fs.
Lemma noOutputsInputMeansNoOutputs: forall fs,
noInputOrOutput fs -> noOutputs fs.
Lemma noInputDoesNotMeanOneInput : forall fs,
noInputs fs /\ oneInput fs -> False.
Lemma noOutputDoesNotMeanOneOutput : forall fs,
noOutputs fs /\ oneOutput fs -> False.
Lemma noInputDoesNotMeanOneInput1 : forall fs,
noInputs fs -> oneInput fs -> False.
Lemma oneOrOtherXorIn : forall fs,
oneInputXorOutput fs -> oneInput fs -> noOutputs fs.
Lemma oneOrOtherXorOut : forall fs,
oneInputXorOutput fs -> oneOutput fs -> noInputs fs.
Lemma noOutOneInIsOneInXorOut : forall fs,
oneInput fs /\ noOutputs fs -> oneInputXorOutput fs.
Lemma noInImpliesHasInIsFalse : forall fs,
noInputs fs -> hasInput fs -> False.
Lemma noOutImpliesHasOutIsFalse : forall fs,
noOutputs fs -> hasOutput fs -> False.
Lemma maxOneInputXor : forall fs,
oneInputXorOutput fs -> hasInput fs -> oneInput fs.
Lemma noInAndHasInIsFalse : forall fs,
noInputs fs /\ hasInput fs -> False.
Lemma maxOneInputIfNoOutput : forall fs,
oneInputXorOutput fs -> hasInput fs -> oneInputAndNoOutputs fs.
Lemma maxOneOutputXor : forall fs,
oneInputXorOutput fs -> hasOutput fs -> oneOutput fs.
Lemma noOutputsMeansOneOrNo: forall fs,
noOutputs fs -> oneOrNoOutput fs.
Lemma oneOutputsInputMeansOneOrNo: forall fs,
oneInputXorOutput fs -> oneOrNoInputXorOutput fs.
Lemma noOutputsInputMeansOneOrNo: forall fs,
noInputOrOutput fs -> oneOrNoInputXorOutput fs.
Lemma oneOutputsMeansOneOrNo: forall fs,
oneOutput fs -> oneOrNoOutput fs.
Axiom outIsNotIn: forall trm t, IN t = OUT trm -> False.
Lemma outIsNotAsubListOfIn: forall trm t, subList [OUT trm] [IN t] -> False.
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.
Lemma noInputSubst : forall f sigma,
noInputs f -> noInputs (applySubFacts sigma f).
Lemma oneInputSubst : forall f sigma,
oneInput f -> oneInput (applySubFacts sigma f).
Lemma oneOutIsOneXorNo : forall fs,
oneOutput fs -> noInputs fs -> oneInputXorOutput fs.
Lemma subListToHasOutput : forall trm fs,
subList [OUT trm] fs -> hasOutput fs.
Lemma noOutMeansNoOutSubList : forall f1 trm,
subList [OUT trm] f1 -> noInputOrOutput f1 -> False.
Lemma InputToOutputMustHaveInput : forall f1 f2 sigma r l,
reduceWithGroundRule (applySubRule sigma r) f1 l f2
-> InputToOutputProtocolRule r -> hasInput f1.
Lemma StateToOutputNoOutputRule : forall r sigma f1 l f2,
noOutputs f1 -> StateToOutputProtocolRule r ->
reduceWithRuleSigma r sigma f1 l f2
-> oneOutput f2.
Axiom StateToStateoneOutputXorInputIs : forall r sigma f1 l f2 trms,
oneOutputXorInputIs f1 trms -> StateToStateProtocolRule r ->
reduceWithRuleSigma r sigma f1 l f2
-> oneOutputXorInputIs f2 trms.
Lemma StateToStateNoOutputRule : forall r sigma f1 l f2,
noInputOrOutput f1 -> StateToStateProtocolRule r ->
reduceWithRuleSigma r sigma f1 l f2
-> noInputOrOutput f2.
Lemma noInputOutputImpliesOneOutputIsTrue: forall fs,
noInputOrOutput fs -> oneOutput fs -> True.
Lemma oneOutputImpliesnoInputOutputIsFalse: forall fs,
oneOutput fs -> noInputOrOutput fs -> False.
Lemma StateToStateOneOutRule : forall r sigma f1 l f2,
oneOutput f1 -> StateToStateProtocolRule r ->
reduceWithRuleSigma r sigma f1 l f2
-> oneOutput f2.
Lemma StateToStateXorOutRule : forall r sigma f1 l f2,
oneInputXorOutput f1 -> StateToStateProtocolRule r ->
reduceWithRuleSigma r sigma f1 l f2
-> oneInputXorOutput f2.
Lemma InputToOutputOneOutRule : forall r sigma f1 l f2,
oneInputAndNoOutputs f1 -> InputToOutputProtocolRule r ->
reduceWithRuleSigma r sigma f1 l f2
-> oneOutput f2.
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.
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).
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).
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.
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.
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.
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).
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.
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).
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).
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).
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).
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.
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.
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.
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).
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).
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).
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).
noOutputs (f::fs) -> not (eq_fact (OUT t1) f) /\ noOutputs fs.
Lemma emptyRuleCantMakeOutput : forall sigma f1 label f2 ,
reduceWithRuleSigma (RuleProto [] label []) sigma f1 label f2
-> noOutputs f1 -> noOutputs f2.
Lemma sigmaNoInputFacts: forall f1 f2 sigma,
applySubFacts sigma f1 = f2 -> noInputs f2 -> noInputs f1.
Lemma sigmaNoInputFacts2: forall f1 f2 sigma,
applySubFacts sigma f1 = f2 -> noInputs f1 -> noInputs f2.
Lemma sigmaNoOutputFacts: forall f1 f2 sigma,
applySubFacts sigma f1 = f2 -> noOutputs f1 -> noOutputs f2.
Lemma sigmaNoOutputFacts2: forall f1 f2 sigma,
applySubFacts sigma f1 = f2 -> noOutputs f2 -> noOutputs f1.
Lemma sigmaNoInputOrOutputFacts: forall f1 f2 sigma,
applySubFacts sigma f1 = f2 -> noInputOrOutput f1 -> noInputOrOutput f2.
Lemma sigmaOneInputXorOutputFacts: forall f1 f2 sigma,
applySubFacts sigma f1 = f2 -> oneInputXorOutput f1 -> oneInputXorOutput f2.
Axiom sigmaoneOutputXorInputIsFacts: forall f1 f2 sigma trms,
applySubFacts sigma f1 = f2
-> oneOutputXorInputIs f1 trms -> oneOutputXorInputIs f2 trms.
Lemma sigmaOneInputFact: forall f1 f2 sigma,
applySubFacts sigma f1 = f2 -> oneInput f2 -> oneInput f1.
Lemma sigmaOneInputFact2: forall f1 f2 sigma,
applySubFacts sigma f1 = f2 -> oneInput f1 -> oneInput f2.
Lemma sigmaOneOutputFact: forall f1 f2 sigma,
applySubFacts sigma f1 = f2 -> oneOutput f1 -> oneOutput f2.
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.
Lemma ginstWithSigmaNoInputP: forall f1 f2 f3 f4 l1 l2 sigma,
ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
-> noInputs f3 -> noInputs f1.
Lemma ginstWithSigmaOneInputP: forall f1 f2 f3 f4 l1 l2 sigma,
ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
-> oneInput f3 -> oneInput f1.
Lemma ginstWithSigmaNoOutputC: forall f1 f2 f3 f4 l1 l2 sigma,
ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
-> noOutputs f4 -> noOutputs f2.
Lemma ginstWithSigmaNoOutputP: forall f1 f2 f3 f4 l1 l2 sigma,
ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
-> noOutputs f3 -> noOutputs f1.
Lemma ginstWithSigmaOneOutputC: forall f1 f2 f3 f4 l1 l2 sigma,
ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
-> oneOutput f4 -> oneOutput f2.
Lemma ginstWithSigmaMoreThanOneOutputC: forall f1 f2 f3 f4 l1 l2 sigma,
ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
-> moreThanOneOutput f4 -> moreThanOneOutput f2.
Lemma ginstWithSigmaNoInputOutputC: forall f1 f2 f3 f4 l1 l2 sigma,
ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
-> noInputOrOutput f4 -> noInputOrOutput f2.
Lemma ginstWithSigmaNoInputOutputP: forall f1 f2 f3 f4 l1 l2 sigma,
ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
-> noInputOrOutput f3 -> noInputOrOutput f1.
Lemma ginstWithSigmaOneInputXorOutputC: forall f1 f2 f3 f4 l1 l2 sigma,
ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
-> oneInputXorOutput f4 -> oneInputXorOutput f2.
Lemma ginstWithSigmaOneInputXorOutputP: forall f1 f2 f3 f4 l1 l2 sigma,
ginstWithSigma (RuleProto f1 l1 f2) sigma (RuleProto f3 l2 f4)
-> oneInputXorOutput f3 -> oneInputXorOutput f1.
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.
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.
Lemma noOutputsTail : forall f fs,
noOutputs (f::fs) -> noOutputs fs.
Lemma noInputsTail : forall f fs,
noInputs (f::fs) -> noInputs fs.
Lemma noInputOrOutputTail : forall f fs,
noInputOrOutput (f::fs) -> noInputOrOutput fs.
Lemma noOutputsAcrossRemoveFact : forall f fs,
noOutputs fs -> noOutputs (removeFact f fs).
Lemma noOutputsAcrossRemove : forall f1 f2,
noOutputs f2 -> noOutputs (removeFacts f1 f2).
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).
Lemma noInputOrOutputAcrossRemoveFact : forall f fs,
noInputOrOutput fs -> noInputOrOutput (removeFact f fs).
Lemma noInputsAcrossRemove : forall f1 f2,
noInputs f2 -> noInputs (removeFacts f1 f2).
Lemma noInputOrOutputAcrossRemove : forall f1 f2,
noInputOrOutput f2 -> noInputOrOutput (removeFacts f1 f2).
Lemma AppendNoOutputs : forall f1 f2,
noOutputs f1 -> noOutputs f2 -> noOutputs (appendAny f1 f2).
Lemma AppendNoInputs : forall f1 f2,
noInputs f1 -> noInputs f2 -> noInputs (appendAny f1 f2).
Lemma AppendSingleOutput : forall f1 f2,
oneOutput f1 -> noOutputs f2 -> oneOutput (appendAny f1 f2).
Lemma AppendSingleOutput2 : forall f1 f2,
oneOutput f2 -> noOutputs f1 -> oneOutput (appendAny f1 f2).
Lemma AppendMinOneOutput : forall f1 f2,
minOneOutput f1 -> noOutputs f2 -> minOneOutput (appendAny f1 f2).
Lemma AppendMoreThanOneOutput : forall f1 f2,
moreThanOneOutput f1 -> noOutputs f2 -> moreThanOneOutput (appendAny f1 f2).
Lemma AppendSingleInput : forall f1 f2,
oneInput f1 -> noInputs f2 -> oneInput (appendAny f1 f2).
Lemma AppendNoInputOrOutput : forall f1 f2,
noInputOrOutput f1 -> noInputOrOutput f2 -> noInputOrOutput (appendAny f1 f2).
Lemma SplitNoInputOrOutput : forall f1 f2,
noInputOrOutput (appendAny f1 f2) -> noInputOrOutput f1 -> noInputOrOutput f2.
Lemma noInputOrOutputMeansNoInputsAndNoOutputs: forall fs,
noInputOrOutput fs -> noInputs fs -> noOutputs fs.
Lemma noInputOrOutputMeansNoInputsAndNoOutputs2: forall fs,
noInputs fs -> noOutputs fs -> noInputOrOutput fs.
Lemma noInputOrOutputMeansNoInputsAndNoOutputs3: forall fs,
noInputs fs /\ noOutputs fs -> noInputOrOutput fs.
Lemma noInputOrOutputMeansNoInputsAndNoOutputs4: forall fs,
noInputOrOutput fs -> noInputs fs /\ noOutputs fs.
Lemma AppendOneInputXorOutput : forall f1 f2,
oneInputXorOutput f1 -> noInputOrOutput f2 -> oneInputXorOutput (appendAny f1 f2).
Lemma AppendOneInputXorOutput2 : forall f1 f2,
noInputOrOutput f1 -> oneInputXorOutput f2 -> oneInputXorOutput (appendAny f1 f2).
Lemma oneInputAndNoOutputsMeaning: forall fs,
oneInputAndNoOutputs fs -> oneInput fs -> noOutputs fs.
Lemma oneInputAndNoOutputsMeaning2: forall fs,
oneInputAndNoOutputs fs -> (oneInput fs /\ noOutputs fs).
Lemma oneInputAndNoOutputsMeaning3: forall fs,
(oneInput fs /\ noOutputs fs) -> oneInputAndNoOutputs fs.
Lemma noOutputsInputMeansNoInputs: forall fs,
noInputOrOutput fs -> noInputs fs.
Lemma noOutputsInputMeansNoOutputs: forall fs,
noInputOrOutput fs -> noOutputs fs.
Lemma noInputDoesNotMeanOneInput : forall fs,
noInputs fs /\ oneInput fs -> False.
Lemma noOutputDoesNotMeanOneOutput : forall fs,
noOutputs fs /\ oneOutput fs -> False.
Lemma noInputDoesNotMeanOneInput1 : forall fs,
noInputs fs -> oneInput fs -> False.
Lemma oneOrOtherXorIn : forall fs,
oneInputXorOutput fs -> oneInput fs -> noOutputs fs.
Lemma oneOrOtherXorOut : forall fs,
oneInputXorOutput fs -> oneOutput fs -> noInputs fs.
Lemma noOutOneInIsOneInXorOut : forall fs,
oneInput fs /\ noOutputs fs -> oneInputXorOutput fs.
Lemma noInImpliesHasInIsFalse : forall fs,
noInputs fs -> hasInput fs -> False.
Lemma noOutImpliesHasOutIsFalse : forall fs,
noOutputs fs -> hasOutput fs -> False.
Lemma maxOneInputXor : forall fs,
oneInputXorOutput fs -> hasInput fs -> oneInput fs.
Lemma noInAndHasInIsFalse : forall fs,
noInputs fs /\ hasInput fs -> False.
Lemma maxOneInputIfNoOutput : forall fs,
oneInputXorOutput fs -> hasInput fs -> oneInputAndNoOutputs fs.
Lemma maxOneOutputXor : forall fs,
oneInputXorOutput fs -> hasOutput fs -> oneOutput fs.
Lemma noOutputsMeansOneOrNo: forall fs,
noOutputs fs -> oneOrNoOutput fs.
Lemma oneOutputsInputMeansOneOrNo: forall fs,
oneInputXorOutput fs -> oneOrNoInputXorOutput fs.
Lemma noOutputsInputMeansOneOrNo: forall fs,
noInputOrOutput fs -> oneOrNoInputXorOutput fs.
Lemma oneOutputsMeansOneOrNo: forall fs,
oneOutput fs -> oneOrNoOutput fs.
Axiom outIsNotIn: forall trm t, IN t = OUT trm -> False.
Lemma outIsNotAsubListOfIn: forall trm t, subList [OUT trm] [IN t] -> False.
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.
Lemma noInputSubst : forall f sigma,
noInputs f -> noInputs (applySubFacts sigma f).
Lemma oneInputSubst : forall f sigma,
oneInput f -> oneInput (applySubFacts sigma f).
Lemma oneOutIsOneXorNo : forall fs,
oneOutput fs -> noInputs fs -> oneInputXorOutput fs.
Lemma subListToHasOutput : forall trm fs,
subList [OUT trm] fs -> hasOutput fs.
Lemma noOutMeansNoOutSubList : forall f1 trm,
subList [OUT trm] f1 -> noInputOrOutput f1 -> False.
Lemma InputToOutputMustHaveInput : forall f1 f2 sigma r l,
reduceWithGroundRule (applySubRule sigma r) f1 l f2
-> InputToOutputProtocolRule r -> hasInput f1.
Lemma StateToOutputNoOutputRule : forall r sigma f1 l f2,
noOutputs f1 -> StateToOutputProtocolRule r ->
reduceWithRuleSigma r sigma f1 l f2
-> oneOutput f2.
Axiom StateToStateoneOutputXorInputIs : forall r sigma f1 l f2 trms,
oneOutputXorInputIs f1 trms -> StateToStateProtocolRule r ->
reduceWithRuleSigma r sigma f1 l f2
-> oneOutputXorInputIs f2 trms.
Lemma StateToStateNoOutputRule : forall r sigma f1 l f2,
noInputOrOutput f1 -> StateToStateProtocolRule r ->
reduceWithRuleSigma r sigma f1 l f2
-> noInputOrOutput f2.
Lemma noInputOutputImpliesOneOutputIsTrue: forall fs,
noInputOrOutput fs -> oneOutput fs -> True.
Lemma oneOutputImpliesnoInputOutputIsFalse: forall fs,
oneOutput fs -> noInputOrOutput fs -> False.
Lemma StateToStateOneOutRule : forall r sigma f1 l f2,
oneOutput f1 -> StateToStateProtocolRule r ->
reduceWithRuleSigma r sigma f1 l f2
-> oneOutput f2.
Lemma StateToStateXorOutRule : forall r sigma f1 l f2,
oneInputXorOutput f1 -> StateToStateProtocolRule r ->
reduceWithRuleSigma r sigma f1 l f2
-> oneInputXorOutput f2.
Lemma InputToOutputOneOutRule : forall r sigma f1 l f2,
oneInputAndNoOutputs f1 -> InputToOutputProtocolRule r ->
reduceWithRuleSigma r sigma f1 l f2
-> oneOutput f2.
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.
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).
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).
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.
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.
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.
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).
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.
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).
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).
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).
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).
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.
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.
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.
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).
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).
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).
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).
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
Global Index
S
Sec9_LemmasOnWellformedness [library]Library Index
S
Sec9_LemmasOnWellformedness| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
This page has been generated by coqdoc