nfa 1 Sections AutomataTheory Doc

NDA_fin Def F(n) == 2of(2of(n))

Thm* Alph,States:Type, n:NDA(Alph;States). F(n) States

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

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

About:
!abstractionspreadalluniversefunctionproductmemberbool