---

Step * 2 of Lemma fun-path-no_repeats


1. T : Type
2. f : T ⟶ T
3. h : T ⟶ ℕ
4. ∀x:T. (((f x) = x ∈ T) ∨ h (f x) < h x)
5. L : T List
6. x : T
7. y : T
8. x=f*(y) via L
9. ∀j:ℕ||L||. ∀i:ℕj.  h L[i] < h L[j]
⊢ no_repeats(T;L)
BY
{ xxx(BLemma `no_repeats_iff`
      THEN Auto
      THEN (D (-1))
      THEN All Reduce
      THEN Auto
      THEN ((((InstHyp [⌜0⌝] (-1))⋅ THENM ((Reduce (-1)) THEN (HypSubst' -1 0 THENM (Thin (-1)))))
             THENM (InstHyp [⌜1⌝] (-1))⋅
             THENM ((Reduce (-1)) THEN (HypSubst' -1 0 THENM (Thin (-1)))))
            THENA Auto'
            ))xxx }

1
1. T : Type
2. f : T ⟶ T
3. h : T ⟶ ℕ
4. ∀x:T. (((f x) = x ∈ T) ∨ h (f x) < h x)
5. L : T List
6. x : T
7. y : T
8. x=f*(y) via L
9. ∀j:ℕ||L||. ∀i:ℕj.  h L[i] < h L[j]
10. x1 : T
11. y1 : T
12. f1 : ℕ2 ⟶ ℕ||L||
13. increasing(f1;2)
14. ∀j:ℕ2. ([x1; y1][j] = L[f1 j] ∈ T)
⊢ ¬(L[f1 0] = L[f1 1] ∈ T)

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  T
3.  h  :  T  {}\mrightarrow{}  \mBbbN{}
4.  \mforall{}x:T.  (((f  x)  =  x)  \mvee{}  h  (f  x)  <  h  x)
5.  L  :  T  List
6.  x  :  T
7.  y  :  T
8.  x=f*(y)  via  L
9.  \mforall{}j:\mBbbN{}||L||.  \mforall{}i:\mBbbN{}j.    h  L[i]  <  h  L[j]
\mvdash{}  no\_repeats(T;L)


By

---

Latex:
xxx(BLemma  `no\_repeats\_iff`
        THEN  Auto
        THEN  (D  (-1))
        THEN  All  Reduce
        THEN  Auto
        THEN  ((((InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-1))\mcdot{}  THENM  ((Reduce  (-1))  THEN  (HypSubst'  -1  0  THENM  (Thin  (-1)))))
                      THENM  (InstHyp  [\mkleeneopen{}1\mkleeneclose{}]  (-1))\mcdot{}
                      THENM  ((Reduce  (-1))  THEN  (HypSubst'  -1  0  THENM  (Thin  (-1)))))
                    THENA  Auto'
                    ))xxx

---

Home Index