Nuprl Lemma : dl-aprog_wf

[x:ℕ]. (atm(x) ∈ Prog)


Proof




Definitions occuring in Statement :  dl-aprog: atm(x) dl-prog: Prog nat: uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] dl-prog: Prog dl-aprog: atm(x) member: t ∈ T subtype_rel: A ⊆B nat: 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) btrue: tt pi2: snd(t) null: null(as) nil: [] it: so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] 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 subtype_rel_self tuple-type_wf prec-arg-types_wf mrec-spec_wf istype-atom istype-nat
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt sqequalRule cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis closedConclusion tokenEquality hypothesisEquality applyEquality atomEquality lambdaEquality_alt inhabitedIsType independent_isectElimination independent_pairFormation natural_numberEquality imageMemberEquality baseClosed

Latex:
\mforall{}[x:\mBbbN{}].  (atm(x)  \mmember{}  Prog)



Date html generated: 2019_10_15-AM-11_39_18
Last ObjectModification: 2019_03_26-AM-11_24_04

Theory : dynamic!logic


Home Index