Nuprl Definition : compat-trip-lists

compat-trip-lists(x;y;R;S;T) ==  [r:R]. [s:S]. [t1,t2:T].  t1 = t2 supposing (<r, s, t1>  x)  (<r, s, t2>  y)


Proof not projected



Definitions occuring in Statement :  uimplies: b supposing a,  uall: [x:A]. B[x],  and: P  Q,  pair: <a, b>,  product: x:A  B[x],  equal: s = t,  l_member: (x  l)
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  and: P  Q,  l_member: (x  l),  pair: <a, b>,  product: x:A  B[x],  equal: s = t
FDL editor aliases :  compat-trip-lists
compat-trip-lists(x;y;R;S;T)  ==
    \mforall{}[r:R].  \mforall{}[s:S].  \mforall{}[t1,t2:T].    t1  =  t2  supposing  (<r,  s,  t1>  \mmember{}  x)  \mwedge{}  (<r,  s,  t2>  \mmember{}  y)


Date html generated: 2011_10_20-PM-04_58_50
Last ObjectModification: 2011_05_10-PM-05_23_04

Home Index