{ 
[P:Pi_term 
]
(P[0]
(pre:pi_prefix(). body:Pi_term. (P[body] P[pre.body]))
(left,right:Pi_term. (P[left] P[right] P[(left + right)]))
(left,right:Pi_term. (P[left] P[right] P[(left | right)]))
(body:Pi_term. (P[body] P[!body]))
(name:Name. body:Pi_term. (P[body] P[(new name. body)]))
{x:Pi_term. P[x]}) }
{ Proof }
Definitions occuring in Statement :
pinew: (new name. body),
pirep: !body,
pipar: (left | right),
pioption: (left + right),
picomm: pre.body,
pizero: 0,
pi_term: Pi_term,
pi_prefix: pi_prefix(),
name: Name,
uall: [x:A]. B[x],
prop: ,
guard: {T},
so_apply: x[s],
all: x:A. B[x],
implies: P Q,
function: x:A B[x]
Definitions :
uall: [x:A]. B[x],
prop: ,
implies: P Q,
so_apply: x[s],
all: x:A. B[x],
guard: {T},
member: t 
T,
type-monotone: Monotone(T.F[T]),
uimplies: b supposing a,
pi_term: Pi_term,
pizero: 0,
picomm: pre.body,
pioption: (left + right),
pipar: (left | right),
pirep: !body,
pinew: (new name. body),
unit: Unit,
it: 
Lemmas :
unit_wf,
pi_prefix_wf,
name_wf,
subtype_rel_sum,
subtype_rel_simple_product,
pi_term_wf,
pinew_wf,
pirep_wf,
pipar_wf,
pioption_wf,
picomm_wf,
pizero_wf
\mforall{}[P:Pi\_term {}\mrightarrow{} \mBbbP{}]
(P[0]
{}\mRightarrow{} (\mforall{}pre:pi\_prefix(). \mforall{}body:Pi\_term. (P[body] {}\mRightarrow{} P[pre.body]))
{}\mRightarrow{} (\mforall{}left,right:Pi\_term. (P[left] {}\mRightarrow{} P[right] {}\mRightarrow{} P[(left + right)]))
{}\mRightarrow{} (\mforall{}left,right:Pi\_term. (P[left] {}\mRightarrow{} P[right] {}\mRightarrow{} P[(left | right)]))
{}\mRightarrow{} (\mforall{}body:Pi\_term. (P[body] {}\mRightarrow{} P[!body]))
{}\mRightarrow{} (\mforall{}name:Name. \mforall{}body:Pi\_term. (P[body] {}\mRightarrow{} P[(new name. body)]))
{}\mRightarrow{} \{\mforall{}x:Pi\_term. P[x]\})
Date html generated:
2011_08_17-PM-06_42_41
Last ObjectModification:
2011_06_18-PM-12_10_22
Home
Index