Thms automata 6 Sections AutomataTheory Doc

auto4 Def Auto4 == < (s,a. 1-s),0,(s.s=0) >

Thm* Auto4 Automata(2;2)

eq_int Def i=j == if i=j true ; false fi

Thm* i,j:. i=j

About:
!abstractionint_eqbtruebfalseallint
memberboolpairlambdasubtractnatural_number