{ 
[Info:Type]. [P:es:EO+(Info) 
E 
].
p:es:EO+(Info). e:E. Dec(P[es;e])
[A,B:Type].
Ia:EClass(A). Ib:EClass(B).
((Singlevalued(Ia) 
Singlevalued(Ib))
(g1:es:EO+(Info) E(Ib) E. q:es:EO+(Info). e:E.
Dec((
e 
Ib)
c P[es;g1 es e]).
es:EO+(Info).
[Q,R:E E ].
((x,y:E. ((Q x y) (P[es;x] 
P[es;y])))
(f:E(Ia) B. g2:E(Ib) E.
(g1 es glues (Ia|p):Q f (Ib|q):R
g2 glues (Ia|
p):Q f (Ib|q):R
[
e.P[es;g1 es e]? g1 es : g2] glues Ia:Q f
Ib:R))))) }
{ Proof }
Definitions occuring in Statement :
Q-R-glues: g glues Ia:Qa f Ib:Rb,
es-interface-co-restrict: (I|p),
es-interface-restrict: (I|p),
es-E-interface: E(X),
sv-class: Singlevalued(X),
in-eclass: e X,
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
conditional: [P? f : g],
es-E: E,
compose: f o g,
assert: b,
decidable: Dec(P),
uall: [x:A]. B[x],
cand: A c B,
prop: ,
so_apply: x[s1;s2],
all: x:A. B[x],
iff: P Q,
implies: P Q,
and: P Q,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
universe: Type
Definitions :
compose: f o g,
conditional: [P? f : g],
Knd: Knd,
es-prior-interface: prior(X),
exists: 
x:A. B[x],
is_list_splitting: is_list_splitting(T;L;LL;L2;f),
is_accum_splitting: is_accum_splitting(T;A;L;LL;L2;f;g;x),
req: x = y,
rnonneg: rnonneg(r),
rleq: x 
y,
i-member: r I,
partitions: partitions(I;p),
modulus-of-ccontinuity: modulus-of-ccontinuity(omega;I;f),
sq_stable: SqStable(P),
so_apply: x[s],
eq_knd: a = b,
l_member: (x l),
tag-by: z
T,
record: record(x.T[x]),
fset: FSet{T},
dataflow: dataflow(A;B),
isect2: T1 
T2,
b-union: A 
B,
fpf-sub: f 
g,
map-class: (f[v] where v from X),
deq: EqDecider(T),
es-filter-image: f[X],
es-tagged-true-class: Tagged_tt(X),
ma-state: State(ds),
fpf-dom: x dom(f),
pair: <a, b>,
squash: 
T,
es-interface-at: X@i,
class-program: ClassProgram(T),
es-empty-interface: Empty,
cond-class: [X?Y],
list: type List,
fpf-cap: f(x)?z,
intensional-universe: IType,
guard: {T},
btrue: tt,
sq_type: SQType(T),
bool: 
,
true: True,
eclass-val: X(e),
inject: Inj(A;B;f),
Q-R-pre-preserving: f is Q-R-pre-preserving on P,
interface_predicate_set: interface_predicate_set{interface_predicate_set_compseq_tag_def:o}(X; es),
es-interface-predicate: {I},
fpf: a:A fp-> B[a],
strong-subtype: strong-subtype(A;B),
ge: i 
j ,
less_than: a < b,
uiff: uiff(P;Q),
uimplies: b supposing a,
suptype: suptype(S; T),
rev_implies: P Q,
set: {x:A| B[x]} ,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
in-eclass: e X,
void: Void,
false: False,
le: A B,
bag: bag(T),
lambda: x.A[x],
not: A,
subtype: S T,
eq_atom: eq_atom$n(x;y),
atom: Atom,
es-base-E: es-base-E(es),
token: "$token",
eq_atom: x =a y,
ifthenelse: if b then t else f fi ,
record-select: r.x,
dep-isect: Error :dep-isect,
record+: record+,
equal: s = t,
member: t T,
union: left + right,
or: P 
Q,
es-causle: e c e',
weak-antecedent-function: Q 
==f== P,
weak-antecedent-surjection: Q = f== P,
eclass: EClass(A[eo; e]),
sv-class: Singlevalued(X),
assert: b,
product: x:A B[x],
cand: A c B,
decidable: Dec(P),
universe: Type,
prop: ,
apply: f a,
so_apply: x[s1;s2],
iff: P Q,
top: Top,
event-ordering+: EO+(Info),
event_ordering: EO,
isect: x:A. B[x],
uall: [x:A]. B[x],
so_lambda: 
x.t[x],
all: x:A. B[x],
implies: P Q,
Q-R-glues: g glues Ia:Qa f Ib:Rb,
so_lambda: x y.t[x; y],
function: x:A B[x],
MaAuto: Error :MaAuto,
RepeatFor: Error :RepeatFor,
CollapseTHEN: Error :CollapseTHEN,
Try: Error :Try,
Auto: Error :Auto,
es-E-interface: E(X),
es-interface-co-restrict: (I|p),
subtype_rel: A r B,
and: P Q,
AssertBY: Error :AssertBY,
es-interface-restrict: (I|p),
es-E: E,
Complete: Error :Complete,
D: Error :D,
CollapseTHENA: Error :CollapseTHENA,
Repeat: Error :Repeat,
tactic: Error :tactic,
es-interface-disjoint: X Y = 0,
eclass-compose2: eclass-compose2(f;X;Y),
rel-restriction: R|P,
rel_or: R1 R2,
rel_equivalent: R1 R2,
rev_uimplies: rev_uimplies(P;Q),
infix_ap: x f y,
it: 
,
bool-decider: bool-decider(b),
inr: inr x ,
inl: inl x ,
branch: if p:P then A[p] else B fi ,
limited-type: LimitedType,
base: Base,
label: ...$L... t
Lemmas :
es-E-interface-subtype,
rel-restriction_wf,
rel_equivalent_wf,
rel_or_wf,
Q-R-glues_functionality,
es-interface-restrict-conditional,
rev_implies_wf,
bool-decider_wf,
assert_witness,
es-is-interface-restrict,
es-is-interface-co-restrict,
es-interface-restrict-disjoint,
es-E-interface-conditional-subtype,
cond-class_wf,
Q-R-glues-conditional2,
ext-eq_inversion,
is-interface-conditional-implies,
es-interface-disjoint_wf,
not_wf,
decidable_wf,
assert_wf,
event-ordering+_wf,
uall_wf,
es-E_wf,
iff_wf,
es-E-interface_wf,
Q-R-glues_wf,
es-interface-restrict_wf,
es-interface-co-restrict_wf,
eclass_wf,
sv-class_wf,
es-base-E_wf,
subtype_rel_self,
event-ordering+_inc,
member_wf,
es-interface-top,
in-eclass_wf,
top_wf,
subtype_rel_wf,
es-interface-predicate_wf,
weak-antecedent-surjection_wf,
Q-R-pre-preserving_wf,
inject_wf,
eclass-val_wf,
false_wf,
ifthenelse_wf,
true_wf,
bool_wf,
subtype_base_sq,
bool_subtype_base,
assert_elim,
intensional-universe_wf,
subtype_rel_function,
squash_wf,
subtype_rel_set,
subtype_rel_sets,
sq_stable__assert,
bag_wf,
es-E-interface-restrict,
es-E-interface-co-restrict
\mforall{}[Info:Type]. \mforall{}[P:es:EO+(Info) {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}].
\mforall{}p:\mforall{}es:EO+(Info). \mforall{}e:E. Dec(P[es;e])
\mforall{}[A,B:Type].
\mforall{}Ia:EClass(A). \mforall{}Ib:EClass(B).
((Singlevalued(Ia) \mwedge{} Singlevalued(Ib))
{}\mRightarrow{} (\mforall{}g1:es:EO+(Info) {}\mrightarrow{} E(Ib) {}\mrightarrow{} E. \mforall{}q:\mforall{}es:EO+(Info). \mforall{}e:E.
Dec((\muparrow{}e \mmember{}\msubb{} Ib) c\mwedge{} P[es;g1 es e]). \mforall{}es:EO+(Info).
\mforall{}[Q,R:E {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}].
((\mforall{}x,y:E. ((Q x y) {}\mRightarrow{} (P[es;x] \mLeftarrow{}{}\mRightarrow{} P[es;y])))
{}\mRightarrow{} (\mforall{}f:E(Ia) {}\mrightarrow{} B. \mforall{}g2:E(Ib) {}\mrightarrow{} E.
(g1 es glues (Ia|p):Q {}{}f{}\mrightarrow{} (Ib|q):R
{}\mRightarrow{} g2 glues (Ia|\mneg{}p):Q {}{}f{}\mrightarrow{} (Ib|\mneg{}q):R
{}\mRightarrow{} [\mlambda{}e.P[es;g1 es e]? g1 es : g2] glues Ia:Q {}{}f{}\mrightarrow{} Ib:R)))))
Date html generated:
2011_08_16-PM-05_58_51
Last ObjectModification:
2011_06_20-AM-01_41_18
Home
Index