// ======== // Show "if two functions f and g are bound then f+g is bound": // ======== // === Types: === TYPE nat // 'real' as a supertype of 'nat': TYPE real (>nat) // type for functions: TYPE natF = nat -> real // === Declarations: === // "is bound": LET B < natF LET abs : real -> real (notation = |_|) LET less < real real (notation = _<_) LET fPlus : natF natF -> natF (prior = 5, notation = _+_) LET nPlus : real real -> real (prior = 5, notation = _+_) // === Axioms: === AX ax1 (VARS x1 e real, x2 e real, y1 e real, y2 e real) FORALL x1 : FORALL x2 : FORALL y1 : FORALL y2 : (x1 x1+x2 x f(n) + g(n) // === Definitions: === // Definition for relation "is bound": RDEF bDef (PARAMS f e natF) (VARS S e real, n e nat) B(f) :<=> EXISTS S : FORALL n : |(f)(n)| < S // === Main goal: === GOAL (VARS f e natF, g e natF) FORALL f : FORALL g : (B(f) & B(g) => B(f+g))