PrintForm Definitions choice 1 Sections AutomataTheory Doc

At: min ar sound

f:(), n:, i:(n+1). f(n-MinAr(f;i;n)) = f(n)
By:
UnivCD
THEN
NSubsetInd 3
THEN
RecCaseSplit `min_ar`
THEN
Assert (n-0 = n)
THEN
RWH (HypC 4) 3
THEN
Analyze 3
Generated subgoals:

None

About:
allfunctionboolnatural_numberaddequalapplysubtract