Nuprl Lemma : sv-list-equal
∀T:Type. ∀L1,L2:T List. ∀x:T.
  (single-valued-list(L1;T)
  
⇒ single-valued-list(L2;T)
  
⇒ (x ∈ L1)
  
⇒ (x ∈ L2)
  
⇒ (||L1|| = ||L2|| ∈ ℤ)
  
⇒ (L1 = L2 ∈ (T List)))
Proof
Definitions occuring in Statement : 
single-valued-list: single-valued-list(L;T)
, 
l_member: (x ∈ l)
, 
length: ||as||
, 
list: T List
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
int: ℤ
, 
universe: Type
, 
equal: s = t ∈ T
Definitions unfolded in proof : 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
uimplies: b supposing a
, 
single-valued-list: single-valued-list(L;T)
, 
nat: ℕ
, 
ge: i ≥ j 
, 
decidable: Dec(P)
, 
or: P ∨ Q
, 
satisfiable_int_formula: satisfiable_int_formula(fmla)
, 
exists: ∃x:A. B[x]
, 
false: False
, 
not: ¬A
, 
top: Top
, 
and: P ∧ Q
, 
prop: ℙ
, 
int_seg: {i..j-}
, 
lelt: i ≤ j < k
, 
le: A ≤ B
Latex:
\mforall{}T:Type.  \mforall{}L1,L2:T  List.  \mforall{}x:T.
    (single-valued-list(L1;T)
    {}\mRightarrow{}  single-valued-list(L2;T)
    {}\mRightarrow{}  (x  \mmember{}  L1)
    {}\mRightarrow{}  (x  \mmember{}  L2)
    {}\mRightarrow{}  (||L1||  =  ||L2||)
    {}\mRightarrow{}  (L1  =  L2))
Date html generated:
2016_05_17-AM-11_10_14
Last ObjectModification:
2016_01_18-AM-00_11_08
Theory : process-model
Home
Index