Def Min{ x | xEn } == MinArg(E(n) : {0..n})

Thm* E:(), n:. Min{ x | xEn }

Def MinArg(f : {0..n}) == n-MinAr(f;n;n)

Thm* f:(), n:. MinArg(f : {0..n}) (n+1)

Def MinAr(f;i;n) == if (f(n-i))=(f(n)) i else MinAr(f;i-1;n) fi (recursive)

Thm* f:(), n:, i:(n+1). MinAr(f;i;n) (i+1)

Def p=q == (pq) (pq)

Thm* p,q:. p=q

Def b == if b false else true fi

Thm* b:. b

Def pq == if p q else false fi

Thm* p,q:. (pq)

Def p q == if p true else q fi

Thm* p,q:. (p q)