Definitions
GenAutomata
Sections
NuprlLIB
Doc
No mentions to report in GenAutomata
union1
Def union1() ==
+Type+(
)
Thm* union1{i}()
Type{i'}
nat
Def
== {i:
| 0
i }
Thm*
Type
le
Def
A
B ==
B < A
Thm*
i,j:
. (i
j)
Prop
not
Def
A == A
False
Thm*
A:Prop. (
A)
Prop
Syntax:
union1()
has structure:
union1{i:l}
About:
Definitions
GenAutomata
Sections
NuprlLIB
Doc