Nuprl Lemma : int_term_ind_wf
∀[A:Type]. ∀[R:A ⟶ int_term() ⟶ ℙ]. ∀[v:int_term()]. ∀[Constant:const:ℤ ⟶ {x:A| R[x;"const"]} ].
∀[Var:var:ℤ ⟶ {x:A| R[x;vvar]} ]. ∀[Add:left:int_term()
⟶ right:int_term()
⟶ {x:A| R[x;left]}
⟶ {x:A| R[x;right]}
⟶ {x:A| R[x;left (+) right]} ]. ∀[Subtract:left:int_term()
⟶ right:int_term()
⟶ {x:A| R[x;left]}
⟶ {x:A| R[x;right]}
⟶ {x:A| R[x;left (-) right]} ].
∀[Multiply:left:int_term() ⟶ right:int_term() ⟶ {x:A| R[x;left]} ⟶ {x:A| R[x;right]} ⟶ {x:A| R[x;left (*) right]} \000C].
∀[Minus:num:int_term() ⟶ {x:A| R[x;num]} ⟶ {x:A| R[x;"-"num]} ].
(int_term_ind(v;
itermConstant(const)⇒ Constant[const];
itermVar(var)⇒ Var[var];
itermAdd(left,right)⇒ rec1,rec2.Add[left;right;rec1;rec2];
itermSubtract(left,right)⇒ rec3,rec4.Subtract[left;right;rec3;rec4];
itermMultiply(left,right)⇒ rec5,rec6.Multiply[left;right;rec5;rec6];
itermMinus(num)⇒ rec7.Minus[num;rec7]) ∈ {x:A| R[x;v]} )
Proof
Definitions occuring in Statement :
int_term_ind: int_term_ind,
itermMinus: "-"num,
itermMultiply: left (*) right,
itermSubtract: left (-) right,
itermAdd: left (+) right,
itermVar: vvar,
itermConstant: "const",
int_term: int_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,
int_term_ind: int_term_ind,
so_apply: x[s1;s2],
so_apply: x[s1;s2;s3;s4],
so_apply: x[s],
int_term-definition,
int_term-induction,
uniform-comp-nat-induction,
int_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 :
int_term-definition,
istype-void,
has-value_wf_base,
is-exception_wf,
lifting-strict-atom_eq,
strict4-decide,
istype-int,
itermConstant_wf,
itermVar_wf,
itermAdd_wf,
itermSubtract_wf,
itermMultiply_wf,
itermMinus_wf,
int_term_wf,
all_wf,
set_wf,
subtype_rel_function,
subtype_rel_self,
istype-universe,
int_term-induction,
uniform-comp-nat-induction,
int_term-ext,
bool_cases_sqequal,
eqff_to_assert
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
cut,
sqequalRule,
Error :isect_memberEquality_alt,
voidElimination,
introduction,
extract_by_obid,
hypothesis,
Error :inhabitedIsType,
Error :lambdaFormation_alt,
thin,
sqequalSqle,
divergentSqle,
callbyvalueDecide,
sqequalHypSubstitution,
hypothesisEquality,
unionElimination,
sqleReflexivity,
Error :equalityIstype,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
independent_functionElimination,
decideExceptionCases,
axiomSqleEquality,
exceptionSqequal,
baseApply,
closedConclusion,
baseClosed,
isectElimination,
independent_isectElimination,
instantiate,
applyEquality,
Error :lambdaEquality_alt,
Error :isectIsType,
Error :functionIsType,
Error :universeIsType,
universeEquality,
Error :setIsType,
because_Cache,
functionEquality,
setEquality,
functionExtensionality,
intEquality,
setElimination,
rename,
Error :dependent_set_memberEquality_alt
Latex:
\mforall{}[A:Type]. \mforall{}[R:A {}\mrightarrow{} int\_term() {}\mrightarrow{} \mBbbP{}]. \mforall{}[v:int\_term()]. \mforall{}[Constant:const:\mBbbZ{} {}\mrightarrow{} \{x:A| R[x;"const"]\} ].
\mforall{}[Var:var:\mBbbZ{} {}\mrightarrow{} \{x:A| R[x;vvar]\} ]. \mforall{}[Add:left:int\_term()
{}\mrightarrow{} right:int\_term()
{}\mrightarrow{} \{x:A| R[x;left]\}
{}\mrightarrow{} \{x:A| R[x;right]\}
{}\mrightarrow{} \{x:A| R[x;left (+) right]\} ].
\mforall{}[Subtract:left:int\_term()
{}\mrightarrow{} right:int\_term()
{}\mrightarrow{} \{x:A| R[x;left]\}
{}\mrightarrow{} \{x:A| R[x;right]\}
{}\mrightarrow{} \{x:A| R[x;left (-) right]\} ]. \mforall{}[Multiply:left:int\_term()
{}\mrightarrow{} right:int\_term()
{}\mrightarrow{} \{x:A| R[x;left]\}
{}\mrightarrow{} \{x:A| R[x;right]\}
{}\mrightarrow{} \{x:A| R[x;left (*) right]\} ].
\mforall{}[Minus:num:int\_term() {}\mrightarrow{} \{x:A| R[x;num]\} {}\mrightarrow{} \{x:A| R[x;"-"num]\} ].
(int\_term\_ind(v;
itermConstant(const){}\mRightarrow{} Constant[const];
itermVar(var){}\mRightarrow{} Var[var];
itermAdd(left,right){}\mRightarrow{} rec1,rec2.Add[left;right;rec1;rec2];
itermSubtract(left,right){}\mRightarrow{} rec3,rec4.Subtract[left;right;rec3;rec4];
itermMultiply(left,right){}\mRightarrow{} rec5,rec6.Multiply[left;right;rec5;rec6];
itermMinus(num){}\mRightarrow{} rec7.Minus[num;rec7]) \mmember{} \{x:A| R[x;v]\} )
Date html generated:
2019_06_20-PM-00_45_02
Last ObjectModification:
2019_01_09-PM-01_10_29
Theory : omega
Home
Index