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