Step * 2 1 1 of Lemma agree_on_common_append

.....assertion..... 
1. [T] Type
2. T
3. 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 List
6. ds List
7. (∀x∈[].¬(x ∈ bs))
8. (u ∈ ds)) ∧ (∀x∈v.¬(x ∈ ds))
9. agree_on_common(T;[u v];[])
10. agree_on_common(T;bs;ds)
⊢ agree_on_common(T;v bs;[] ds)
BY
(((BackThruSomeHyp THEN Auto{1,3}-1) THEN BackThruLemma `agree_on_common_nil`) THEN Auto)⋅ }


Latex:


Latex:
.....assertion..... 
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.  ds  :  T  List
7.  (\mforall{}x\mmember{}[].\mneg{}(x  \mmember{}  bs))
8.  (\mneg{}(u  \mmember{}  ds))  \mwedge{}  (\mforall{}x\mmember{}v.\mneg{}(x  \mmember{}  ds))
9.  agree\_on\_common(T;[u  /  v];[])
10.  agree\_on\_common(T;bs;ds)
\mvdash{}  agree\_on\_common(T;v  @  bs;[]  @  ds)


By


Latex:
(((BackThruSomeHyp  THEN  Auto\{1,3\}-1)  THEN  BackThruLemma  `agree\_on\_common\_nil`)  THEN  Auto)\mcdot{}




Home Index