Step
*
of Lemma
merge-int-one-one
∀[T:Type]
∀[as,bs,cs:T List].
(as = bs ∈ (T List)) supposing
((merge-int(cs;as) = merge-int(cs;bs) ∈ (T List)) and
sorted(bs) and
sorted(as) and
sorted(cs))
supposing T ⊆r ℤ
BY
{ (Auto THEN (RWO "merge-int-comm" (-1) THENA Auto) THEN FLemma `merge-int-1-1` [-1] THEN Auto) }
Latex:
Latex:
\mforall{}[T:Type]
\mforall{}[as,bs,cs:T List].
(as = bs) supposing
((merge-int(cs;as) = merge-int(cs;bs)) and
sorted(bs) and
sorted(as) and
sorted(cs))
supposing T \msubseteq{}r \mBbbZ{}
By
Latex:
(Auto THEN (RWO "merge-int-comm" (-1) THENA Auto) THEN FLemma `merge-int-1-1` [-1] THEN Auto)
Home
Index