Thms
finite
sets
Sections
AutomataTheory
Doc
decidable
Def
Dec(P) == P
P
Thm*
A:Prop. Dec(A)
Prop
so_lambda2
Def (
1,2. b(1;2))(1,2) == b(1;2)
not
Def
A == A
False
Thm*
A:Prop. (
A)
Prop
About:
P
A:Prop. Dec(A) 
Prop
1,2. b(1;2))(1,2) == b(1;2)
A == A 
False
A:Prop. (A) Prop P
1,2. b(1;2))(1,2) == b(1;2)
A == A False
