Nuprl Lemma : int_term-definition
∀[A:Type]. ∀[R:A ⟶ int_term() ⟶ ℙ].
((∀const:ℤ. {x:A| R[x;"const"]} )
⇒ (∀var:ℤ. {x:A| R[x;vvar]} )
⇒ (∀left,right:int_term(). ({x:A| R[x;left]} ⇒ {x:A| R[x;right]} ⇒ {x:A| R[x;left "+" right]} ))
⇒ (∀left,right:int_term(). ({x:A| R[x;left]} ⇒ {x:A| R[x;right]} ⇒ {x:A| R[x;left "-" right]} ))
⇒ (∀left,right:int_term(). ({x:A| R[x;left]} ⇒ {x:A| R[x;right]} ⇒ {x:A| R[x;left "*" right]} ))
⇒ (∀num:int_term(). ({x:A| R[x;num]} ⇒ {x:A| R[x;"-"num]} ))
⇒ {∀v:int_term(). {x:A| R[x;v]} })
Proof
Definitions occuring in Statement :
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: ℙ,
guard: {T},
so_apply: x[s1;s2],
all: ∀x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
int: ℤ,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
guard: {T},
so_lambda: λ2x.t[x],
member: t ∈ T,
so_apply: x[s1;s2],
subtype_rel: A ⊆r B,
so_apply: x[s],
prop: ℙ
Lemmas referenced :
int_term-induction,
set_wf,
int_term_wf,
all_wf,
itermMinus_wf,
itermMultiply_wf,
itermSubtract_wf,
itermAdd_wf,
itermVar_wf,
itermConstant_wf
Rules used in proof :
cut,
lemma_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
sqequalRule,
lambdaEquality,
hypothesisEquality,
applyEquality,
because_Cache,
independent_functionElimination,
functionEquality,
universeEquality,
intEquality,
cumulativity
Latex:
\mforall{}[A:Type]. \mforall{}[R:A {}\mrightarrow{} int\_term() {}\mrightarrow{} \mBbbP{}].
((\mforall{}const:\mBbbZ{}. \{x:A| R[x;"const"]\} )
{}\mRightarrow{} (\mforall{}var:\mBbbZ{}. \{x:A| R[x;vvar]\} )
{}\mRightarrow{} (\mforall{}left,right:int\_term().
(\{x:A| R[x;left]\} {}\mRightarrow{} \{x:A| R[x;right]\} {}\mRightarrow{} \{x:A| R[x;left "+" right]\} ))
{}\mRightarrow{} (\mforall{}left,right:int\_term().
(\{x:A| R[x;left]\} {}\mRightarrow{} \{x:A| R[x;right]\} {}\mRightarrow{} \{x:A| R[x;left "-" right]\} ))
{}\mRightarrow{} (\mforall{}left,right:int\_term().
(\{x:A| R[x;left]\} {}\mRightarrow{} \{x:A| R[x;right]\} {}\mRightarrow{} \{x:A| R[x;left "*" right]\} ))
{}\mRightarrow{} (\mforall{}num:int\_term(). (\{x:A| R[x;num]\} {}\mRightarrow{} \{x:A| R[x;"-"num]\} ))
{}\mRightarrow{} \{\mforall{}v:int\_term(). \{x:A| R[x;v]\} \})
Date html generated:
2016_05_14-AM-06_59_11
Last ObjectModification:
2015_12_26-PM-01_13_05
Theory : omega
Home
Index