At: nd auto eq auto 1 1 2 1 1 1 1 1 2 2 1 1 2 1 1 1
1. Alph: Type
2. St: Type
3. NDA: NDA(Alph;St)
4. Fin(St)
5. 
x,y:St, a:Alph. Dec(
NDA(x,a,y))
6. y:St. Dec(I(NDA) = y)
7. g: St
8. t:St. I(NDA) = t 
g(t)
9. f:(St). Dec(
s:St. f(s) & F(NDA)(s))
10. g1: (St)
11. t:(St). (s:St. t(s) & F(NDA)(s)) g1(t)
12. f:(St), a:Alph, y:St. Dec(s:St. f(s) & NDA(s,a,y))
13. t: (St)
AlphSt
14. Dec(s:St. 1of(t)(s) & NDA(s,1of(2of(t)),2of(2of(t))))
Dec((
t.s:St. 1of(t)(s) & NDA(s,1of(2of(t)),2of(2of(t))))(t))
By: Reduce 0
Generated subgoals:None
About:
