Nuprl Lemma : int_term_ind_wf_simple

∀[A:Type]. ∀[v:int_term()]. ∀[Constant,Var:var:ℤ ⟶ A]. ∀[Add,Subtract,Multiply:left:int_term()
                                                                                ⟶ right:int_term()
                                                                                ⟶ A
                                                                                ⟶ A
                                                                                ⟶ A].
∀[Minus:num:int_term() ⟶ A ⟶ A].
  (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])  ∈ A)


Proof



Definitions occuring in Statement :  int_term_ind: int_term_ind,  int_term: int_term(),  uall: ∀[x:A]. B[x],  so_apply: x[s1;s2;s3;s4],  so_apply: x[s1;s2],  so_apply: x[s],  member: t ∈ T,  function: x:A ⟶ B[x],  int: ℤ,  universe: Type
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  so_lambda: λ2x y.t[x; y],  so_apply: x[s1;s2],  subtype_rel: A ⊆r B,  true: True,  prop: ℙ,  so_lambda: λ2x.t[x],  so_apply: x[s],  uimplies: b supposing a,  all: ∀x:A. B[x]
Lemmas referenced :  int_term_ind_wf,  true_wf,  int_term_wf,  subtype_rel_dep_function,  istype-int,  istype-universe
Rules used in proof :  cut,  introduction,  extract_by_obid,  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  Error :isect_memberFormation_alt,  hypothesis,  sqequalHypSubstitution,  isectElimination,  thin,  hypothesisEquality,  sqequalRule,  Error :lambdaEquality_alt,  Error :universeIsType,  functionExtensionality,  applyEquality,  Error :dependent_set_memberEquality_alt,  natural_numberEquality,  Error :inhabitedIsType,  equalityTransitivity,  equalitySymmetry,  closedConclusion,  intEquality,  functionEquality,  because_Cache,  setEquality,  independent_isectElimination,  Error :lambdaFormation_alt,  Error :setIsType,  setElimination,  rename,  applyLambdaEquality,  Error :functionIsType,  instantiate,  universeEquality
Latex:
\mforall{}[A:Type].  \mforall{}[v:int\_term()].  \mforall{}[Constant,Var:var:\mBbbZ{}  {}\mrightarrow{}  A].  \mforall{}[Add,Subtract,Multiply:left:int\_term()
                                                                                                                                                                {}\mrightarrow{}  right:int\_term()
                                                                                                                                                                {}\mrightarrow{}  A
                                                                                                                                                                {}\mrightarrow{}  A
                                                                                                                                                                {}\mrightarrow{}  A].
\mforall{}[Minus:num:int\_term()  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    (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{}  A)


Date html generated: 2019_06_20-PM-00_45_05
Last ObjectModification: 2019_01_22-AM-08_39_20

Theory : omega


Home Index