{ 
[P:Expression 
]
((val:Atom. P[val])
(fst,snd:Expression. (P[fst] P[snd] P[fst,snd]))
(fun:Atom. arg:Expression. (P[arg] P[fun(arg)]))
{x:Expression. P[x]}) }
{ Proof }
Definitions occuring in Statement :
expapply: fun(arg),
exppair: fst,snd,
expbase: val,
expression: Expression,
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],
atom: Atom
Definitions :
uall: [x:A]. B[x],
prop: ,
implies: P Q,
all: x:A. B[x],
so_apply: x[s],
guard: {T},
type-monotone: Monotone(T.F[T]),
uimplies: b supposing a,
member: t 
T,
expression: Expression,
expbase: val,
exppair: fst,snd,
expapply: fun(arg)
Lemmas :
subtype_rel_sum,
subtype_rel_simple_product,
expression_wf,
expapply_wf,
exppair_wf,
expbase_wf
\mforall{}[P:Expression {}\mrightarrow{} \mBbbP{}]
((\mforall{}val:Atom. P[val])
{}\mRightarrow{} (\mforall{}fst,snd:Expression. (P[fst] {}\mRightarrow{} P[snd] {}\mRightarrow{} P[fst,snd]))
{}\mRightarrow{} (\mforall{}fun:Atom. \mforall{}arg:Expression. (P[arg] {}\mRightarrow{} P[fun(arg)]))
{}\mRightarrow{} \{\mforall{}x:Expression. P[x]\})
Date html generated:
2011_08_17-PM-04_33_54
Last ObjectModification:
2011_06_18-AM-11_44_56
Home
Index