Nuprl Definition : compat-pair-lists
compat-pair-lists(x;y;S;T) == 
[s:S]. [t1,t2:T]. t1 = t2 supposing (<s, t1> 
x) 
(<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-pair-lists
compat-pair-lists(x;y;S;T) == \mforall{}[s:S]. \mforall{}[t1,t2:T]. t1 = t2 supposing (<s, t1> \mmember{} x) \mwedge{} (<s, t2> \mmember{} y)
Date html generated:
2011_10_20-PM-04_58_24
Last ObjectModification:
2011_05_10-PM-05_07_04
Home
Index