{ 
[Info,A,B,C,D,E:Type]. 
[F:Id
                              
 bag(A)
                              
 bag(B)
                              
 bag(C)
                              
 bag(D)
                              
 bag(E)]. 
[W:EClass(A)]. 
[X:EClass(B)].
  
[Y:EClass(C)]. 
[Z:EClass(D)].
    (simple-loc-comb-4(F;W;X;Y;Z) 
 EClass(E)) }
{ Proof }
Definitions occuring in Statement : 
simple-loc-comb-4: simple-loc-comb-4(F;W;X;Y;Z), 
eclass: EClass(A[eo; e]), 
Id: Id, 
uall:
[x:A]. B[x], 
member: t 
 T, 
function: x:A 
 B[x], 
universe: Type, 
bag: bag(T)
Lemmas : 
int_seg_properties, 
decidable__equal_int, 
int_subtype_base, 
es-E_wf, 
event-ordering+_wf, 
eclass_wf, 
event-ordering+_inc, 
Id_wf, 
bag_wf, 
member_wf, 
simple-loc-comb_wf, 
le_wf, 
not_wf, 
false_wf, 
nat_wf, 
int_seg_wf, 
select_wf, 
length_wf_nat, 
length_nil, 
length_cons, 
non_neg_length, 
length_wf1, 
top_wf, 
subtype_rel_wf, 
es-interface-top, 
subtype_base_sq
\mforall{}[Info,A,B,C,D,E:Type].  \mforall{}[F:Id  {}\mrightarrow{}  bag(A)  {}\mrightarrow{}  bag(B)  {}\mrightarrow{}  bag(C)  {}\mrightarrow{}  bag(D)  {}\mrightarrow{}  bag(E)].  \mforall{}[W:EClass(A)].
\mforall{}[X:EClass(B)].  \mforall{}[Y:EClass(C)].  \mforall{}[Z:EClass(D)].
    (simple-loc-comb-4(F;W;X;Y;Z)  \mmember{}  EClass(E))
Date html generated:
2011_08_16-PM-05_00_57
Last ObjectModification:
2011_07_24-PM-11_46_17
Home
Index