PrintForm
Definitions
nfa
1
Sections
AutomataTheory
Doc
At:
nd
compute
list
wf
1
2
1
1.
Alph:
Type
2.
St:
Type
3.
NDA:
NDA(Alph;St)
4.
l:
Alph*
5.
u:
Alph
6.
v:
Alph*
7.
q:St. NDA(v)
q
Prop
8.
q:
St
NDA(u.v)
q
Prop
By:
RecUnfold `nd_compute_list` 0
Generated subgoal:
1
if null(u.v)
q = I(NDA) else
t:St. NDA(tl((u.v)))
t &
NDA(t,hd((u.v)),q) fi
Prop
About:
if null(u.v)
q = I(NDA) else 
t:St. NDA(tl((u.v)))t & 
NDA(t,hd((u.v)),q) fi 
Prop
q:St. NDA(v)q Prop NDA(u.v)q Prop if null(u.v) q = I(NDA) else t:St. NDA(tl((u.v)))t & NDA(t,hd((u.v)),q) fi Prop
