/*


*/



use(dto).


% f is continuous
0<Eps -> exists(D,all(Z,abs(Z+(-a))=<D =>  abs(f(Z)+ (-f(a)))=<Eps)).

% g is continuous
0<Eps -> exists(D,all(Z,abs(Z+(-a))=<D =>  abs(g(Z)+ (-g(a)))=<Eps)).


% f+g is not continuous
goal ~all(Eps, 0<Eps => exists(D,all(Z,abs(Z+(-a))=<D =>  
                          abs((f(Z)+ (-f(a)))+(g(Z)+ (-g(a))))=<Eps))).

% 8 
abs(X+Y)=<abs(X)+abs(Y).



% min is a concept that is implicit anyway in total orderings
% it will not be used in the proof.
% 9.1 
X<min(X,Y) -> [].

% 9.2
min(X,Y)<X -> Y<X.

% 9.1.1 Z=<min(X,Y) -> Z=<X
% X<Z -> min(X,Y)<Z.

% 10.1.1 Z=<min(X,Y) -> Z=<Y

% Y<Z -> min(X,Y)<Z.

% 10.1
Y<min(X,Y) -> [].

% 10.2
min(X,Y)<Y -> X<Y.


% 10.3 min(X,Y)=<0 -> X=<0, Y=<0.
% 0<X, 0<Y -> 0<min(X,Y).

% 11.3 
X=< half(Z), Y=<half(Z) -> X+Y=<Z.


% 12 
half(X)=<0 -> X=<0.


