---

Step * 2 of Lemma decidable__sublist-rec

.....decidable?..... 
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)@i
3. u : T@i
4. v : T List@i
5. ∀l1:T List. Dec(sublist-rec(T;l1;v))@i
6. l1 : T List@i
⊢ Dec(sublist-rec(T;l1;[u / v]))
BY
{ (DVar `l1'
   THEN Try (Complete ((RWO "sublist-rec-nil-iff" 0 THEN Auto)))
   THEN RecUnfold `sublist-rec` 0
   THEN Reduce 0
   THEN (InstHyp [⌜[u1 / v1]⌝] (-3)⋅ THENA Auto)
   THEN D (-1)
   THEN Try (Complete (((OrLeft THENA Auto) THEN OrRight THEN Auto)))
   THEN (InstHyp [⌜v1⌝] (-4)⋅ THENA Auto)
   THEN D (-1)
   THEN Try (Complete (((OrRight THENA Auto) THEN (D 0 THENA Auto) THEN D (-1) THEN Auto)))
   THEN (InstHyp [⌜u1⌝;⌜u⌝] (-8)⋅ THENA Auto)
   THEN D (-1)
   THEN Try (Complete (RepeatFor 2 ((OrLeft THEN Auto))))
   THEN (OrRight THENA Auto)
   THEN (D 0 THENA Auto)
   THEN D (-1)
   THEN Auto) }

---

Latex:

---

Latex:
.....decidable?..... 
1.  [T]  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)@i
3.  u  :  T@i
4.  v  :  T  List@i
5.  \mforall{}l1:T  List.  Dec(sublist-rec(T;l1;v))@i
6.  l1  :  T  List@i
\mvdash{}  Dec(sublist-rec(T;l1;[u  /  v]))


By

---

Latex:
(DVar  `l1'
  THEN  Try  (Complete  ((RWO  "sublist-rec-nil-iff"  0  THEN  Auto)))
  THEN  RecUnfold  `sublist-rec`  0
  THEN  Reduce  0
  THEN  (InstHyp  [\mkleeneopen{}[u1  /  v1]\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  Try  (Complete  (((OrLeft  THENA  Auto)  THEN  OrRight  THEN  Auto)))
  THEN  (InstHyp  [\mkleeneopen{}v1\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  Try  (Complete  (((OrRight  THENA  Auto)  THEN  (D  0  THENA  Auto)  THEN  D  (-1)  THEN  Auto)))
  THEN  (InstHyp  [\mkleeneopen{}u1\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]  (-8)\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  Try  (Complete  (RepeatFor  2  ((OrLeft  THEN  Auto))))
  THEN  (OrRight  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  D  (-1)
  THEN  Auto)

---

Home Index