PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 3 1 1 1 2 1 1 2 1 1 1 1 1 1 1 1 1
1. Alph: Type
2. R: Alph*Alph*Prop
3. n:
4. x:Alph*. R(x,x)
5. x,y:Alph*. R(x,y) R(y,x)
6. x,y,z:Alph*. R(x,y) & R(y,z) R(x,z)
7. x,y,z:Alph*. R(x,y) R((z @ x),z @ y)
8. w: nAlph*
9. l:Alph*. i:n. R(l,w(i))
10. a: Alph*
11. b: Alph*
12. c: Alph*
13. ||a||nn
14. f: Alph*n
15. x:Alph*. R(x,w(f(x)))
16. f1: nn(nn)
17. Surj(nn; (nn); f1)
18. i: (nn+1)
19. j: (nn+1)
20. i < j
21. f1( < f((a[||a||-i..||a||]) @ b),f((a[||a||-i..||a||]) @ c) > ) = f1( < f((a[||a||-j..||a||]) @ b),f((a[||a||-j..||a||]) @ c) > )
22. f((a[||a||-i..||a||]) @ b) = f((a[||a||-j..||a||]) @ b)
23. f((a[||a||-i..||a||]) @ c) = f((a[||a||-j..||a||]) @ c)
24. R(((a[||a||-i..||a||]) @ b),w(f((a[||a||-j..||a||]) @ b)))
25. R(((a[||a||-j..||a||]) @ b),w(f((a[||a||-j..||a||]) @ b)))
26. R(((a[||a||-i..||a||]) @ c),w(f((a[||a||-j..||a||]) @ c)))
27. R(((a[||a||-j..||a||]) @ c),w(f((a[||a||-j..||a||]) @ c)))
28. R(w(f((a[||a||-j..||a||]) @ b)),(a[||a||-i..||a||]) @ b)
29. R(w(f((a[||a||-j..||a||]) @ c)),(a[||a||-i..||a||]) @ c)
30. R(((a[||a||-j..||a||]) @ b),(a[||a||-i..||a||]) @ b)
31. R(((a[||a||-j..||a||]) @ c),(a[||a||-i..||a||]) @ c)

R((a @ b),((a[0..||a||-j]) @ (a[||a||-i..||a||])) @ b) & R((a @ c),((a[0..||a||-j]) @ (a[||a||-i..||a||])) @ c)
By:
InstHyp [(a[||a||-j..||a||]) @ b;(a[||a||-i..||a||]) @ b;a[0..||a||-j]] 7
THEN
InstHyp [(a[||a||-j..||a||]) @ c;(a[||a||-i..||a||]) @ c;a[0..||a||-j]] 7
Generated subgoal:

132. R(((a[0..||a||-j]) @ (a[||a||-j..||a||]) @ b),(a[0..||a||-j]) @ (a[||a||-i..||a||]) @ b)
33. R(((a[0..||a||-j]) @ (a[||a||-j..||a||]) @ c),(a[0..||a||-j]) @ (a[||a||-i..||a||]) @ c)
R((a @ b),((a[0..||a||-j]) @ (a[||a||-i..||a||])) @ b) & R((a @ c),((a[0..||a||-j]) @ (a[||a||-i..||a||])) @ c)

About:
andapplynatural_numbersubtractuniversefunction
listpropallimpliesexistsmultiply
productaddless_thanequalpair