Thms det automata Sections AutomataTheory Doc

DA_act Def a == 1of(a)

Thm* Alph,States:Type, a:Automata(Alph;States). a StatesAlphStates

DA_fin Def FinalState(a) == 2of(2of(a))

Thm* Alph,States:Type, a:Automata(Alph;States). FinalState(a) States

DA_init Def InitialState(a) == 1of(2of(a))

Thm* Alph,States:Type, a:Automata(Alph;States). InitialState(a) States

automata Def Automata(Alph;States) == (StatesAlphStates)States(States)

Thm* Alph,States:Type{i}. Automata(Alph;States) Type{i'}

pi1 Def 1of(t) == t.1

Thm* A:Type, B:(AType), p:a:AB(a). 1of(p) A

pi2 Def 2of(t) == t.2

Thm* A:Type, B:(AType), p:a:AB(a). 2of(p) B(1of(p))

About:
!abstractionspreadalluniversefunctionproductmemberbool