{ 
[cp:ClassProgram(Top)]. [i:{i:Id| (i 
cp-domain(cp))} ].
[k:{k:Knd| (k cp-kinds(cp) i)} ].
(cp-ktype(cp;i;k) Type) }
{ Proof }
Definitions occuring in Statement :
cp-ktype: cp-ktype(cp;i;k),
cp-kinds: cp-kinds(cp),
cp-domain: cp-domain(cp),
class-program: ClassProgram(T),
Knd: Knd,
Id: Id,
uall: [x:A]. B[x],
top: Top,
member: t T,
set: {x:A| B[x]} ,
apply: f a,
universe: Type,
l_member: (x l)
Definitions :
intensional-universe: IType,
pi1: fst(t),
fpf-domain: fpf-domain(f),
strong-subtype: strong-subtype(A;B),
le: A 
B,
ge: i 
j ,
not: 
A,
uimplies: b supposing a,
and: P 
Q,
uiff: uiff(P;Q),
atom: Atom$n,
subtype_rel: A 
r B,
nat: 
,
less_than: a < b,
cand: A c B,
pair: <a, b>,
union: left + right,
spread: spread def,
exists: 
x:A. B[x],
axiom: Ax,
cp-ktype: cp-ktype(cp;i;k),
bool: 
,
subtype: S T,
hasloc: hasloc(k;i),
list: type List,
cp-kinds: cp-kinds(cp),
apply: f a,
Knd: Knd,
cp-domain: cp-domain(cp),
universe: Type,
prop: 
,
product: x:A 
B[x],
isect: 
x:A. B[x],
all: x:A. B[x],
function: x:A 
B[x],
uall: [x:A]. B[x],
set: {x:A| B[x]} ,
l_member: (x l),
Id: Id,
top: Top,
equal: s = t,
class-program: ClassProgram(T),
assert: 
b,
member: t T,
fpf: a:A fp-> B[a],
tactic: Error :tactic,
filter: filter(P;l),
natural_number: $n,
void: Void,
select: l[i],
length: ||as||,
real: 
,
grp_car: |g|,
int: 
,
or: P 
Q,
guard: {T},
so_apply: x[s],
rev_implies: P 
Q,
fpf-join: f 
g,
fpf-single: x : v,
eqof: eqof(d),
fpf-cap: f(x)?z,
iff: P 
Q,
true: True,
fpf-dom: x dom(f),
false: False,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
ifthenelse: if b then t else f fi ,
deq: EqDecider(T),
nil: [],
implies: P Q,
id-deq: IdDeq,
fpf-ap: f(x),
lambda: 
x.A[x],
spreadn: spread6,
so_lambda: 
x.t[x]
Lemmas :
fpf_wf,
fpf-domain_wf,
fpf-trivial-subtype-top,
fpf-ap_wf,
id-deq_wf,
deq_wf,
false_wf,
ifthenelse_wf,
fpf-dom_wf,
true_wf,
fpf-type,
iff_wf,
bool_wf,
strong-subtype-deq-subtype,
strong-subtype_wf,
strong-subtype-set3,
strong-subtype-self,
member-fpf-dom,
uiff_inversion,
length_wf_nat,
select_wf,
top_wf,
Knd_wf,
l_member_wf,
member_wf,
Id_wf,
assert_wf,
nat_wf,
hasloc_wf,
cp-kinds_wf,
cp-domain_wf,
class-program_wf,
subtype_rel_wf,
intensional-universe_wf
\mforall{}[cp:ClassProgram(Top)]. \mforall{}[i:\{i:Id| (i \mmember{} cp-domain(cp))\} ]. \mforall{}[k:\{k:Knd| (k \mmember{} cp-kinds(cp) i)\} ].
(cp-ktype(cp;i;k) \mmember{} Type)
Date html generated:
2011_08_16-AM-11_01_40
Last ObjectModification:
2011_06_18-AM-09_35_07
Home
Index