PrintForm Definitions nfa 1 Sections AutomataTheory Doc

At: nd comp extend wf 1 2 1
1. Alph: Type
2. St: Type
3. C: {C:{l:((StAlph*)*)| ||l|| > 0 }| i:(||C||-1). ||2of(C[i])|| > 0 }
4. a: Alph
5. q: St
6. i:
7. 0 i < ||map(c. < 1of(c),a.2of(c) > ;C) @ [ < q,nil > ]||-1

||2of((map(c. < 1of(c),a.2of(c) > ;C) @ [ < q,nil > ])[i])|| > 0
By: RWH (LemmaC Thm* as,bs:T*. ||as @ bs|| = ||as||+||bs||) 7
Generated subgoals:

11. Alph: Type{i}
2. St: Type{i}
3. C: {C:{l:((StAlph*)*)| ||l|| > 0 }| i:(||C||-1). ||2of(C[i])|| > 0 }
4. a: Alph
5. q: St
6. i:
7. 0i
8. i < ||map(c. < 1of(c),a.2of(c) > ;C) @ [ < q,nil > ]||-1
(i < ||map(c. < 1of(c),a.2of(c) > ;C) @ [ < q,nil > ]||-1) = (i < ||map(c. < 1of(c),a.2of(c) > ;C)||+||[ < q,nil > ]||-1)
27. 0 i < ||map(c. < 1of(c),a.2of(c) > ;C)||+||[ < q,nil > ]||-1
||2of((map(c. < 1of(c),a.2of(c) > ;C) @ [ < q,nil > ])[i])|| > 0

About:
lambdapairconsnilnatural_numberuniversealllist
equalintaddsetproductsubtractless_than