Nuprl Definition : language1
language1{i:l}(D,A,B,C,P,Q,R,H.fml[D;A;B;C;P;Q;R;H]) ==
∀[D:Type]. ∀[A:ℙ]. ∀[B,C:D ─→ ℙ]. ∀[P,Q,R:D ─→ D ─→ ℙ]. ∀[H:D ─→ D ─→ D ─→ ℙ]. fml[D;A;B;C;P;Q;R;H]
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
prop: ℙ,
function: x:A ─→ B[x],
universe: Type
FDL editor aliases :
language1
language1\{i:l\}(D,A,B,C,P,Q,R,H.fml[D;A;B;C;P;Q;R;H]) ==
\mforall{}[D:Type]. \mforall{}[A:\mBbbP{}]. \mforall{}[B,C:D {}\mrightarrow{} \mBbbP{}]. \mforall{}[P,Q,R:D {}\mrightarrow{} D {}\mrightarrow{} \mBbbP{}]. \mforall{}[H:D {}\mrightarrow{} D {}\mrightarrow{} D {}\mrightarrow{} \mBbbP{}].
fml[D;A;B;C;P;Q;R;H]
Date html generated:
2015_07_17-AM-07_52_31
Last ObjectModification:
2012_07_12-AM-10_34_31
Home
Index