PrintForm
Definitions
automata
6
Sections
AutomataTheory
Doc
At:
auto
oddeven
wf
1
2
1.
n:
2.
s:
(2
n)
3.
a:
n
((s+(2
a)) rem (2
n)) < (2
n)
By:
Inst
Thm*
a:
, n:
. 0
(a rem n) & (a rem n) < n [s+(2
a);(2
n)] THENA Inst
Thm*
m:
, n:
. 0 < (m
n) [2;a]
Generated subgoals:
None
About:
(2
n)n
((s+(2a)) rem (2n)) < (2n)
a:, n:. 0
(a rem n) & (a rem n) < n
[s+(2a);(2n)]
THENA
Inst
Thm* m:, n:. 0 < (mn)
[2;a]