Nuprl Lemma : dl-valid-diamond-dist-or2

a:Prog. ∀phi,psi:Prop.  (|= <a> phi ∨ <a> psi  |= <a> phi ∨ psi)


Proof




Definitions occuring in Statement :  dl-valid: |= phi dl-diamond: <x1> x dl-or: 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: |= 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|] prop: or: P ∨ Q exists: x:A. B[x] and: P ∧ Q cand: c∧ B subtype_rel: A ⊆B
Lemmas referenced :  istype-void istype-atom istype-universe dl-valid_wf dl-prop-sem_wf subtype_rel_self dl-prog-sem_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt sqequalHypSubstitution sqequalRule cut introduction extract_by_obid isectElimination thin isect_memberEquality_alt voidElimination hypothesis dependent_functionElimination hypothesisEquality universeIsType functionIsType universeEquality because_Cache instantiate inhabitedIsType unionElimination productElimination dependent_pairFormation_alt independent_pairFormation inlFormation_alt applyEquality lambdaEquality_alt productIsType unionIsType inrFormation_alt

Latex:
\mforall{}a:Prog.  \mforall{}phi,psi:Prop.    (|=  <a>  phi  \mvee{}  <a>  psi  {}\mRightarrow{}  |=  <a>  phi  \mvee{}  psi)



Date html generated: 2019_10_15-AM-11_44_57
Last ObjectModification: 2019_03_26-AM-11_28_34

Theory : dynamic!logic


Home Index