Nuprl Lemma : dl-diamond_wf

[x1:Prog]. ∀[x:Prop].  (<x1> x ∈ Prop)


Proof




Definitions occuring in Statement :  dl-diamond: <x1> x dl-prop: Prop dl-prog: Prog uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] dl-prop: Prop dl-diamond: <x1> x member: t ∈ T tuple-type: tuple-type(L) list_ind: list_ind prec-arg-types: prec-arg-types(lbl,p.a[lbl; p];i;lbl) map: map(f;as) mrec-spec: mrec-spec(L;lbl;p) apply-alist: apply-alist(eq;L;x) dl-Spec: dl-Spec() cons: [a b] ifthenelse: if then else fi  atom-deq: AtomDeq eq_atom: =a y pi1: fst(t) bfalse: ff btrue: tt pi2: snd(t) null: null(as) prec: prec(lbl,p.a[lbl; p];i) dl-prog: Prog mrec: mrec(L;i) nil: [] it: uimplies: supposing a less_than: a < b squash: T less_than': less_than'(a;b) length: ||as|| true: True and: P ∧ Q
Lemmas referenced :  mk-prec_wf-mrec dl-Spec_wf dl-prop_wf dl-prog_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt sqequalRule cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis closedConclusion tokenEquality independent_pairEquality hypothesisEquality independent_isectElimination independent_pairFormation natural_numberEquality imageMemberEquality baseClosed universeIsType

Latex:
\mforall{}[x1:Prog].  \mforall{}[x:Prop].    (<x1>  x  \mmember{}  Prop)



Date html generated: 2019_10_15-AM-11_39_56
Last ObjectModification: 2019_03_26-AM-11_24_39

Theory : dynamic!logic


Home Index