Selected Objects
| def | min_ar | (rec) MinAr(f;i;n) == if (f(n-i))= (f(n)) i else MinAr(f;i-1;n) fi |
| THM | min_ar_alt |  f:(    ), n:, i:(n+1), j:(n-i+1). f(n-i) = f(n)   MinAr(f;j+i;n) = MinAr(f;j;n-i)+i |
| THM | min_ar_sound | f:(), n:, i:(n+1). f(n-MinAr(f;i;n)) = f(n) |
| def | min_arg | MinArg(f : {0..n }) == n-MinAr(f;n;n) |
| THM | min_arg_unique | f:(), n,k:. f(n) = f(k) MinArg(f : {0..n}) = MinArg(f : {0..k})  |
| THM | min_arg_sound | f:(), n:. f(MinArg(f : {0..n})) = f(n) |
| THM | min_arg_iff | f:(), n,k:. f(n) = f(k)  MinArg(f : {0..n}) = MinArg(f : {0..k}) |
| def | min_el | Min{ x | xEn } == MinArg(E(n) : {0..n}) |
| THM | equiv_rel_fun | E:(TT), s,t:T. (EquivRel x,y:T. x E y) (s E t) E(s) = E(t) |
| THM | min_el_unique | E:(), n,k:. (EquivRel x,y:. x E y) (n E k) Min{ x | xEn } = Min{ x | xEk } |
| THM | min_el_sound | E:(), n:. (EquivRel x,y:. x E y) (n E Min{ x | xEn }) |
| THM | min_el_iff | E:(), n,k:. (EquivRel x,y:. x E y) ((n E k) Min{ x | xEn } = Min{ x | xEk }) |
| THM | decide_imp_bool | R:(TTProp). (x,y:T. Dec(x R y)) ( r:(TT). x,y:T. (x r y) (x R y)) |
| THM | comp_choice | E:(Prop).
(EquivRel x,y:. x E y) & (x,y:. Dec(x E y))
(h:(). (n,k:. (n E k) h(n) = h(k)) & (n:. n E (h(n)))) |