Nuprl Lemma : pi_term-definition
∀[A:Type]. ∀[R:A ─→ pi_term() ─→ ℙ].
({x:A| R[x;pizero()]}
⇒ (∀pre:pi_prefix(). ∀body:pi_term(). ({x:A| R[x;body]} ⇒ {x:A| R[x;picomm(pre;body)]} ))
⇒ (∀left,right:pi_term(). ({x:A| R[x;left]} ⇒ {x:A| R[x;right]} ⇒ {x:A| R[x;pioption(left;right)]} ))
⇒ (∀left,right:pi_term(). ({x:A| R[x;left]} ⇒ {x:A| R[x;right]} ⇒ {x:A| R[x;pipar(left;right)]} ))
⇒ (∀body:pi_term(). ({x:A| R[x;body]} ⇒ {x:A| R[x;pirep(body)]} ))
⇒ (∀name:Name. ∀body:pi_term(). ({x:A| R[x;body]} ⇒ {x:A| R[x;pinew(name;body)]} ))
⇒ {∀v:pi_term(). {x:A| R[x;v]} })
Proof
Definitions occuring in Statement :
pinew: pinew(name;body),
pirep: pirep(body),
pipar: pipar(left;right),
pioption: pioption(left;right),
picomm: picomm(pre;body),
pizero: pizero(),
pi_term: pi_term(),
pi_prefix: pi_prefix(),
name: Name,
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],
universe: Type
Lemmas :
pi_term-induction,
set_wf,
all_wf,
name_wf,
pi_term_wf,
pinew_wf,
pirep_wf,
pipar_wf,
pioption_wf,
pi_prefix_wf,
picomm_wf,
pizero_wf
Latex:
\mforall{}[A:Type]. \mforall{}[R:A {}\mrightarrow{} pi\_term() {}\mrightarrow{} \mBbbP{}].
(\{x:A| R[x;pizero()]\}
{}\mRightarrow{} (\mforall{}pre:pi\_prefix(). \mforall{}body:pi\_term(). (\{x:A| R[x;body]\} {}\mRightarrow{} \{x:A| R[x;picomm(pre;body)]\} ))
{}\mRightarrow{} (\mforall{}left,right:pi\_term().
(\{x:A| R[x;left]\} {}\mRightarrow{} \{x:A| R[x;right]\} {}\mRightarrow{} \{x:A| R[x;pioption(left;right)]\} ))
{}\mRightarrow{} (\mforall{}left,right:pi\_term().
(\{x:A| R[x;left]\} {}\mRightarrow{} \{x:A| R[x;right]\} {}\mRightarrow{} \{x:A| R[x;pipar(left;right)]\} ))
{}\mRightarrow{} (\mforall{}body:pi\_term(). (\{x:A| R[x;body]\} {}\mRightarrow{} \{x:A| R[x;pirep(body)]\} ))
{}\mRightarrow{} (\mforall{}name:Name. \mforall{}body:pi\_term(). (\{x:A| R[x;body]\} {}\mRightarrow{} \{x:A| R[x;pinew(name;body)]\} ))
{}\mRightarrow{} \{\mforall{}v:pi\_term(). \{x:A| R[x;v]\} \})
Date html generated:
2015_07_23-AM-11_32_44
Last ObjectModification:
2015_01_29-AM-00_53_58
Home
Index