Thms
myhill
nerode
Sections
AutomataTheory
Doc
beq
Def
p =
q == if p
q else
q fi
Thm*
p,q:
. p =
q
bnot
Def
b == if b
false
else true
fi
Thm*
b:
.
b
About:
q == if p
q else 
q fi
p,q:
. p = q 
b == if b false else true fi
b:. b q == if p q else q fi
b == if b false else true fi
