PrintForm Definitions action sets Sections AutomataTheory Doc

At: n0n1 irregular 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 2 1 1 1 1 1 1 1 1
1. S: ActionSet()
2. s: S.car
3. q: S.car
4. n:
5. f: S.carn
6. g: nS.car
7. g o f = Id
8. f o g = Id
9. k:. (S:n0n1(k)s) = q
10. i: (n+1)
11. j: (n+1)
12. i < j
13. f((S:([1]i)s)) = f((S:([1]j)s))
14. (S:([1]i)s) = (S:([1]j)s)
15. k:
16. (([0]j) @ ([1]i)) = (([0]k) @ ([1]k))
17. k = i
18. j||0:[0]||+i||0:[1]|| = k||0:[0]||+k||0:[1]||
19. ||0:([0]j)||+||0:([1]i)||0

False
By: RWH (RecUnfoldC `el_counter`) 18
Generated subgoal:

118. jif null([0])0 ;0=hd([0])1+||0:tl([0])|| else ||0:tl([0])|| fi +iif null([1])0 ;0=hd([1])1+||0:tl([1])|| else ||0:tl([1])|| fi = kif null([0])0 ;0=hd([0])1+||0:tl([0])|| else ||0:tl([0])|| fi +kif null([1])0 ;0=hd([1])1+||0:tl([1])|| else ||0:tl([1])|| fi
19. ||0:([0]j)||+||0:([1]i)||0
False

About:
falseintfunctionnatural_numberequalalladd
less_thanapplyconsnillistmultiply