/*

961023 eagle SICStus 3.0


Proof:
======

   1 : A<A ->                                                           [axiom]
  10 : 0<A -> exists(B,all(C,abs(C+ -(a))=<B=>abs(f(C)+ -(f(a)))=<A))   [axiom]
  11 : 0<A -> exists(B,all(C,abs(C+ -(a))=<B=>abs(g(C)+ -(g(a)))=<A))   [axiom]
  12 + ~all(A,0<A=>exists(B,all(C,abs(C+ -(a))=<B=>abs(f(C)+ -(f(a))+(g(C)+ -(g(a))))=<A))) [axiom]
  13 : abs(A)+abs(B)<abs(A+B) ->                                        [axiom]
  18 : A<B+C -> half(A)<B,half(A)<C                                     [axiom]
  19 : 0<A -> 0<half(A)                                                 [axiom]
  20 : A=<0,exists(B,all(C,abs(C+ -(a))=<B=>abs(f(C)+ -(f(a)))=<A)) [totality resolution from 10]
  21 : A=<0,exists(B,all(C,abs(C+ -(a))=<B=>abs(g(C)+ -(g(a)))=<A)) [totality resolution from 11]
  22 + all(A,0<A=>exists(B,all(C,abs(C+ -(a))=<B=>abs(f(C)+ -(f(a))+(g(C)+ -(g(a))))=<A))) ->  [tableau expansion from 12]
  23 : abs(A+B)=<abs(A)+abs(B)                    [totality resolution from 13]
  28 : A+B=<C,half(C)<A,half(C)<B                 [totality resolution from 18]
  29 : A=<0,0<half(A)                             [totality resolution from 19]
  30 : A=<0,all(B,abs(B+ -(a))=<s$1(A)=>abs(f(B)+ -(f(a)))=<A) [tableau expansion from 20]
  31 : abs(A+ -(a))=<s$1(B) -> B=<0,abs(f(A)+ -(f(a)))=<B [tableau expansion from 30]
  32 : s$1(A)<abs(B+ -(a)),A=<0,abs(f(B)+ -(f(a)))=<A [totality resolution from 31]
  33 : A=<0,all(B,abs(B+ -(a))=<s$2(A)=>abs(g(B)+ -(g(a)))=<A) [tableau expansion from 21]
  34 : abs(A+ -(a))=<s$2(B) -> B=<0,abs(g(A)+ -(g(a)))=<B [tableau expansion from 33]
  35 : s$2(A)<abs(B+ -(a)),A=<0,abs(g(B)+ -(g(a)))=<A [totality resolution from 34]
  36 + 0<s$3=>exists(A,all(B,abs(B+ -(a))=<A=>abs(f(B)+ -(f(a))+(g(B)+ -(g(a))))=<s$3)) ->  [tableau expansion from 22]
  37 + 0<s$3                                        [tableau expansion from 36]
  38 + exists(A,all(B,abs(B+ -(a))=<A=>abs(f(B)+ -(f(a))+(g(B)+ -(g(a))))=<s$3)) ->  [tableau expansion from 36]
  39 + all(A,abs(A+ -(a))=<B=>abs(f(A)+ -(f(a))+(g(A)+ -(g(a))))=<s$3) ->  [tableau expansion from 38]
  40 + abs(s$4(A)+ -(a))=<A=>abs(f(s$4(A))+ -(f(a))+(g(s$4(A))+ -(g(a))))=<s$3 ->  [tableau expansion from 39]
  41 + abs(s$4(A)+ -(a))=<A                         [tableau expansion from 40]
  42 + abs(f(s$4(A))+ -(f(a))+(g(s$4(A))+ -(g(a))))=<s$3 ->  [tableau expansion from 40]
  43 + s$3<abs(f(s$4(A))+ -(f(a))+(g(s$4(A))+ -(g(a)))) [totality resolution from 42]
  52 + s$3<abs(f(s$4(A))+ -(f(a)))+abs(g(s$4(A))+ -(g(a))) [chaining of 23 from 43]
  56 : 0<A,B+A=<C,half(C)<B,C=<0                       [chaining of 28 from 29]
  57 + s$3<A,half(A)<abs(f(s$4(B))+ -(f(a))),half(A)<abs(g(s$4(B))+ -(g(a))) [chaining of 28 from 52]
  78 + s$3<A,half(A)<abs(f(s$4(B))+ -(f(a))),0<abs(g(s$4(B))+ -(g(a))),A=<0 [chaining of 52 from 56]
 229 + s$1(A)<B,abs(f(s$4(B))+ -(f(a)))=<A,A=<0        [chaining of 32 from 41]
 235 + abs(f(s$4(s$1(A)))+ -(f(a)))=<A,A=<0    [ordered resolution of 229 on 1]
 240 + half(A)<B,0<abs(g(s$4(s$1(B)))+ -(g(a))),s$3<A,A=<0,B=<0 [chaining of 78 from 235]
 245 + half(s$3)<A,0<abs(g(s$4(s$1(A)))+ -(g(a))),s$3=<0,A=<0 [ordered resolution of 240 on 1]
 250 + half(s$3)<A,0<abs(g(s$4(s$1(A)))+ -(g(a))),A=<0 [reduction of 245 by [37]]
 271 + s$2(A)<B,abs(g(s$4(B))+ -(g(a)))=<A,A=<0        [chaining of 35 from 41]
 282 + abs(g(s$4(s$2(A)))+ -(g(a)))=<A,A=<0    [ordered resolution of 271 on 1]
 292 + half(A)<B,s$3<A,half(A)<abs(f(s$4(s$2(B)))+ -(f(a))),B=<0 [chaining of 57 from 282]
 301 + half(A)<B,s$1(B)<s$2(C),B=<0,half(A)<C,s$3<A,C=<0 [chaining of 229 from 292]
 304 + half(s$3)<A,s$1(A)<s$2(B),half(s$3)<B,A=<0,B=<0 [ordered resolution of 301 on 1]
 314 + s$1(half(s$3))<s$2(A),half(s$3)<A,half(s$3)=<0,A=<0 [ordered resolution of 304 on 1]
 320 + s$1(half(s$3))<s$2(A),half(s$3)<A,A=<0     [reduction of 314 by [29,37]]
 329 + s$1(half(s$3))<A,abs(g(s$4(A))+ -(g(a)))=<B,B=<0,half(s$3)<B,B=<0 [chaining of 271 from 320]
 333 + s$1(half(s$3))<A,abs(g(s$4(A))+ -(g(a)))=<B,half(s$3)<B,B=<0 [condensement of 329]
 334 + s$1(half(s$3))<A,abs(g(s$4(A))+ -(g(a)))=<0,half(s$3)=<0 [variable elimination from 333]
 335 + s$1(half(s$3))<A,abs(g(s$4(A))+ -(g(a)))=<0 [reduction of 334 by [29,37]]
 347 + half(s$3)<A,A=<0,s$1(half(s$3))<s$1(A)        [chaining of 250 from 335]
 349 + half(s$3)=<0                            [ordered resolution of 347 on 1]
 358 + false                                      [reduction of 349 by [29,37]]


Length = 50, Depth = 22



Total time: 34390 milliseconds

Number of forward inferences: 234
Number of tableau inferences: 8
Number of kept clauses: 144


*/