Nuprl Lemma : ses-flow-induction
∀s:SES. ∀es:EO+(Info).
∀[P:E ⟶ E ⟶ Atom1 ⟶ ℙ]
((∀e1,e2:E.
((∀x,y:E.
(e1 c≤ x ⇒ x c≤ y ⇒ y c≤ e2 ⇒ ((e1 < x) ∨ (y < e2)) ⇒ (∀a:Atom1. (ses-flow(s;es;a;x;y) ⇒ P[x;y;a]))))
⇒ (∀a:Atom1. (ses-flow(s;es;a;e1;e2) ⇒ P[e1;e2;a]))))
⇒ {∀e1,e2:E. ∀a:Atom1. (ses-flow(s;es;a;e1;e2) ⇒ P[e1;e2;a])})
Proof
Definitions occuring in Statement :
ses-flow: ses-flow(s;es;a;e1;e2),
ses-info: Info,
security-event-structure: SES,
event-ordering+: EO+(Info),
es-causle: e c≤ e',
es-causl: (e < e'),
es-E: E,
atom: Atom$n,
uall: ∀[x:A]. B[x],
prop: ℙ,
guard: {T},
so_apply: x[s1;s2;s3],
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
function: x:A ⟶ B[x]
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
member: t ∈ T,
prop: ℙ,
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
or: P ∨ Q,
so_apply: x[s1;s2;s3],
so_apply: x[s],
guard: {T},
int_seg: {i..j-},
lelt: i ≤ j < k,
and: P ∧ Q,
uimplies: b supposing a,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
false: False,
not: ¬A,
top: Top,
decidable: Dec(P),
le: A ≤ B,
less_than': less_than'(a;b),
nat: ℕ,
ge: i ≥ j ,
less_than: a < b,
squash: ↓T,
ses-flow: ses-flow(s;es;a;e1;e2),
ycomb: Y,
es-E-interface: E(X)
Latex:
\mforall{}s:SES. \mforall{}es:EO+(Info).
\mforall{}[P:E {}\mrightarrow{} E {}\mrightarrow{} Atom1 {}\mrightarrow{} \mBbbP{}]
((\mforall{}e1,e2:E.
((\mforall{}x,y:E.
(e1 c\mleq{} x
{}\mRightarrow{} x c\mleq{} y
{}\mRightarrow{} y c\mleq{} e2
{}\mRightarrow{} ((e1 < x) \mvee{} (y < e2))
{}\mRightarrow{} (\mforall{}a:Atom1. (ses-flow(s;es;a;x;y) {}\mRightarrow{} P[x;y;a]))))
{}\mRightarrow{} (\mforall{}a:Atom1. (ses-flow(s;es;a;e1;e2) {}\mRightarrow{} P[e1;e2;a]))))
{}\mRightarrow{} \{\mforall{}e1,e2:E. \mforall{}a:Atom1. (ses-flow(s;es;a;e1;e2) {}\mRightarrow{} P[e1;e2;a])\})
Date html generated:
2016_05_17-AM-11_47_14
Last ObjectModification:
2016_01_18-AM-07_46_45
Theory : event-logic-applications
Home
Index