% Adaptive flight control system: Example from my AIAA paper.
% template: -we^2 - b*intwe^2 -c*(L-optL)^2  is a Lyapunov fn.
% When we instantiate a,d,e by 1: we quickly elim all -varaibales
% and slfq simplifies the BIG output formula to
% [ b - 5 > 0 /\ b - 15 < 0 /\ 3200 c + b - 16 < 0 /\ 1200 c - b + 4 < 0 /\ 3200 c - b + 14 > 0 /\ 1200 c + b - 6 > 0 /\ [ b - 10 /= 0 \/ 440000 c^2 + 1800 c - b + 10 /= 0 ] ]
% e.g. b=10, c=1/600 works: slfq timings:
% System time: 57340 milliseconds.
% System time after the initialization: 56850 milliseconds.
% There were 1607 QEPCADB calls!

on echo;
load_package redlog;
rlset r;
load_package qepcad;
on rlqefbqepcad;      % use QEPCAD as the fallback QE
rlqepcadn(100*10^6);  % The number of cells used by QEPCAD. The
		      % default is (only) 1 * 10^6.
rlqepcadl(200*10^3);  % The size of the prime list used by QEPCAD. The
		      % default is (only) 2 * 10^3.
on rlverbose;
on time;
off rlqefb;		% No fallback QE

phi := 
  ((intwe^2 <= 1 and
   (L-optL)^2*beta^2 <= 1  and
   we^2 >= 1) impl
   -2*we*(-5*we -10*intwe + (L-optL)*beta) - 2*b*intwe*we - 2*c*(L-optL)*(-1000*intwe - 2200*we)*beta > 0 );

psi := rlqe( all({intwe, we, L, optL, beta}, phi ) );
%psi := rlgqe( all({intwe, we, L, optL, beta}, phi ) );
%psi1 := second psi;
psi1 := psi;
psi2 := rlqepcad( rlex(psi1), "adaptive.qepcad" );
%psi2 := rlqepcad( psi1 );
%psi3 := rlqepcad( rlex(psi2), "adaptive2.qepcad" );
off nat;	% Output same syntax as input (for reduce)
out "adaptive.out";
psi;
psi2;
shut "adaptive.out";
end;
% suppose a = 1, e = 1, d = 1;
% suppose b = 10
% redlog takes a long time on this one;
% but qepcad immmediately gives
% [ [ 800 c + 1 > 0 /\ 4400 c - 7 <= 0 ] \/ [ 1600 c - 3 < 0 /\ 4400 c - 7 >= 0 ] ]