Nuprl - Pf nd_valcom

PrintForm Definitions nfa 1 Sections AutomataTheory Doc

Alph,St:Type, NDA:NDA(Alph;St), C:NComp(Alph;St), q:St. NDA(C) q Prop

By: Unfold `nd_valcom` 0 THEN Unfold `nd_computation` 0 THEN Unfold `list_p` 0 THEN UnivCD THEN Analyze 4 THEN Analyze 4

Generated subgoals:

1 1. Alph: Type
2. St: Type
3. NDA: NDA(Alph;St)
4. C: (StAlph*)*
5. ||C|| > 0
6. i:(||C||-1). ||2of(C[i])|| > 0
7. q: St
8. i: (||C||-1)
||rev(2of(C[i]))||1

2 1. Alph: Type
2. St: Type
3. NDA: NDA(Alph;St)
4. C: (StAlph*)*
5. ||C|| > 0
6. i:(||C||-1). ||2of(C[i])|| > 0
7. q: St
||rev(C)||1

3 1. Alph: Type
2. St: Type
3. NDA: NDA(Alph;St)
4. C: (StAlph*)*
5. ||C|| > 0
6. i:(||C||-1). ||2of(C[i])|| > 0
7. q: St
||rev(C)||1

About:

1	1. `Alph:` `Type` 2. `St:` `Type` 3. `NDA:` `NDA(Alph;St)` 4. `C:` `(StAlph)` 5. `\|\|C\|\| > 0` 6. `i:(\|\|C\|\|-1). \|\|2of(C[i])\|\| > 0` 7. `q:` `St` 8. `i:` `(\|\|C\|\|-1)` `\|\|rev(2of(C[i]))\|\|1`
2	1. `Alph:` `Type` 2. `St:` `Type` 3. `NDA:` `NDA(Alph;St)` 4. `C:` `(StAlph)` 5. `\|\|C\|\| > 0` 6. `i:(\|\|C\|\|-1). \|\|2of(C[i])\|\| > 0` 7. `q:` `St` `\|\|rev(C)\|\|1`
3	1. `Alph:` `Type` 2. `St:` `Type` 3. `NDA:` `NDA(Alph;St)` 4. `C:` `(StAlph)` 5. `\|\|C\|\| > 0` 6. `i:(\|\|C\|\|-1). \|\|2of(C[i])\|\| > 0` 7. `q:` `St` `\|\|rev(C)\|\|1`