Nuprl - Pf mn_23_lem_1 1 1 1 2 1 1 1

PrintForm Definitions myhill nerode Sections AutomataTheory Doc

1. Alph: Type
2. R: Alph*Alph*Prop
3. Fin(Alph)
4. EquivRel x,y:Alph*. x R y
5. Fin(x,y:Alph*//(x R y))
6. x,y,z:Alph*. (x R y) ((z @ x) R (z @ y))
7. g: (x,y:Alph*//(x R y))
8. x: x,y:Alph*//(x R y)
9. y: x,y:Alph*//(x R y)

< (x,y:Alph*//(x R y))(x,y:Alph*//(x R y)),a,p. p/x,y. < a.x,a.y > > ActionSet(Alph)

By: Unfold `action_set` 0

Generated subgoals:

1 10. a: Alph
11. p: (x,y:Alph*//(x R y))(x,y:Alph*//(x R y))
12. x1: x,y:Alph*//(x R y)
13. y1: x,y:Alph*//(x R y)
14. p = < x1,y1 >
a.x1 x,y:Alph*//(x R y)

2 10. a: Alph
11. p: (x,y:Alph*//(x R y))(x,y:Alph*//(x R y))
12. x1: x,y:Alph*//(x R y)
13. y1: x,y:Alph*//(x R y)
14. p = < x1,y1 >
a.y1 x,y:Alph*//(x R y)

About:

1	10. `a:` `Alph` 11. `p:` `(x,y:Alph//(x R y))(x,y:Alph//(x R y))` 12. `x1:` `x,y:Alph//(x R y)` 13. `y1:` `x,y:Alph//(x R y)` 14. `p = < x1,y1 >` `a.x1 x,y:Alph*//(x R y)`
2	10. `a:` `Alph` 11. `p:` `(x,y:Alph//(x R y))(x,y:Alph//(x R y))` 12. `x1:` `x,y:Alph//(x R y)` 13. `y1:` `x,y:Alph//(x R y)` 14. `p = < x1,y1 >` `a.y1 x,y:Alph*//(x R y)`