{ 
[dv:ClassDerivation]
cdv-classes-and-programs(dv) 
ClassProgram List supposing WF(dv) }
{ Proof }
Definitions occuring in Statement :
cdv-classes-and-programs: cdv-classes-and-programs(dv),
cdv-class-program: ClassProgram,
cdv-wf: WF(dv),
classderiv: ClassDerivation,
uimplies: b supposing a,
uall: [x:A]. B[x],
member: t T,
list: type List
Definitions :
axiom: Ax,
prop: 
,
so_lambda: 
x.t[x],
fpf: a:A fp-> B[a],
strong-subtype: strong-subtype(A;B),
le: A 
B,
ge: i 
j ,
not: 
A,
less_than: a < b,
uimplies: b supposing a,
uiff: uiff(P;Q),
union: left + right,
rec: rec(x.A[x]),
subtype_rel: A 
r B,
product: x:A 
B[x],
subtype: S T,
event_ordering: EO,
es-E: E,
event-ordering+: EO+(Info),
so_lambda: x y.t[x; y],
function: x:A 
B[x],
isect: 
x:A. B[x],
uall: [x:A]. B[x],
cdv-classes-and-programs: cdv-classes-and-programs(dv),
cdv-class-program: ClassProgram,
list: type List,
member: t T,
cdv-types: cdv-types(dv),
pi1: fst(t),
lambda: x.A[x],
map: map(f;as),
universe: Type,
equal: s = t,
and: P 
Q,
cdv-wf: WF(dv),
implies: P 
Q,
classderiv: ClassDerivation,
all: x:A. B[x],
Message: Message,
eclass: EClass(A[eo; e]),
rec-comb-program: rec-comb-program(F;B;Ps),
rec-combined-class: f|X,(self)'|,
so_apply: x[s],
or: P 
Q,
locl: locl(a),
Knd: Knd,
assert: 
b,
classderiv_ind_cdvreccomb: classderiv_ind_cdvreccomb_compseq_tag_def,
simple-comb-program: simple-comb-program(F;B;Ps),
simple-comb: simple-comb(F;Xs),
ext-eq: A 
B,
class-program: ClassProgram(T),
fpf-sub: f g,
sq_stable: SqStable(P),
fpf-cap: f(x)?z,
lelt: i j < k,
false: False,
real: 
,
rationals: 
,
select: l[i],
int_seg: {i..j
},
length: ||as||,
let: let,
filter: filter(P;l),
permutation: permutation(T;L1;L2),
intensional-universe: IType,
es-E-interface: E(X),
guard: {T},
sq_type: SQType(T),
empty-bag: {},
limited-type: LimitedType,
classderiv_ind_cdvcomb: classderiv_ind_cdvcomb_compseq_tag_def,
listp: A List
,
combination: Combination(n;T),
delay-program: delay-program(P),
es-prior-val: (X)',
spreadn: spread3,
natural_number: $n,
classderiv_ind_cdvdelay: classderiv_ind_cdvdelay_compseq_tag_def,
bool: 
,
void: Void,
top: Top,
squash: 
T,
sqequal: s ~ t,
append: as @ bs,
pi2: snd(t),
ycomb: Y,
classderiv_ind: classderiv_ind,
apply: f a,
classderiv_ind_cdvpair: classderiv_ind_cdvpair_compseq_tag_def,
eclass-program: eclass-program{i:l}(Info),
tl: tl(l),
hd: hd(l),
name: Name,
quotient: x,y:A//B[x; y],
l_member: (x l),
base-deriv-program: base-deriv-program(bdv),
base-deriv-class: base-deriv-class(bdv),
pair: <a, b>,
nil: [],
base-deriv-type: base-deriv-type(bdv),
cons: [car / cdr],
cand: A c B,
true: True,
classderiv_ind_cdvbase: classderiv_ind_cdvbase_compseq_tag_def,
bag: bag(T),
int: 
,
unit: Unit,
set: {x:A| B[x]} ,
base-deriv: BaseDef,
cdv-argtype: cdv-argtype(dv),
label: ...$L... t,
defined-class: defined-class(prg),
eclass-program-type: eclass-program-type(prg),
base-program: base-program(locs;hdr;T),
Id: Id,
exists: 
x:A. B[x],
IdLnk: IdLnk,
fpf-dom: x dom(f),
atom: Atom$n,
deq: EqDecider(T),
ma-state: State(ds),
df-program-type: df-program-type(dfp),
tag-by: zT,
rev_implies: P 
Q,
iff: P Q,
ldag: LabeledDAG(T),
labeled-graph: LabeledGraph(T),
record+: record+,
record: record(x.T[x]),
fset: FSet{T},
dataflow: dataflow(A;B),
isect2: T1 T2,
b-union: A 
B,
dataflow-program: DataflowProgram(A),
parameter: parm{i},
spread: spread def,
suptype: suptype(S; T),
nat: 
,
null-df-program: null-df-program(B),
parallel-df-program: parallel-df-program(B;F;dfps),
fpf-domain: fpf-domain(f),
id-deq: IdDeq,
union-list2: union-list2(eq;ll),
mk_fpf: mk_fpf(L;f),
fpf-single: x : v,
eclass-program-flows: eclass-program-flows(p),
fpf-join: f 
g,
bag-size: bag-size(bs),
lt_int: i <z j,
feedback-df-program: Error :feedback-df-program
Lemmas :
es-interface-subtype_rel2,
defined-by-rec-comb-program,
rec-comb-program_wf,
rec-combined-class_wf,
union-list2_wf,
id-deq_wf,
defined-by-simple-comb-program,
simple-comb-program_wf,
int_seg_properties,
simple-comb_wf,
cdv-types-non-empty,
pos_length2,
ge_wf,
select-map,
not_wf,
false_wf,
le_wf,
length_wf_nat,
length-map,
map_wf,
pi1_wf_top,
defined-by-delay-program,
es-prior-val_wf,
delay-program_wf,
subtype_base_sq,
fpf_wf,
Id_wf,
dataflow-program_wf,
subtype_rel_product,
df-program-type_wf,
subtype-fpf2,
subtype_rel_set,
subtype_rel_sets,
subtype_rel_self,
es-interface-subtype_rel,
defined-by-base-program,
assert_wf,
limited-type_wf,
defined-class_wf,
eclass_wf2,
eclass-program-type_wf,
es-interface-top,
eclass-program_wf,
base-deriv-program_wf,
base-deriv-class_wf,
base-deriv-type_wf,
true_wf,
map_append_sq,
squash_wf,
append_wf,
top_wf,
bag_wf,
cdv-argtype_wf,
empty-bag_wf,
intensional-universe_wf,
permutation_wf,
cdv-types_wf,
int_seg_wf,
select_wf,
length_wf1,
sq_stable__subtype_rel,
subtype_rel_weakening,
ext-eq_weakening,
eclass_wf,
es-E_wf,
event-ordering+_inc,
Message_wf,
event-ordering+_wf,
subtype_rel_wf,
uall_wf,
classderiv_wf,
cdv-class-program_wf,
member_wf,
cdv-wf_wf
\mforall{}[dv:ClassDerivation]. cdv-classes-and-programs(dv) \mmember{} ClassProgram List supposing WF(dv)
Date html generated:
2011_08_17-PM-04_28_24
Last ObjectModification:
2011_01_19-PM-08_37_52
Home
Index