Def (qn) == if n=0 0 else (qn-1)+(qn-1) fi (recursive)

Thm* q,n:. (qn)

Def (basepower) == if power=0 1 else base(basepower-1) fi (recursive)

Thm* n,k:. (nk)

Thm* n,k:. (nk)

Def i=j == if i=j true ; false fi

Thm* i,j:. i=j