(2steps)
PrintForm
Definitions
Lemmas
mb
automata
4
Sections
GenAutomata
Doc
At:
ioa
trans
all
wf
A:ioa{i:l}(), I:Fmla. ioa_trans_all{i}(A;I)
VCs
By:
Unfolds [`vcs`;`ioa_trans_all`] 0
Generated subgoal:
1
1.
A:
ioa{i:l}()
2.
I:
Fmla{i}
A
ioa{i':l}
About:
(2steps)
PrintForm
Definitions
Lemmas
mb
automata
4
Sections
GenAutomata
Doc