PrintForm
Definitions
list
3
autom
Sections
AutomataTheory
Doc
At:
shorten
list
1
1.
T:
Type
2.
L:
T*
3.
La:
T*
4.
Fin(T)
La':T*. (
t:T. False
mem_f(T;t;L)
mem_f(T;t;La')) & (
t:T. mem_f(T;t;La')
False) & (||La'||
1
mem_f(T;hd(La');L))
By:
InstConcl [nil]
THEN
Reduce 0
Generated subgoals:
None
About:
La':T*.
(
t:T. False 
mem_f(T;t;L) 
mem_f(T;t;La'))
& (t:T. mem_f(T;t;La') False)
& (||La'||
1 
mem_f(T;hd(La');L))
