Nuprl Lemma : dl-aprog-1_wf

[x:Prog]. dl-aprog-1(x) ∈ ℕ supposing ↑dl-aprog?(x)


Proof




Definitions occuring in Statement :  dl-aprog-1: dl-aprog-1(x) dl-aprog?: dl-aprog?(x) dl-prog: Prog nat: assert: b uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T dl-prog: Prog mrec: mrec(L;i) so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] ext-eq: A ≡ B and: P ∧ Q subtype_rel: A ⊆B all: x:A. B[x] eager-map: eager-map(f;as) list_ind: list_ind outl: outl(x) 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) nil: [] it: iff: ⇐⇒ Q implies:  Q or: P ∨ Q sq_type: SQType(T) guard: {T} mrec-spec: mrec-spec(L;lbl;p) top: Top mk-prec: mk-prec(lbl;x) dl-aprog: atm(x) assert: b dl-aprog?: dl-aprog?(x) dl-label: dl-label(d) mobj-label: mobj-label(x) prec-label: prec-label(x) mobj-data: mobj-data(x) dl-prog-obj: prog(x) true: True dl-aprog-1: dl-aprog-1(x) select-tuple: x.n eq_int: (i =z j) bfalse: ff dl-comp: (x1;x) false: False dl-choose: x1 ⋃ x dl-iterate: (x)* dl-prop: Prop dl-test: (x)?
Lemmas referenced :  prec-ext mrec-spec_wf dl-Spec_wf istype-atom mrec-label-cases1-ext cons_member cons_wf nil_wf subtype_base_sq atom_subtype_base atomdeq_reduce_lemma istype-void map_cons_lemma map_nil_lemma tupletype_cons_lemma null_nil_lemma tupletype_nil_lemma null_cons_lemma member_singleton istype-assert dl-aprog?_wf dl-prog_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut sqequalHypSubstitution introduction extract_by_obid isectElimination thin atomEquality sqequalRule lambdaEquality_alt hypothesis hypothesisEquality inhabitedIsType tokenEquality promote_hyp hypothesis_subsumption productElimination applyEquality dependent_functionElimination setElimination rename independent_functionElimination unionElimination instantiate cumulativity independent_isectElimination equalityTransitivity equalitySymmetry isect_memberEquality_alt voidElimination equalityElimination universeIsType

Latex:
\mforall{}[x:Prog].  dl-aprog-1(x)  \mmember{}  \mBbbN{}  supposing  \muparrow{}dl-aprog?(x)



Date html generated: 2019_10_15-AM-11_40_41
Last ObjectModification: 2019_03_26-AM-11_24_43

Theory : dynamic!logic


Home Index