Nuprl Lemma : dl-valid-box-comp-double-box

a,b:Prog. ∀phi:Prop.  (|= [(a;b)] phi  |= [a] [b] phi)


Proof




Definitions occuring in Statement :  dl-valid: |= phi dl-box: [x1] x dl-comp: (x1;x) dl-prop: Prop dl-prog: Prog all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q dl-valid: Error :dl-valid,  member: t ∈ T dl-sem: Error :dl-sem,  uall: [x:A]. B[x] so_lambda: λ2x.t[x] top: Top so_apply: x[s] so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]) so_apply: x[s1;s2;s3;s4] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] exists: x:A. B[x] and: P ∧ Q cand: c∧ B pi1: fst(t) subtype_rel: A ⊆B prop:
Lemmas referenced :  istype-void istype-atom subtype_rel_self istype-universe
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt sqequalHypSubstitution cut hypothesis dependent_functionElimination thin hypothesisEquality sqequalRule introduction extract_by_obid isectElimination isect_memberEquality_alt voidElimination independent_functionElimination dependent_pairFormation_alt independent_pairFormation productIsType universeIsType applyEquality lambdaEquality_alt inhabitedIsType productElimination equalityIstype equalityTransitivity equalitySymmetry instantiate universeEquality because_Cache functionIsType

Latex:
\mforall{}a,b:Prog.  \mforall{}phi:Prop.    (|=  [(a;b)]  phi  {}\mRightarrow{}  |=  [a]  [b]  phi)



Date html generated: 2019_10_15-AM-11_45_19
Last ObjectModification: 2019_03_26-AM-11_28_43

Theory : dynamic!logic


Home Index