PrintForm Definitions exponent Sections AutomataTheory Doc

At: en inj 1
1. n:
2. m:

l1,l2:n*. ||l1|| = m & ||l2|| = m en(l1) = en(l2) l1 = l2
By: NatInd 2
Generated subgoals:

1 l1,l2:n*. ||l1|| = 0 & ||l2|| = 0 en(l1) = en(l2) l1 = l2
22. m:
3. 0 < m
4. l1,l2:n*. ||l1|| = m-1 & ||l2|| = m-1 en(l1) = en(l2) l1 = l2
l1,l2:n*. ||l1|| = m & ||l2|| = m en(l1) = en(l2) l1 = l2

About:
alllistnatural_numberimpliesandequalint