Nuprl Lemma : rat_term_wf

rat_term() ∈ Type


Proof




Definitions occuring in Statement :  rat_term: rat_term() member: t ∈ T universe: Type
Definitions unfolded in proof :  rat_term: rat_term() member: t ∈ T uall: [x:A]. B[x] uimplies: supposing a nat: so_lambda: λ2x.t[x] so_apply: x[s] prop:
Lemmas referenced :  rat_termco_wf has-value_wf-partial nat_wf set-value-type le_wf istype-int int-value-type rat_termco_size_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep setEquality cut introduction extract_by_obid hypothesis sqequalHypSubstitution isectElimination thin independent_isectElimination intEquality lambdaEquality_alt natural_numberEquality hypothesisEquality

Latex:
rat\_term()  \mmember{}  Type



Date html generated: 2019_10_29-AM-09_25_17
Last ObjectModification: 2019_03_31-PM-05_24_00

Theory : reals


Home Index