PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
en
inj
n:
, m:
, l1,l2:
n*. ||l1|| = m & ||l2|| = m
en(l1) = en(l2)
l1 = l2
By:
Analyze 0
THEN
Analyze 0
Generated subgoal:
1
1.
n:
2.
m:
l1,l2:
n*. ||l1|| = m & ||l2|| = m
en(l1) = en(l2)
l1 = l2
About:
l1,l2:n*. ||l1|| = m & ||l2|| = m 
en(l1) = en(l2) l1 = l2 n:, m:, l1,l2:n*. ||l1|| = m & ||l2|| = m en(l1) = en(l2) l1 = l2 l1,l2:n*. ||l1|| = m & ||l2|| = m en(l1) = en(l2) l1 = l2
