---

Step * 2 2 1 of Lemma agree_on_common_append


1. [T] : Type
2. u : T
3. v : T List
4. ∀bs,cs,ds:T List.
     (agree_on_common(T;v;cs) ⇒ agree_on_common(T;bs;ds) ⇒ agree_on_common(T;v @ bs;cs @ ds)) supposing 
        ((∀x∈v.¬(x ∈ ds)) and 
        (∀x∈cs.¬(x ∈ bs)))
5. bs : T List
6. u1 : T
7. v1 : T List
8. ∀ds:T List
     (agree_on_common(T;[u / v];v1) ⇒ agree_on_common(T;bs;ds) ⇒ agree_on_common(T;[u / (v @ bs)];v1 @ ds)) supposing 
        ((∀x∈[u / v].¬(x ∈ ds)) and 
        (∀x∈v1.¬(x ∈ bs)))
9. ds : T List
10. (∀x∈[u1 / v1].¬(x ∈ bs))
11. (∀x∈[u / v].¬(x ∈ ds))
12. agree_on_common(T;[u / v];[u1 / v1])
13. agree_on_common(T;bs;ds)
⊢ agree_on_common(T;[u / (v @ bs)];[u1 / (v1 @ ds)])
BY
{ ((((((AllHyps (RWO "l_all_cons") THENA Auto) THEN RecUnfold `agree_on_common` (-2)) THEN Reduce (-2))
     THEN RecUnfold `agree_on_common` 0
     )
    THEN Reduce 0
    )
   THEN RepeatFor 2 (ParallelOp (-2))
   ) }

1
1. [T] : Type
2. u : T
3. v : T List
4. ∀bs,cs,ds:T List.
     (agree_on_common(T;v;cs) ⇒ agree_on_common(T;bs;ds) ⇒ agree_on_common(T;v @ bs;cs @ ds)) supposing 
        ((∀x∈v.¬(x ∈ ds)) and 
        (∀x∈cs.¬(x ∈ bs)))
5. bs : T List
6. u1 : T
7. v1 : T List
8. ∀ds:T List
     (agree_on_common(T;[u / v];v1) ⇒ agree_on_common(T;bs;ds) ⇒ agree_on_common(T;[u / (v @ bs)];v1 @ ds)) supposing 
        (((¬(u ∈ ds)) ∧ (∀x∈v.¬(x ∈ ds))) and 
        (∀x∈v1.¬(x ∈ bs)))
9. ds : T List
10. (¬(u1 ∈ bs)) ∧ (∀x∈v1.¬(x ∈ bs))
11. (¬(u ∈ ds)) ∧ (∀x∈v.¬(x ∈ ds))
12. agree_on_common(T;v;[u1 / v1])
13. ¬(u ∈ [u1 / v1])
14. agree_on_common(T;bs;ds)
⊢ ¬(u ∈ [u1 / (v1 @ ds)])

2
1. [T] : Type
2. u : T
3. v : T List
4. ∀bs,cs,ds:T List.
     (agree_on_common(T;v;cs) ⇒ agree_on_common(T;bs;ds) ⇒ agree_on_common(T;v @ bs;cs @ ds)) supposing 
        ((∀x∈v.¬(x ∈ ds)) and 
        (∀x∈cs.¬(x ∈ bs)))
5. bs : T List
6. u1 : T
7. v1 : T List
8. ∀ds:T List
     (agree_on_common(T;[u / v];v1) ⇒ agree_on_common(T;bs;ds) ⇒ agree_on_common(T;[u / (v @ bs)];v1 @ ds)) supposing 
        (((¬(u ∈ ds)) ∧ (∀x∈v.¬(x ∈ ds))) and 
        (∀x∈v1.¬(x ∈ bs)))
9. ds : T List
10. (¬(u1 ∈ bs)) ∧ (∀x∈v1.¬(x ∈ bs))
11. (¬(u ∈ ds)) ∧ (∀x∈v.¬(x ∈ ds))
12. ¬(u ∈ [u1 / v1])
13. agree_on_common(T;v;[u1 / v1])
14. agree_on_common(T;bs;ds)
⊢ agree_on_common(T;v @ bs;[u1 / (v1 @ ds)])

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

4
1. [T] : Type
2. u : T
3. v : T List
4. ∀bs,cs,ds:T List.
     (agree_on_common(T;v;cs) ⇒ agree_on_common(T;bs;ds) ⇒ agree_on_common(T;v @ bs;cs @ ds)) supposing 
        ((∀x∈v.¬(x ∈ ds)) and 
        (∀x∈cs.¬(x ∈ bs)))
5. bs : T List
6. u1 : T
7. v1 : T List
8. ∀ds:T List
     (agree_on_common(T;[u / v];v1) ⇒ agree_on_common(T;bs;ds) ⇒ agree_on_common(T;[u / (v @ bs)];v1 @ ds)) supposing 
        (((¬(u ∈ ds)) ∧ (∀x∈v.¬(x ∈ ds))) and 
        (∀x∈v1.¬(x ∈ bs)))
9. ds : T List
10. (¬(u1 ∈ bs)) ∧ (∀x∈v1.¬(x ∈ bs))
11. (¬(u ∈ ds)) ∧ (∀x∈v.¬(x ∈ ds))
12. (u = u1 ∈ T) ∧ agree_on_common(T;v;v1)
13. agree_on_common(T;bs;ds)
⊢ (u = u1 ∈ T) ∧ agree_on_common(T;v @ bs;v1 @ ds)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}bs,cs,ds:T  List.
          (agree\_on\_common(T;v;cs)
                {}\mRightarrow{}  agree\_on\_common(T;bs;ds)
                {}\mRightarrow{}  agree\_on\_common(T;v  @  bs;cs  @  ds))  supposing 
                ((\mforall{}x\mmember{}v.\mneg{}(x  \mmember{}  ds))  and 
                (\mforall{}x\mmember{}cs.\mneg{}(x  \mmember{}  bs)))
5.  bs  :  T  List
6.  u1  :  T
7.  v1  :  T  List
8.  \mforall{}ds:T  List
          (agree\_on\_common(T;[u  /  v];v1)
                {}\mRightarrow{}  agree\_on\_common(T;bs;ds)
                {}\mRightarrow{}  agree\_on\_common(T;[u  /  (v  @  bs)];v1  @  ds))  supposing 
                ((\mforall{}x\mmember{}[u  /  v].\mneg{}(x  \mmember{}  ds))  and 
                (\mforall{}x\mmember{}v1.\mneg{}(x  \mmember{}  bs)))
9.  ds  :  T  List
10.  (\mforall{}x\mmember{}[u1  /  v1].\mneg{}(x  \mmember{}  bs))
11.  (\mforall{}x\mmember{}[u  /  v].\mneg{}(x  \mmember{}  ds))
12.  agree\_on\_common(T;[u  /  v];[u1  /  v1])
13.  agree\_on\_common(T;bs;ds)
\mvdash{}  agree\_on\_common(T;[u  /  (v  @  bs)];[u1  /  (v1  @  ds)])


By

---

Latex:
((((((AllHyps  (RWO  "l\_all\_cons")  THENA  Auto)  THEN  RecUnfold  `agree\_on\_common`  (-2))
        THEN  Reduce  (-2)
        )
      THEN  RecUnfold  `agree\_on\_common`  0
      )
    THEN  Reduce  0
    )
  THEN  RepeatFor  2  (ParallelOp  (-2))
  )

---

Home Index