Nuprl Lemma : dl-box-iterate

a:Prog. ∀phi:Prop.  ([(a)*] phi ⇐⇒ phi ∧ [a] [(a)*] phi)


Proof




Definitions occuring in Statement :  dl-equiv: (phi ⇐⇒ psi) dl-box: [x1] x dl-and: x1 ∧ x dl-iterate: (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 cand: c∧ B subtype_rel: A ⊆B prop: or: P ∨ Q exists: x:A. B[x] infix_ap: y iff: ⇐⇒ Q rev_implies:  Q guard: {T}
Lemmas referenced :  dl-ind-dl-implies istype-void dl-ind-dl-box dl-ind-dl-iterate dl-ind-dl-and rel_star_wf dl-prog-sem_wf istype-nat subtype_rel_self dl-prop-sem_wf istype-universe dl-prop_wf dl-prog_wf rel_star_iff2
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 universeIsType applyEquality hypothesisEquality lambdaEquality_alt instantiate universeEquality because_Cache functionIsType productElimination productIsType dependent_functionElimination independent_functionElimination inrFormation_alt inhabitedIsType inlFormation_alt dependent_pairFormation_alt equalityIstype unionElimination hyp_replacement equalitySymmetry

Latex:
\mforall{}a:Prog.  \mforall{}phi:Prop.    ([(a)*]  phi  \mLeftarrow{}{}\mRightarrow{}  phi  \mwedge{}  [a]  [(a)*]  phi)



Date html generated: 2019_10_15-AM-11_44_49
Last ObjectModification: 2019_03_27-AM-00_54_18

Theory : dynamic!logic


Home Index