---

Step * 1 of Lemma agree_on_common_append


1. [T] : Type
⊢ ∀bs,cs,ds:T List.
    (agree_on_common(T;[];cs) ⇒ agree_on_common(T;bs;ds) ⇒ agree_on_common(T;bs;cs @ ds)) supposing 
       ((∀x∈[].¬(x ∈ ds)) and 
       (∀x∈cs.¬(x ∈ bs)))
BY
{ ((((D 0 THENA Auto) THEN InductionOnList) THEN Reduce 0) THEN Auto) }

1
1. [T] : Type
2. bs : T List
3. u : T
4. v : T List
5. ∀ds:T List
     (agree_on_common(T;[];v) ⇒ agree_on_common(T;bs;ds) ⇒ agree_on_common(T;bs;v @ ds)) supposing 
        ((∀x∈[].¬(x ∈ ds)) and 
        (∀x∈v.¬(x ∈ bs)))
6. ds : T List
7. (∀x∈[u / v].¬(x ∈ bs))
8. (∀x∈[].¬(x ∈ ds))
9. agree_on_common(T;[];[u / v])
10. agree_on_common(T;bs;ds)
⊢ agree_on_common(T;bs;[u / (v @ ds)])

---

Latex:

---

Latex:

1.  [T]  :  Type
\mvdash{}  \mforall{}bs,cs,ds:T  List.
        (agree\_on\_common(T;[];cs)
              {}\mRightarrow{}  agree\_on\_common(T;bs;ds)
              {}\mRightarrow{}  agree\_on\_common(T;bs;cs  @  ds))  supposing 
              ((\mforall{}x\mmember{}[].\mneg{}(x  \mmember{}  ds))  and 
              (\mforall{}x\mmember{}cs.\mneg{}(x  \mmember{}  bs)))


By

---

Latex:
((((D  0  THENA  Auto)  THEN  InductionOnList)  THEN  Reduce  0)  THEN  Auto)

---

Home Index