Step * of Lemma adjacent-to-same

[T:Type]. ∀[L:T List]. ∀[a,b,c:T].
  (b c ∈ T) supposing (adjacent(T;L;a;c) and adjacent(T;L;a;b) and no_repeats(T;L))
BY
((Auto THEN Using [`z',⌜c⌝(FLemma `before-adjacent2` [6;7])⋅THEN Auto) }

1
.....antecedent..... 
1. Type
2. List
3. T
4. T
5. T
6. no_repeats(T;L)
7. adjacent(T;L;a;b)
8. adjacent(T;L;a;c)
⊢ before c ∈ L

2
1. Type
2. List
3. T
4. T
5. T
6. no_repeats(T;L)
7. adjacent(T;L;a;b)
8. adjacent(T;L;a;c)
9. before c ∈ L ∨ (c b ∈ T)
⊢ c ∈ T


Latex:


Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[a,b,c:T].
    (b  =  c)  supposing  (adjacent(T;L;a;c)  and  adjacent(T;L;a;b)  and  no\_repeats(T;L))


By


Latex:
((Auto  THEN  Using  [`z',\mkleeneopen{}c\mkleeneclose{}]  (FLemma  `before-adjacent2`  [6;7])\mcdot{})  THEN  Auto)




Home Index