Nuprl - Pf nd_comp_extend

PrintForm Definitions nfa 1 Sections AutomataTheory Doc

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

(map(c. < 1of(c),a.2of(c) > ;C) @ [ < q,nil > ]) {C:{l:((StAlph*)*)| ||l|| > 0 }| i:(||C||-1). ||2of(C[i])|| > 0 }

By: Analyze

Generated subgoals:

1 (map(c. < 1of(c),a.2of(c) > ;C) @ [ < q,nil > ]) {l:((StAlph*)*)| ||l|| > 0 }

2 6. 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:

1	`(map(c. < 1of(c),a.2of(c) > ;C) @ [ < q,nil > ]) {l:((StAlph))\| \|\|l\|\| > 0 }`
2	6. `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`