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