PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 8 1
1. Alph: Type
2. R: Alph*Alph*Prop
3. n:
4. L: Alph*
5. m:
6. (x:Alph*. R(x,x)) & (x,y:Alph*. R(x,y) R(y,x)) & (x,y,z:Alph*. R(x,y) & R(y,z) R(x,z)) & (x,y,z:Alph*. R(x,y) R((z @ x),z @ y)) & (w:(nAlph*). l:Alph*. i:n. R(l,w(i))) & (v:(mAlph*). l:Alph*. L(l) (i:m. R(l,v(i)))) & Fin(Alph)
7. x: Alph*
8. y: Alph*

Dec(l:Alph*. L(l @ x) = L(l @ y))
By: Inst Thm* P:(TProp). (x:T. Dec(P(x))) & Dec(x:T. P(x)) Dec(x:T. P(x)) [Alph*;l.L(l @ x) = L(l @ y)]
Generated subgoals:

16. x:Alph*. R(x,x)
7. x,y:Alph*. R(x,y) R(y,x)
8. x,y,z:Alph*. R(x,y) & R(y,z) R(x,z)
9. x,y,z:Alph*. R(x,y) R((z @ x),z @ y)
10. w:(nAlph*). l:Alph*. i:n. R(l,w(i))
11. v:(mAlph*). l:Alph*. L(l) (i:m. R(l,v(i)))
12. Fin(Alph)
13. x: Alph*
14. y: Alph*
15. x@0: Alph*
Dec((l.L(l @ x) = L(l @ y))(x@0))
26. x:Alph*. R(x,x)
7. x,y:Alph*. R(x,y) R(y,x)
8. x,y,z:Alph*. R(x,y) & R(y,z) R(x,z)
9. x,y,z:Alph*. R(x,y) R((z @ x),z @ y)
10. w:(nAlph*). l:Alph*. i:n. R(l,w(i))
11. v:(mAlph*). l:Alph*. L(l) (i:m. R(l,v(i)))
12. Fin(Alph)
13. x: Alph*
14. y: Alph*
Dec(x@0:Alph*. (l.L(l @ x) = L(l @ y))(x@0))
39. Dec(x@0:Alph*. (l.L(l @ x) = L(l @ y))(x@0))
Dec(l:Alph*. L(l @ x) = L(l @ y))

About:
alllistequalboolapplylambdauniverse
functionpropandimpliesexistsnatural_numberassert