---

Step * 1 2 1 1 of Lemma decidable__archive-condition


1. [V] : Type
2. v0 : V@i
3. A : Id List@i
4. t : ℕ+@i
5. f : (V List) ─→ V@i
6. v1 : 𝔹@i
7. v3 : ℤ@i
8. v5 : {a:Id| (a ∈ A)}  List@i
9. v7 : V List@i
10. v8 : V@i
11. ff = v1
12. 0 = v3 ∈ ℤ
13. [] = v5 ∈ ({a:Id| (a ∈ A)}  List)
14. [] = v7 ∈ (V List)
15. v0 = v8 ∈ V
⊢ Dec(∃n:ℕ. ∃v:V. ((↑v1) ∧ ((n + 1) = v3 ∈ ℤ) ∧ (v = v8 ∈ V)))
BY
{ ((OrRight THEN Auto) THEN (D 0 THENA Auto) THEN ExRepD THEN Auto')⋅ }

---

Latex:



1.  [V]  :  Type
2.  v0  :  V@i
3.  A  :  Id  List@i
4.  t  :  \mBbbN{}\msupplus{}@i
5.  f  :  (V  List)  {}\mrightarrow{}  V@i
6.  v1  :  \mBbbB{}@i
7.  v3  :  \mBbbZ{}@i
8.  v5  :  \{a:Id|  (a  \mmember{}  A)\}    List@i
9.  v7  :  V  List@i
10.  v8  :  V@i
11.  ff  =  v1
12.  0  =  v3
13.  []  =  v5
14.  []  =  v7
15.  v0  =  v8
\mvdash{}  Dec(\mexists{}n:\mBbbN{}.  \mexists{}v:V.  ((\muparrow{}v1)  \mwedge{}  ((n  +  1)  =  v3)  \mwedge{}  (v  =  v8)))


By

((OrRight  THEN  Auto)  THEN  (D  0  THENA  Auto)  THEN  ExRepD  THEN  Auto')\mcdot{}

---

Home Index