Nuprl Lemma : language1_wf
∀[fml:D:Type ─→ ℙ ─→ (D ─→ ℙ) ─→ (D ─→ ℙ) ─→ (D ─→ D ─→ ℙ) ─→ (D ─→ D ─→ ℙ) ─→ (D ─→ D ─→ ℙ) ─→ (D ─→ D ─→ D ─→ ℙ) ─→ ℙ]
(language1{i:l}(D,A,B,C,P,Q,R,H.fml[D;A;B;C;P;Q;R;H]) ∈ ℙ')
Proof
Definitions occuring in Statement :
language1: language1{i:l}(D,A,B,C,P,Q,R,H.fml[D;A;B;C;P;Q;R;H]),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[a;b;c;d;e;f;g;h],
member: t ∈ T,
function: x:A ─→ B[x],
universe: Type
Lemmas :
uall_wf
\mforall{}[fml:D:Type
{}\mrightarrow{} \mBbbP{}
{}\mrightarrow{} (D {}\mrightarrow{} \mBbbP{})
{}\mrightarrow{} (D {}\mrightarrow{} \mBbbP{})
{}\mrightarrow{} (D {}\mrightarrow{} D {}\mrightarrow{} \mBbbP{})
{}\mrightarrow{} (D {}\mrightarrow{} D {}\mrightarrow{} \mBbbP{})
{}\mrightarrow{} (D {}\mrightarrow{} D {}\mrightarrow{} \mBbbP{})
{}\mrightarrow{} (D {}\mrightarrow{} D {}\mrightarrow{} D {}\mrightarrow{} \mBbbP{})
{}\mrightarrow{} \mBbbP{}]
(language1\{i:l\}(D,A,B,C,P,Q,R,H.fml[D;A;B;C;P;Q;R;H]) \mmember{} \mBbbP{}')
Date html generated:
2015_07_17-AM-07_52_31
Last ObjectModification:
2015_01_30-AM-01_13_26
Home
Index