Nuprl Lemma : rtermMinus_wf

[num:rat_term()]. (rtermMinus(num) ∈ rat_term())


Proof




Definitions occuring in Statement :  rtermMinus: rtermMinus(num) rat_term: rat_term() uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T rat_term: rat_term() rtermMinus: rtermMinus(num) eq_atom: =a y ifthenelse: if then else fi  bfalse: ff btrue: tt subtype_rel: A ⊆B ext-eq: A ≡ B and: P ∧ Q rat_termco_size: rat_termco_size(p) rat_term_size: rat_term_size(p) nat: all: x:A. B[x] decidable: Dec(P) or: P ∨ Q uimplies: supposing a not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top prop: false: False so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  rat_termco-ext ifthenelse_wf eq_atom_wf rat_termco_wf add_nat_wf decidable__le full-omega-unsat intformnot_wf intformle_wf itermConstant_wf istype-int int_formula_prop_not_lemma istype-void int_formula_prop_le_lemma int_term_value_constant_lemma int_formula_prop_wf istype-le rat_term_size_wf value-type-has-value nat_wf set-value-type le_wf int-value-type istype-universe has-value_wf-partial rat_termco_size_wf rat_term_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut dependent_set_memberEquality_alt introduction extract_by_obid hypothesis sqequalRule dependent_pairEquality_alt tokenEquality sqequalHypSubstitution setElimination thin rename hypothesisEquality universeIsType instantiate isectElimination universeEquality intEquality productEquality voidEquality applyEquality productElimination natural_numberEquality dependent_functionElimination unionElimination independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt isect_memberEquality_alt voidElimination inhabitedIsType lambdaFormation_alt equalityIstype equalityTransitivity equalitySymmetry

Latex:
\mforall{}[num:rat\_term()].  (rtermMinus(num)  \mmember{}  rat\_term())



Date html generated: 2019_10_29-AM-09_26_58
Last ObjectModification: 2019_03_31-PM-05_24_23

Theory : reals


Home Index