Nuprl - Pf nd_comp_init

PrintForm Definitions nfa 1 Sections AutomataTheory Doc

Alph,St:Type, NDA:NDA(Alph;St). NDA([ < I(NDA),[] > ]) I(NDA)

By: Unfold `nd_valcom` 0 THEN Unfold `nd_comp_init` 0

Generated subgoals:

1 1. Alph: Type
2. St: Type
3. NDA: NDA(Alph;St)
I(NDA) = 1of(hd([ < I(NDA),nil > ]))

2 1. Alph: Type
2. St: Type
3. NDA: NDA(Alph;St)
4. i: (||[ < I(NDA),nil > ]||-1)
NDA(1of([ < I(NDA),nil > ][i]),hd(rev(2of([ < I(NDA),nil > ][i]))),1of([ < I(NDA),nil > ][(i+1)]))

3 1. Alph: Type
2. St: Type
3. NDA: NDA(Alph;St)
4. i: (||[ < I(NDA),nil > ]||-1)
2of([ < I(NDA),nil > ][(i+1)]) = rev(tl(rev(2of([ < I(NDA),nil > ][i])))) Alph*

4 1. Alph: Type
2. St: Type
3. NDA: NDA(Alph;St)
||[ < I(NDA),nil > ]||

5 1. Alph: Type
2. St: Type
3. NDA: NDA(Alph;St)
1of(hd(rev([ < I(NDA),nil > ]))) = I(NDA)

6 1. Alph: Type
2. St: Type
3. NDA: NDA(Alph;St)
2of(hd(rev([ < I(NDA),nil > ]))) = nil Alph*

About:

1	1. `Alph:` `Type` 2. `St:` `Type` 3. `NDA:` `NDA(Alph;St)` `I(NDA) = 1of(hd([ < I(NDA),nil > ]))`
2	1. `Alph:` `Type` 2. `St:` `Type` 3. `NDA:` `NDA(Alph;St)` 4. `i:` `(\|\|[ < I(NDA),nil > ]\|\|-1)` `NDA(1of([ < I(NDA),nil > ][i]),hd(rev(2of([ < I(NDA),nil > ][i]))),1of([ < I(NDA),nil > ][(i+1)]))`
3	1. `Alph:` `Type` 2. `St:` `Type` 3. `NDA:` `NDA(Alph;St)` 4. `i:` `(\|\|[ < I(NDA),nil > ]\|\|-1)` `2of([ < I(NDA),nil > ][(i+1)]) = rev(tl(rev(2of([ < I(NDA),nil > ][i])))) Alph*`
4	1. `Alph:` `Type` 2. `St:` `Type` 3. `NDA:` `NDA(Alph;St)` `\|\|[ < I(NDA),nil > ]\|\|`
5	1. `Alph:` `Type` 2. `St:` `Type` 3. `NDA:` `NDA(Alph;St)` `1of(hd(rev([ < I(NDA),nil > ]))) = I(NDA)`
6	1. `Alph:` `Type` 2. `St:` `Type` 3. `NDA:` `NDA(Alph;St)` `2of(hd(rev([ < I(NDA),nil > ]))) = nil Alph*`