Nuprl Lemma : dl-box-comp

a,b:Prog. ∀phi:Prop.  ([(a;b)] phi ⇐⇒ [a] [b] phi)


Proof




Definitions occuring in Statement :  dl-equiv: (phi ⇐⇒ psi) dl-box: [x1] x dl-comp: (x1;x) dl-prop: Prop dl-prog: Prog all: x:A. B[x]
Definitions unfolded in proof :  all: x:A. B[x] dl-equiv: (phi ⇐⇒ psi) and: P ∧ Q dl-valid: |= phi dl-prop-sem: [|phi|] dl-sem: dl-sem(K;n.R[n];m.P[m]) uall: [x:A]. B[x] so_lambda: λ2x.t[x] member: t ∈ T 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] dl-prog-sem: [|alpha|] implies:  Q exists: x:A. B[x] cand: c∧ B subtype_rel: A ⊆B prop: guard: {T}
Lemmas referenced :  dl-ind-dl-implies istype-void dl-ind-dl-box dl-ind-dl-comp dl-prog-sem_wf istype-nat subtype_rel_self dl-prop-sem_wf istype-universe dl-prop_wf dl-prog_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt independent_pairFormation sqequalRule cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin isect_memberEquality_alt voidElimination hypothesis dependent_functionElimination hypothesisEquality independent_functionElimination dependent_pairFormation_alt productIsType universeIsType applyEquality lambdaEquality_alt instantiate universeEquality because_Cache functionIsType productElimination inhabitedIsType

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



Date html generated: 2019_10_15-AM-11_44_35
Last ObjectModification: 2019_03_27-AM-00_37_25

Theory : dynamic!logic


Home Index