Nuprl Lemma : dlo-refl
∀a:dl-Obj(). (↑a ≤ a)
Proof
Definitions occuring in Statement :
dlo_le: a ≤ b,
dl-Obj: dl-Obj(),
assert: ↑b,
all: ∀x:A. B[x]
Definitions unfolded in proof :
dl-induction,
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
member: t ∈ T,
subtype_rel: A ⊆r B,
prop: ℙ,
so_apply: x[s],
implies: P ⇒ Q,
dlo_le: a ≤ b,
dlo-le: dlo-le(),
top: Top,
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),
so_apply: x[s1;s2;s3;s4],
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
all: ∀x:A. B[x],
or: P ∨ Q,
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
uiff: uiff(P;Q),
rev_uimplies: rev_uimplies(P;Q),
uimplies: b supposing a,
assert: ↑b,
ifthenelse: if b then t else f fi ,
dlo_eq: dlo_eq(a;b),
dlo-eq: dlo-eq(),
dl-ind: dl-ind,
mrec_ind: mrec_ind(L;h;x),
dl-prop-obj: prop(x),
genrec-ap: genrec-ap,
decidable__atom_equal,
eq_atom: x =a y,
pi1: fst(t),
dl-false: 0,
mk-prec: mk-prec(lbl;x),
bfalse: ff,
bool_cases_sqequal,
btrue: tt,
band: p ∧b q,
dl-kind: dl-kind(d),
mobj-kind: mobj-kind(x),
dl-false?: dl-false?(x),
dl-label: dl-label(d),
mobj-label: mobj-label(x),
prec-label: prec-label(x),
mobj-data: mobj-data(x),
pi2: snd(t),
dl-obj-prop: dl-obj-prop(x),
true: True
Lemmas referenced :
dl-induction,
assert_wf,
dlo_le_wf,
subtype-TYPE,
dl-Obj_wf,
dl-ind-dl-aprog,
istype-void,
istype-nat,
dl-ind-dl-comp,
iff_transitivity,
bor_wf,
dl-prog-obj_wf,
dl-comp_wf,
dlo_eq_wf,
iff_weakening_uiff,
assert_of_bor,
istype-assert,
dl-prog_wf,
dl-ind-dl-choose,
dl-choose_wf,
dl-ind-dl-iterate,
dl-iterate_wf,
dl-ind-dl-test,
dl-test_wf,
dl-prop-obj_wf,
dl-prop_wf,
dl-ind-dl-aprop,
dl-ind-dl-false,
dl-ind-dl-implies,
dl-implies_wf,
dl-ind-dl-and,
dl-and_wf,
dl-ind-dl-or,
dl-or_wf,
dl-ind-dl-box,
dl-box_wf,
dl-ind-dl-diamond,
dl-diamond_wf,
dl-aprog_wf,
dl-aprop_wf,
assert-dlo_eq,
decidable__atom_equal,
bool_cases_sqequal
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isectElimination,
thin,
sqequalRule,
lambdaEquality_alt,
hypothesisEquality,
hypothesis,
applyEquality,
universeIsType,
independent_functionElimination,
isect_memberEquality_alt,
voidElimination,
lambdaFormation_alt,
dependent_functionElimination,
unionEquality,
because_Cache,
independent_pairFormation,
unionElimination,
inlFormation_alt,
productElimination,
inrFormation_alt,
unionIsType,
inhabitedIsType,
independent_isectElimination,
natural_numberEquality,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}a:dl-Obj(). (\muparrow{}a \mleq{} a)
Date html generated:
2019_10_15-AM-11_43_20
Last ObjectModification:
2019_04_12-PM-05_26_59
Theory : dynamic!logic
Home
Index