Nuprl Lemma : basic-seq-1-2

{

[s:SES].

[pas:Id

Id

Atom1

(ProtocolAction List)].
(A

B: pas[A;B;m;n]

Basic1) }

{ Proof }

Definitions occuring in Statement : basic-seq-1-2: A

B: pas[A; B; m; n], ses-basic-sequence1: Basic1, protocol-action: ProtocolAction, security-event-structure: SES, Id: Id, uall:

[x:A]. B[x], so_apply: x[s1;s2;s3;s4], member: t

T, function: x:A

B[x], list: type List, atom: Atom$n
Definitions : uall:

[x:A]. B[x], member: t

T, ses-basic-sequence1: Basic1, basic-seq-1-2: A

B: pas[A; B; m; n], so_apply: x[s1;s2;s3;s4], exists:

x:A. B[x], prop:

Lemmas : ses-is-protocol-actions_wf, ses-thread_wf, event-ordering+_wf, ses-info_wf, Id_wf, protocol-action_wf, security-event-structure_wf

\mforall{}[s:SES]. \mforall{}[pas:Id {}\mrightarrow{} Id {}\mrightarrow{} Atom1 {}\mrightarrow{} Atom1 {}\mrightarrow{} (ProtocolAction List)]. (A {}\mrightarrow{} B: pas[A;B;m;n] \mmember{} Basic1) Date html generated: 2011_08_17-PM-07_42_19 Last ObjectModification: 2011_06_18-PM-01_36_17 Home Index