PrintForm Definitions det automata Sections AutomataTheory Doc

At: reach aux 1 1 1 1 2 2 1 1 2
1. Alph: Type
2. S: ActionSet(Alph)
3. si: S.car
4. Fin(S.car)
5. n:
6. f: nAlph
7. g: Alphn
8. InvFuns(n; Alph; f; g)
9. n1:
10. f1: n1S.car
11. g1: S.carn1
12. InvFuns(n1; S.car; f1; g1)
13. RL: {y:{x:(S.car*)| 0 < ||x|| & ||x||n1+1 }| y[(||y||-1)] = si }
14. ||RL|| = n1+1
15. i:||RL||, j:i. RL[i] = RL[j]
16. s:S.car. mem_f(S.car;s;RL) (w:Alph*. (S:wsi) = s)
17. i: (n1+1)
18. j: i
19. g1(RL[i]) = g1(RL[j])
20. f1(g1(RL[i])) = f1(g1(RL[j]))

RL[i] = RL[j]
By:
RWH add_composeC -1
THEN
Analyze 12
Generated subgoal:

112. g1 o f1 = Id
13. f1 o g1 = Id
14. RL: {y:{x:(S.car*)| 0 < ||x|| & ||x||n1+1 }| y[(||y||-1)] = si }
15. ||RL|| = n1+1
16. i:||RL||, j:i. RL[i] = RL[j]
17. s:S.car. mem_f(S.car;s;RL) (w:Alph*. (S:wsi) = s)
18. i: (n1+1)
19. j: i
20. g1(RL[i]) = g1(RL[j])
21. (f1 o g1)(RL[i]) = (f1 o g1)(RL[j])
RL[i] = RL[j]

About:
equaluniversefunctionnatural_numbersetlistandless_than
addsubtractintallimpliesexistsapply