Nuprl Lemma : rtermAdd?_wf

[v:rat_term()]. (rtermAdd?(v) ∈ 𝔹)


Proof




Definitions occuring in Statement :  rtermAdd?: rtermAdd?(v) rat_term: rat_term() bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T ext-eq: A ≡ B and: P ∧ Q subtype_rel: A ⊆B all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) uimplies: supposing a sq_type: SQType(T) guard: {T} eq_atom: =a y ifthenelse: if then else fi  rtermConstant: "const" rtermAdd?: rtermAdd?(v) pi1: fst(t) bfalse: ff exists: x:A. B[x] or: P ∨ Q bnot: ¬bb assert: b false: False rtermVar: rtermVar(var) rtermAdd: left "+" right rtermSubtract: left "-" right rtermMultiply: left "*" right rtermDivide: num "/" denom rtermMinus: rtermMinus(num)
Lemmas referenced :  rat_term-ext eq_atom_wf eqtt_to_assert assert_of_eq_atom subtype_base_sq atom_subtype_base bfalse_wf eqff_to_assert bool_cases_sqequal bool_wf bool_subtype_base assert-bnot neg_assert_of_eq_atom btrue_wf rat_term_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut introduction extract_by_obid promote_hyp sqequalHypSubstitution productElimination thin hypothesis_subsumption hypothesis hypothesisEquality applyEquality sqequalRule isectElimination tokenEquality inhabitedIsType lambdaFormation_alt unionElimination equalityElimination equalityTransitivity equalitySymmetry independent_isectElimination instantiate cumulativity atomEquality dependent_functionElimination independent_functionElimination because_Cache dependent_pairFormation_alt equalityIstype voidElimination universeIsType

Latex:
\mforall{}[v:rat\_term()].  (rtermAdd?(v)  \mmember{}  \mBbbB{})



Date html generated: 2019_10_29-AM-09_27_59
Last ObjectModification: 2019_03_31-PM-05_24_39

Theory : reals


Home Index