{ TrivialCompResult 
CompilationResult }
{ Proof }
Definitions occuring in Statement :
trivial-comp-result: TrivialCompResult,
compilation-result: CompilationResult,
member: t T
Definitions :
compilation-result: CompilationResult,
true: True,
lambda: 
x.A[x],
eclass: EClass(A[eo; e]),
equal: s = t,
function: x:A 
B[x],
all: 
x:A. B[x],
subtype_rel: A 
r B,
fpf: a:A fp-> B[a],
strong-subtype: strong-subtype(A;B),
l_member: (x l),
implies: P 
Q,
product: x:A 
B[x],
trivial-comp-result: TrivialCompResult,
lg-nil: lg-nil(),
nil: [],
pair: <a, b>,
InitSys: InitSys,
member: t T,
Unfold: Error :Unfold,
CollapseTHEN: Error :CollapseTHEN,
tactic: Error :tactic,
RepUR: Error :RepUR,
Sys: Sys,
std-initial: std-initial(S),
universe: Type,
set: {x:A| B[x]} ,
System: System(P.M[P]),
Auto: Error :Auto,
so_lambda: 
x.t[x],
name: Name,
mData: mData,
pInTransit: pInTransit(P.M[P]),
lg-all: xG.P[x],
pi1: fst(t),
lg-label: lg-label(g;x),
real: 
,
subtype: S T,
rationals: 
,
nat: 
,
lg-size: lg-size(g),
prop: 
,
list: type List,
not: 
A,
false: False,
ldag: LabeledDAG(T),
top: Top,
lelt: i 
j < k,
and: P 
Q,
less_than: a < b,
le: A B,
int: 
,
minus: -n,
int_seg: {i..j
},
natural_number: $n,
AssertBY: Error :AssertBY,
RepeatFor: Error :RepeatFor,
D: Error :D,
labeled-graph: LabeledGraph(T),
is-dag: is-dag(g),
atom: Atom$n,
apply: f a,
pCom: pCom(P.M[P]),
Id: Id,
isect: 
x:A. B[x],
void: Void,
EnvType: EnvType,
RunType: RunType,
reliable-env: reliable-env(env; r),
pRunType: pRunType(T.M[T]),
pEnvType: pEnvType(T.M[T]),
std-l2m: std-l2m(),
std-n2m: std-n2m(),
Message: Message,
event-ordering+: EO+(Info),
strong-realizes: strong-realizes,
so_lambda: x y.t[x; y],
Complete: Error :Complete,
Try: Error :Try,
InitialSystem: InitialSystem(P.M[P]),
system-strongly-realizes: system-strongly-realizes,
CollapseTHENA: Error :CollapseTHENA,
guard: {T},
sub-system: sub-system(P.M[P];S1;S2),
let: let,
system-realizes: system-realizes,
THENM: Error :THENM,
pMsg: pMsg(P.M[P]),
spread: spread def,
strong-type-continuous: Continuous+(T.F[T]),
suptype: suptype(S; T),
pRun: pRun(S0;env;nat2msg;loc2msg),
fulpRunType: fulpRunType(T.M[T]),
so_apply: x[s],
bool: 
,
es-E-interface: E(X),
tag-case: z:T,
isect2: T1 T2,
union: left + right,
type-continuous: Continuous(T.F[T]),
intensional-universe: IType,
limited-type: LimitedType,
exists: 
x:A. B[x],
assert: 
b,
or: P 
Q,
unit: Unit,
MaAuto: Error :MaAuto,
parameter: parm{i},
component: component(P.M[P]),
fpf-sub: f g,
fpf-cap: f(x)?z,
deq: EqDecider(T),
ma-state: State(ds),
class-program: ClassProgram(T),
tag-by: zT,
rev_implies: P 
Q,
iff: P Q,
record: record(x.T[x]),
record+: record+,
fset: FSet{T},
b-union: A 
B
Lemmas :
fulpRunType-subtype,
subtype_rel_function,
pRunType_wf,
unit_wf,
fulpRunType_wf,
strong-continuous-product,
continuous-constant,
limited-type_wf,
intensional-universe_wf,
pRun_wf,
reliable-env_wf,
pRun_wf2,
nat_wf,
strong-type-continuous_wf,
pMsg_wf,
pEnvType_wf,
sub-system_wf,
System_wf,
InitSys_wf,
strong-realizes_wf,
Message_wf,
event-ordering+_wf,
std-n2m_wf,
std-l2m_wf,
reliable-env_wf2,
RunType_wf,
EnvType_wf,
Id_wf,
pCom_wf,
subtype_rel_wf,
lg-all_wf_dag,
int_seg_wf,
ldag_wf,
top_wf,
le_wf,
lg-label_wf_dag,
pi1_wf_top,
pInTransit_wf,
lg-nil_wf_dag,
mData_wf,
name_wf,
component_wf,
compilation-result_wf,
member_wf,
true_wf
TrivialCompResult \mmember{} CompilationResult
Date html generated:
2011_08_17-PM-04_39_01
Last ObjectModification:
2010_09_24-PM-03_26_39
Home
Index