Nuprl Lemma : rat_term_ind_wf
∀[A:Type]. ∀[R:A ⟶ rat_term() ⟶ ℙ]. ∀[v:rat_term()]. ∀[Constant:const:ℤ ⟶ {x:A| R[x;"const"]} ].
∀[Var:var:ℤ ⟶ {x:A| R[x;rtermVar(var)]} ]. ∀[Add:left:rat_term()
⟶ right:rat_term()
⟶ {x:A| R[x;left]}
⟶ {x:A| R[x;right]}
⟶ {x:A| R[x;left "+" right]} ]. ∀[Subtract:left:rat_term()
⟶ right:rat_term()
⟶ {x:A| R[x;left]}
⟶ {x:A| R[x;right]}
⟶ {x:A|
R[x;left "-" right]} ].
∀[Multiply:left:rat_term() ⟶ right:rat_term() ⟶ {x:A| R[x;left]} ⟶ {x:A| R[x;right]} ⟶ {x:A| R[x;left "*" right]} \000C].
∀[Divide:num:rat_term() ⟶ denom:rat_term() ⟶ {x:A| R[x;num]} ⟶ {x:A| R[x;denom]} ⟶ {x:A| R[x;num "/" denom]} ].
∀[Minus:num:rat_term() ⟶ {x:A| R[x;num]} ⟶ {x:A| R[x;rtermMinus(num)]} ].
(rat_term_ind(v;
rtermConstant(const)⇒ Constant[const];
rtermVar(var)⇒ Var[var];
rtermAdd(left,right)⇒ rec1,rec2.Add[left;right;rec1;rec2];
rtermSubtract(left,right)⇒ rec3,rec4.Subtract[left;right;rec3;rec4];
rtermMultiply(left,right)⇒ rec5,rec6.Multiply[left;right;rec5;rec6];
rtermDivide(num,denom)⇒ rec7,rec8.Divide[num;denom;rec7;rec8];
rtermMinus(num)⇒ rec9.Minus[num;rec9]) ∈ {x:A| R[x;v]} )
Proof
Definitions occuring in Statement :
rat_term_ind: rat_term_ind,
rtermMinus: rtermMinus(num),
rtermDivide: num "/" denom,
rtermMultiply: left "*" right,
rtermSubtract: left "-" right,
rtermAdd: left "+" right,
rtermVar: rtermVar(var),
rtermConstant: "const",
rat_term: rat_term(),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s1;s2;s3;s4],
so_apply: x[s1;s2],
so_apply: x[s],
member: t ∈ T,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
int: ℤ,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
rat_term_ind: rat_term_ind,
so_apply: x[s1;s2],
so_apply: x[s1;s2;s3;s4],
so_apply: x[s],
rat_term-definition,
rat_term-induction,
uniform-comp-nat-induction,
rat_term-ext,
eq_atom: x =a y,
btrue: tt,
it: ⋅,
bfalse: ff,
bool_cases_sqequal,
eqff_to_assert,
any: any x,
top: Top,
all: ∀x:A. B[x],
implies: P ⇒ Q,
has-value: (a)↓,
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),
so_lambda: λ2x.t[x],
uimplies: b supposing a,
subtype_rel: A ⊆r B,
prop: ℙ,
guard: {T}
Lemmas referenced :
rat_term-definition,
istype-void,
has-value_wf_base,
is-exception_wf,
lifting-strict-atom_eq,
strict4-decide,
istype-int,
rtermConstant_wf,
rtermVar_wf,
rtermAdd_wf,
rtermSubtract_wf,
rtermMultiply_wf,
rtermDivide_wf,
rtermMinus_wf,
rat_term_wf,
all_wf,
set_wf,
subtype_rel_self,
istype-universe,
rat_term-induction,
uniform-comp-nat-induction,
rat_term-ext,
bool_cases_sqequal,
eqff_to_assert
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
cut,
sqequalRule,
isect_memberEquality_alt,
voidElimination,
introduction,
extract_by_obid,
hypothesis,
inhabitedIsType,
lambdaFormation_alt,
thin,
sqequalSqle,
divergentSqle,
callbyvalueDecide,
sqequalHypSubstitution,
hypothesisEquality,
unionElimination,
sqleReflexivity,
equalityIstype,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
independent_functionElimination,
decideExceptionCases,
axiomSqleEquality,
exceptionSqequal,
baseApply,
closedConclusion,
baseClosed,
isectElimination,
independent_isectElimination,
lambdaEquality_alt,
isectIsType,
functionIsType,
universeIsType,
universeEquality,
setIsType,
because_Cache,
applyEquality,
functionEquality,
setEquality,
instantiate,
functionExtensionality,
intEquality,
setElimination,
rename,
dependent_set_memberEquality_alt
Latex:
\mforall{}[A:Type]. \mforall{}[R:A {}\mrightarrow{} rat\_term() {}\mrightarrow{} \mBbbP{}]. \mforall{}[v:rat\_term()]. \mforall{}[Constant:const:\mBbbZ{} {}\mrightarrow{} \{x:A| R[x;"const"]\} ].
\mforall{}[Var:var:\mBbbZ{} {}\mrightarrow{} \{x:A| R[x;rtermVar(var)]\} ]. \mforall{}[Add:left:rat\_term()
{}\mrightarrow{} right:rat\_term()
{}\mrightarrow{} \{x:A| R[x;left]\}
{}\mrightarrow{} \{x:A| R[x;right]\}
{}\mrightarrow{} \{x:A| R[x;left "+" right]\} ].
\mforall{}[Subtract:left:rat\_term()
{}\mrightarrow{} right:rat\_term()
{}\mrightarrow{} \{x:A| R[x;left]\}
{}\mrightarrow{} \{x:A| R[x;right]\}
{}\mrightarrow{} \{x:A| R[x;left "-" right]\} ]. \mforall{}[Multiply:left:rat\_term()
{}\mrightarrow{} right:rat\_term()
{}\mrightarrow{} \{x:A| R[x;left]\}
{}\mrightarrow{} \{x:A| R[x;right]\}
{}\mrightarrow{} \{x:A| R[x;left "*" right]\} ].
\mforall{}[Divide:num:rat\_term()
{}\mrightarrow{} denom:rat\_term()
{}\mrightarrow{} \{x:A| R[x;num]\}
{}\mrightarrow{} \{x:A| R[x;denom]\}
{}\mrightarrow{} \{x:A| R[x;num "/" denom]\} ]. \mforall{}[Minus:num:rat\_term()
{}\mrightarrow{} \{x:A| R[x;num]\}
{}\mrightarrow{} \{x:A| R[x;rtermMinus(num)]\} ].
(rat\_term\_ind(v;
rtermConstant(const){}\mRightarrow{} Constant[const];
rtermVar(var){}\mRightarrow{} Var[var];
rtermAdd(left,right){}\mRightarrow{} rec1,rec2.Add[left;right;rec1;rec2];
rtermSubtract(left,right){}\mRightarrow{} rec3,rec4.Subtract[left;right;rec3;rec4];
rtermMultiply(left,right){}\mRightarrow{} rec5,rec6.Multiply[left;right;rec5;rec6];
rtermDivide(num,denom){}\mRightarrow{} rec7,rec8.Divide[num;denom;rec7;rec8];
rtermMinus(num){}\mRightarrow{} rec9.Minus[num;rec9]) \mmember{} \{x:A| R[x;v]\} )
Date html generated:
2019_10_29-AM-09_31_06
Last ObjectModification:
2019_03_31-PM-05_26_29
Theory : reals
Home
Index