(* worksheet for cleaning up axioms of CC *)

script "structural";(* declare primitives *)

declareunary "~";  (* negation *)

declareinfix "*";   (* product *)

declareinfix "/";   (* quotient *)

declareunary "%";   (* diagonalization *)

(* universal concept = degree *)

defineconstant "V@?A" "~(%?A)/ ~?A";

(* null concept of a particular degree *)

defineconstant "Null@?A" "~V@?A";

(* degree operation is a retraction *)

axiom "D1" "V@V@?A" "V@?A";

(* degree computation for negation, diagonalization, and product *)

axiom "D2" "V@ ~?A" "V@?A";

axiom "D3" "V@ %?A" "(V@?A) * V@?A";

axiom "D4" "V@?A*?B" "(V@?A)*V@?B";

(* product is associative *)

axiom "D5" "(?A*?B)*?C" "?A*?B*?C";

(* addition of degrees is commutative *)

axiom "D6" "(V@?A)*V@?B" "(V@?B)*V@?A";

axiom "D7" "V@?A/?A" "V@?B/?B";

(* the truth values (objects of degree zero) introduced *)

declareconstant "XX";  (* just an arbitary concept *)

defineconstant "V0" "V@XX/XX";

defineconstant "Null0" "Null@XX/XX";

s "V@?A/?A";
initializecounter();
ri "D7"; ex();
assign "?B_1" "XX";
rri "V0"; ex();
p "V0Def";


(* identity and absorption properties *)

axiom "D8a" "?A*V0" "?A";
axiom "D8b" "V0*?A" "?A";
axiom "D8c" "?A/V0" "?A";

axiom "D9a" "?A*Null0" "Null@?A";
axiom "D9b" "Null0*?A" "Null@?A";

(* axioms of degree subtraction *)

(* this is really old Q5 *)

axiom "D10b" "(?A*?B)/V@?B/?C" "?A*(?B/V@?B/?C)";
axiom "D11a" "((V@?A)*V@?B/?A)/V@?A/?B" "V@?B";
axiom "D11b" "((V@?A)/V@?A/?B)*V@?B/?A" "V@?B";

axiom "D12" "((V@?A)/V@?A/?B)*V@?A/?B" "V@?A";
axiom "D13" "?A/?B*?C" "(?A/?C)/?B";

axiom "D14" "V@?A/?B" "(V@?A)/V@?B";

(* a convenient partial assumption about bad quotients *)

(* it might actually be a theorem, but I don't think so *)

axiom "D15"  "?A/V@?B" "?A/V@?B/?B/?A";


(* restore old D10a for proofs *)

s "(?A*V@?B)/V@?B";
right();rri "D1";ex();right();
rri "D8c"; ex();
top(); ri "D10b"; ex();
ri "EVERYWHERE@D8c"; ex();
ri "EVERYWHERE@ D1"; ex();
ri "RIGHT@($D14)**V0Def"; ex();
ri "D8a"; ex();
p "D10a";

(* restore old form of D10 for old proofs *)

getleftside "D10a";
assign "?A" "V@?A";
ri "D10a"; ex();
p "D10";

s "?A";
ri "D13";
arri "D13";
p "D13x";

s "V@(?A*?C)/?B*?C";
ri "TOPDOWN@D1**D4**D14"; ex();
ri "D13x"; ex();
ri "LEFT@D10"; ex();
rri "D14"; ex();
p "CANCEL";

s "V@(?C*?A)/(?C*?B)";
ri "TOPDOWN@D1**D4**D14"; ex();
ri "RL@D6"; ex();
ri "EVERYWHERE@ ($D4)** $D14"; ex();
ri "CANCEL"; ex();
p "SYMCANCEL";


s "V@?A/?A/?B";
ri "D14"; ex();
initializecounter(); rri "D10a"; ex(); assign "?B_1" "?B/?A";
left(); ri "D11b"; ex();
up(); rri "D14"; ex();
p "MINSYM";

s "V@?A*?B/?A";
ri "D4"; ex();
left(); initializecounter(); rri "D12"; ex();assign "?B_1" "?B";
ri "TOPDOWN@D1**D4**D14"; ex();
ri "EVERYWHERE@ $D14"; ex();
ri "LEFT@D14"; ex();
up(); ri "D5"; ri "RIGHT@D6"; ex();
rri "D5"; ri "LEFT@D11b"; ex();
rri "D4"; ex();
p "MAXSYM";

s "(?A*V@?B)/V@?B/?C";
left();right(); initializecounter(); rri "D11b"; ex();
assign "?A_1" "?C";
up(); rri "D5"; ex();
up(); ri "D10a"; ex();
right(); rri "D14"; ri "MINSYM"; ri "D14"; ex();
p "OLDQ5";

s "V@V0";
right(); rri "V0Def"; ex();
top(); ri "D14"; ri "D1"; ri "V0Def"; ex();
p "VV0";

(* degree computation for Null *)

s "V@Null@?A";
right(); ri "Null"; ex();
top(); ri "D2"; ex();
top(); ri "D1"; ex();
p "NULLDEGREE";

s "V0";
initializecounter();
rri "VV0"; rri "D11a"; ex();
assign "?A_2" "?A";
ri "EVERYWHERE@D8c"; ex();
ri "LEFT@D6";ex();
ri "D10"; ex();
ri "D14"; ex();
ri "LEFT@VV0"; ex();
wb();
p "QUOTOFV0";

(* begin definitions and axioms for boolean operations *)

(* double negation *)

axiom "B1" "~ ~?A" "?A";

(* begin development of definition of intersection *)

(* define degree forcing operation *)
(* the intention is that the degree of ?A^?B will be the lub of 
the degree of ?A and the degree of ?B (in the original interpretation,
simply the maximum *)

defineinfix "DEGFORCE" "?A^?B" "?A*V@?B/?A";

start "V@?A^?B";
ri "RIGHT@DEGFORCE";ex();
ri "D4"; ri "RIGHT@D1"; rri "D4"; ex();
ri "MAXSYM";ex();
ri "D4"; ri "RIGHT@ $D1"; rri "D4";
ri "RIGHT@ $DEGFORCE"; ex();
p "DEGFORCESYM";


(* we now define intersection *)

defineinfix "AND" "?A&?B" "(%?A^?B)/?B^?A";

defineinfix "B2" "?A|?B" "~(~?A)& ~?B";

(* degree of forcing expressions *)

s "V@?A^?B";
right();ri "DEGFORCE"; ex();
up();ri "D4"; ex();
right(); ri "D1"; ex();
up(); rri "D4"; ex();
p "FORCEDEGREE";

s "?A^?A";
ri "DEGFORCE"; ex();
right(); ri "V0Def"; ex();
up(); ri "D8a"; ex();
p "SELFFORCE";

s "?A^?A/?B";
ri "DEGFORCE"; ex();
right(); ri "TOPDOWN@D14"; rri "D13"; ex();
right(); ri "D6"; ex();
up(); ri "D13"; ex();
left(); rri "D14"; ri "V0Def"; ex();
up(); ri "QUOTOFV0"; ex();
up(); ri "D8a"; ex();
p "SMALLERFORCE";

(* this whole group of lemmas is much easier to prove with consistent use
of B8! *)

s "?A^V@?B";
ri "DEGFORCE"; ex();
right();ri "D14**(LEFT@D1)** $D14"; ex();
top(); rri "DEGFORCE"; ex();
p "FORCEV";

s "(?A^?B)^?B";
ri "EVERYWHERE@DEGFORCE"; ex();
ri "TOPDOWN@D4**D14**D1"; ex();
ri "TOPDOWN@D4**D14**D1"; ex();
ri "D5"; ex();
right();right();right();
ri "RIGHT@ $D14"; ri "D6"; ex();
up(); ri "D13"; ex();
ri "(LEFT@ $D14)** $D14"; ri "V0Def"; ex();
up(); ri "D8a"; ex();
up(); ri "RIGHT@ $D14"; rri "DEGFORCE"; ex();
p "FORCERETRACT";

s "V@?A^?B^?C";
ri "DEGFORCESYM"; ri "FORCEDEGREE"; ex();
ri "D4"; ex();
right(); ri "D14"; ex();
top(); ri "EVERYWHERE@FORCEDEGREE"; ex();
ri "TOPDOWN@D4**D14**D1"; ex();
right();right(); ri "RIGHT@ $D14"; ri "D6"; ex();
up(); ri "D13"; ex();
up(); ri "EVERYWHERE@ $D14"; ri "D5"; ex();
right(); rri "D4"; ex(); saveenv "Lemma6"; 
rri "FORCEDEGREE"; ri "DEGFORCESYM"; ri "FORCEDEGREE"; ex();
top(); applyconvenv "Lemma6";
saveenv "Lemma7";
ri "FORCEDEGREE"; ex();
ri "D4**(RIGHT@D14)**EVERYWHERE@DEGFORCESYM"; ex();
ri "(RIGHT@ $D14)** $D4"; rri "FORCEDEGREE"; ex();
applyenv "Lemma7";
p "DEGFORCESWAP";

s "(V@?A)^?B";
ri "DEGFORCE"; ex();
right();ri "D14"; ri "RIGHT@D1"; rri "D14"; ex();
up(); rri "D4"; ex();
rri "FORCEDEGREE"; ex();
p "VFORCE";


s "?A^?B^?A";
ri "EVERYWHERE@DEGFORCE"; ex();
right();ri "TOPDOWN@D4**D14**D1"; ex();
left(); right(); ri "D14"; ri "RIGHT@ $D1"; rri "D14"; ex();
up(); rri "DEGFORCE"; ri "VFORCE"; ri "DEGFORCESYM"; 
rri "VFORCE"; ri "DEGFORCE"; ri "D6"; ex();
up(); ri "D10"; ri "D14"; ri "RIGHT@D1"; rri "D14"; ex();
up(); rri "DEGFORCE"; ex();
p "CANCELFORCE";


(* degree of intersections *)

s "V@?A&?B";
right(); ri "AND"; ex();
up(); ri "D14"; ex();
left(); ri "D3"; ex();
top(); right(); ri "DEGFORCESYM"; ex();
top(); ri "D10"; ex();
p "ANDDEGREE";

s "V@(V@?A)&(V@?B)";
ri "ANDDEGREE"; ex();
ri "FORCEDEGREE"; ex();
ri "TOPDOWN@D4**D14**D1"; ex();
ri "EVERYWHERE@($D4)**($D14)";
rri "FORCEDEGREE";
rri "ANDDEGREE"; ex();
p "ANDDEGV";

(* original B3 is our Null *)

(* also seems out of place in original *)

(* are some of these axioms redundant? *)

(* Yes -- associativity and idempotence should be theorems *)

axiom "B4" "?P&?Q" "?Q&?P";

axiom "B5" "(?P&?Q)&?R" "?P&?Q&?R";  (* redundant *)

axiom "B6" "?P&?Q|?R" "(?P&?Q)|(?P&?R)";

axiom "B7" "?P&Null@?Q" "Null@?P^?Q";  (* might be redundant *)

axiom "B8" "?P&V@?Q" "?P^?Q";

axiom "B9" "?P& ~?P" "Null@?P";

axiom "B10" "?P&?P" "?P";  (* redundant *)

(* do we want to switch to a set like the one in cylinders.mk2? *)

(* No, but we already have such a system, with duality handled by
double negation and the de Morgan law defining union *)

(* a theorem about degree computations proved with help of B8 *)

s "(?A^?B)^?C";
ri "EVERYWHERE@ $B8"; ex();
ri "B5"; ex();
right(); ri "B8"; ri "VFORCE"; ex();
up(); ri "B8"; ri "FORCEV"; ex();
p "FORCEASSOC";


(* axioms of padding *)

axiom "PAD1" "~(V@?A)*?B*(V@?C)" "(V@?A)*(~?B)*(V@?C)";

(* do we actually need to pad on both sides? YES! *)

axiom "PAD2" "(V@?A)*(?B&?C)*V@?D" "((V@?A)*(?B^?C)*V@?D)&(V@?A)*(?C^?B)*V@?D";

(* padding on the right is redundant, strictly speaking; PAD2a
could as well be the axiom *)

axiom "PAD3" "?A*?B" "((V@?A)*?B)&?A*V@?B";


s "?A*V@?B";
right(); initializecounter(); rri "D10"; ex(); assign "?B_1" "?A";
ri "EVERYWHERE@($D4)**($D14)"; ex();
top(); rri "DEGFORCE"; ex();
p "PADTOFORCE";


s "(?A&?B)^?C";
rri "B8"; ex();
right(); rri "B10"; ex();
up(); ri "B5"; ri "RIGHT@B4**B5**RIGHT@B4**B8"; ex();
top(); rri "B5"; ri "LEFT@B8"; ex();
p "FORCEANDDIST";


s "(?A&?B)&?C";
right(); rri "B10"; ex();
up(); rri "B5"; ri "B4"; ex();
right(); ri "B5"; ex();
up(); rri "B5"; ex();
left(); ri "B4"; ex();
p "ANDSELFDIST";

s "?A&?B";
ri "AND"; ex();
left();right(); 
ri "($SELFFORCE)**($FORCEV)**(RIGHT@DEGFORCESYM)**FORCEV";ex();
top(); right();
ri "($SELFFORCE)**($FORCEV)**(RIGHT@DEGFORCESYM)**FORCEV";ex();
top(); rri "AND"; ex();
p "ANDFORCE";

(* one case of one-sided padding *)

s "(V@?A)*?B&?C";
right();rri "D8a"; ri "RIGHT@ $VV0"; ex();
top(); ri "PAD2"; ex();
ri "RL@(RIGHT@RIGHT@VV0)**RIGHT@D8a"; ex();
ri "EVERYWHERE@DEGFORCE"; ex();
initializecounter(); ri "EVERYWHERE@ $SYMCANCEL"; ex();
assign "?C_28,?C_56" "(V@?A),V@?A";
ri "RL@ $D5"; ex();
ri "EVERYWHERE@ $DEGFORCE"; rri "ANDFORCE"; ex();
p "PAD2a";

s "?A&(?B^?A)";
ri "ANDFORCE"; ex();
ri "(LEFT@CANCELFORCE)**(RIGHT@FORCERETRACT)"; ex();
rri "ANDFORCE"; ex();
wb();
p "ANDONEFORCE";

s "(~?A)^?B";
ri "DEGFORCE"; rri "D8b"; ri "LEFT@ $VV0"; rri "PAD1"; ex();
right(); ri "(LEFT@VV0)**D8b"; ex();
right(); ri "D14"; ri "RIGHT@D2"; rri "D14"; ex();
up(); rri "DEGFORCE"; ex();
p "NOTFORCE";

s "?A|?B";
ri "B2"; ex();
right(); ri "ANDFORCE"; ex();
ri "EVERYWHERE@ $FORCEV"; ex();
ri "EVERYWHERE@D2"; ri "EVERYWHERE@FORCEV"; ri "EVERYWHERE@NOTFORCE"; ex();
up(); rri "B2"; ex();
p "ORFORCE";

s "V@?A|?B";
right(); ri "B2"; ex();
up(); ri "D2"; ex();
ri "ANDDEGREE"; ex();
rri "VFORCE"; rri "FORCEV"; ri "EVERYWHERE@D2"; ex();
ri "FORCEV"; ri "VFORCE"; ex();
p "ORDEGREE";

s "(?A^?B) = ?A&?B";
ri "PCASEINTRO@(?B^?A)=?A|?B"; ex();
right();left();right(); ri "ANDFORCE"; ex();
right(); ri "0|-|1"; ex();
up(); ri "B6"; ex();
left();left();rri "B8"; ex();
up();ri "B4** ($B5) ** LEFT@B10"; ex();
right(); rri "B10"; ex(); up(); rri "B5"; ri "LEFT@B8"; ex();
up(); rri "B6"; ex();
right(); ri "B2"; ex();
right();left();rri "Null";rri "B9"; ex();
up();ri "B5**(RIGHT@B10)**B9**Null"; ex();
up();ri "B1"; ex();
up(); ri "B8"; ri "FORCERETRACT"; ex();
up(); ri "REFLEX"; ex();
up(); right();ri "EQUATION"; ex();
right();left();
rri "(2|-|1)@false"; ex();
left();right();
ri "ORFORCE"; ex();
left(); ri "0|-|2"; ex();
ri "RL@ $B1"; ex();
up(); ri "B2"; ex();
right(); ri "B4"; ex();
right(); rri "B2"; ex();
up(); ri "B6"; ex();
right(); ri "B4"; ex();
right(); rri "NOTFORCE"; rri "B8"; ex();
up(); rri "B5"; ri "LEFT@B10"; 
ri "B8"; rri "FORCERETRACT"; rri "B8"; ri "LEFT@NOTFORCE"; ex();
up(); rri "B6"; ex();
right(); ri "B2"; ex();
ri "EVERYWHERE@B1"; ex();
right(); right(); rri "Null"; rri "B9"; ex();
up(); rri "B5"; ri "LEFT@B10"; ri "B9"; ri "Null"; ex();
up(); ri "B1"; ex();
up(); ri "B8"; ri "(LEFT@ $NOTFORCE)**FORCERETRACT**NOTFORCE"; ex();
up(); ri "B1"; ex();
up(); ri "REFLEX"; ex();
up(); ex();
up(); up(); rri "CASEINTRO"; ex();
up(); up(); rri "EQUATION"; ex();
p "IMPLICATIONS";

s "?A|Null@?B";
ri "B2"; ex();
right();right(); ri "(RIGHT@Null)**B1"; ex();
up(); ri "B8"; ri "NOTFORCE"; ex();
up(); ri "B1"; ex();
p "B8d";

s "?A|V@?B";
ri "B2"; ex();
right();right(); rri "Null"; ex();
up(); ri "B7"; ex();
ri "RIGHT@NOTFORCE"; ri "Null"; ri "RIGHT@D2"; rri "Null"; ex();
p "B7d";

s "?A|?A";
ri "B2"; ex();
right(); ri "B10"; ex();
up(); rri "B2"; ri "B1"; ex();
p "B10d";

s "?A|?B";
ri "B2"; ex();
right(); ri "B4"; ex();
up(); rri "B2"; ex();
p "B4d";

s "?A|?B&?C";
ri "B2"; ex();
right();right();right(); ri "RL@ $B1"; ex();
up(); rri "B2"; ex();
top(); right();
ri "B6"; ri "B2"; ri "RIGHT@RL@ $B2"; ex();
up(); ri "B1"; ex();
p "B6d";

s "?A|?A&?B";
ri "B6d"; ex();
left(); ri "B10d";rri "SELFFORCE"; rri "B8d"; ex();
up(); rri "B6d"; ex();
right(); ri "B4"; ri "B7"; ex();
up(); ri "B8d"; ex();
ri "CANCELFORCE"; ex();
p "ABSORB";

s "?A&?A|?B";
ri "B6"; ex();
left(); ri "B10";rri "SELFFORCE"; rri "B8"; ex();
up(); rri "B6"; ex();
right(); ri "B4d"; ri "B7d"; ex();
ri "(RIGHT@Null)**B1"; ex();
up(); ri "B8"; ex();
ri "CANCELFORCE"; ex();
p "ABSORBd";

s "(?A&?B)*V@?C";
ri "PADTOFORCE"; ex();
ri "LEFT@ANDFORCE"; ex();
rri "B8"; ex();
ri "ANDSELFDIST"; ex();
ri "EVERYWHERE@D4"; ex();
ri "EVERYWHERE@ANDDEGREE"; ex();
drrs "ANDDEGREE"; ri "DEGFORCESYM"; ex();
top(); ri "EVERYWHERE@ $D4";
ri "EVERYWHERE@B8";
ri "EVERYWHERE@ $PADTOFORCE"; ex();
p "PAD2b";  (* notice that this does not depend on PAD2! *)

s "?P| ~?P"; 
ri "B2"; ex();
right(); ri "B4"; ri "LEFT@B1"; ri "B9"; ex();
ri "Null"; ex();
up(); ri "B1"; ex();
p "B9d";

s "(?A&?B)|(?A& ~?B)";
rri "B6"; ex();
ri "RIGHT@B9d"; ex();
ri "B8"; ex();
p "CASES";

(* axioms of quantification *)

(* Q1 reduces good quotients to conjunction and quantification *)

axiom "Q1" "(?A^?B)/?B" "(?A&((V@(?A/?B))*?B))/V@?B";

axiom "Q2" "?A" "?A&?A/V@?B";

axiom "Q3" "(?A|?B)/V@?C"
"((?A^?B)/V@?C)|(?B^?A)/V@?C";

(* stuff to verify to see that we have a quantifier algebra *)

s "Null@V@?A";
ri "Null"; ri "RIGHT@D1"; rri "Null"; ex();
p "NULLV";

s "(Null@?A)/V@?A/?B";
left(); rri "NULLV"; rri "D9b"; ex();
top(); ri "OLDQ5"; ex();
ri "RIGHT@ $D14"; ri "D9b"; ri "NULLV"; ex();
p "QTEST1";

s "((?A/V@?A/?B)*(V@?A/?B))/V@?A/?B";
ri "EVERYWHERE@D10a"; ex();
p "QTEST4";

s "(~((?A/V@?A/?B)*V@?A/?B))/V@?A/?B";
left(); ri "RIGHT@ ($D8b)** LEFT@ $VV0"; ex();
ri "PAD1"; ex();
ri "(LEFT@VV0)**D8b"; ex();
up(); ri "D10a"; ex();
p "QTEST5";

(* a theorem QTEST6 = old PREC3 would be nice *)

(* the other quantifier algebra axioms are obvious *)

(* what remains to be done is a systematic handling of substitution
(and equality proper) *)

(* the definition of mindeg and results about it, taken from the old file *)

defineconstant "mindeg@?A,?B" "V@?A/?A/?B";

(* some theorems about mindeg are presumably needed *)

s "V@?B";
rri "D8c"; ex();
initializecounter();
right(); rri "V0Def"; ex();
assign "?A_1" "V@?B";
up(); left(); rri "D1"; ex();
up(); rri "D14"; rri "mindeg"; ex();
p "SELFMIN";

s "mindeg@?A,?B";
ri "mindeg"; ex();
initializecounter();
rri "D10"; ex();
assign "?B_1" "?B/?A";
left();left(); ri "D14"; ex();
up(); ri "D11b"; ex();
top(); rri "D14"; rri "mindeg"; ex();
p "MINDEGSYM";

s "mindeg@?A,?A^?B";
ri "mindeg"; ex();
ri "TOPDOWN@D4**D14"; ex();
right();right(); ri "FORCEDEGREE"; ri "D4"; ri "D6"; ex();
up(); ri "D13"; ex();
left(); rri "D14"; ri "V0Def"; ex();
up(); ri "QUOTOFV0"; ex();
up(); ri "D8c"; ex();
p "MINWITHFORCE";

s "mindeg@?A,?B";
ri "mindeg"; 
ri "TOPDOWN@D14";
ri "EVERYWHERE@ $D1"; 
ri "EVERYWHERE@ $D14";
rri "mindeg"; ex();
p "MINDEGV";

s "mindeg@(?A^?B),?B";
ri "MINDEGSYM"; ri "MINDEGV"; ri "EVERYWHERE@DEGFORCESYM"; ri "$MINDEGV";
ri "MINWITHFORCE"; ex();
p "MINWITHFORCE2";

s "mindeg@?A,?A/?B";
ri "mindeg"; ex();
initializecounter();
rri "D10"; ex();
assign "?B_1" "?A/?A/?B";
left();left(); ri "D14"; ex();
up(); ri "D12"; ex();
up(); right();
initializecounter();
rri "D10"; ex();
assign "?B_1" "?A/?B";
left();left(); ri "D14"; ex();
up(); ri "D12"; ex();
up(); up();left();
initializecounter(); rri "D12"; ex();
assign "?B_1" "?B"; ri "LEFT@ $D14"; ri "D6"; ex();
up(); ri "RIGHT@ $D14"; ri "D10"; ex();
p "MINWITHQUOT";

s "(Null@?A*?B)/V@?B";
left(); ri "Null"; ex();
right(); rri "D1"; ex();
up(); rri "Null"; rri "D9b"; ex();
right(); ri "D4"; ex();
up(); rri "D5"; ex();
left(); ri "D9b"; ex();
top(); ri "D10a"; ri "NULLV"; ex();
p "NULLQUOT";


s "V@(?A/?B)/?A";
ri "TOPDOWN@D14"; ex();
ri "D13x"; ex();
ri "RIGHT@D6"; ri "D13x"; ex();
left(); ri "($D14)**V0Def"; ex();
up(); ri "QUOTOFV0"; ex();
p "BADQUOT";

s "V@?A/?A/?A/?B";
ri "MINSYM"; ex();
ri "D14";ri "LEFT@D14";ri "D13x"; ex();
dlls "BADQUOT"; ri "BADQUOT"; ex();
top(); ri "EVERYWHERE@D8b"; rri "D14"; ex();
p "MINUSMIN";


s "?A|?A/V@?B";
left();initializecounter();ri "Q2"; ex();
assign "?B_1" "?B";
up(); ri "B4d"; ri "RIGHT@B4"; ri "ABSORB"; ex();
p "Q2d";

s "?A|?A/V@?B";
left();initializecounter();ri "Q2"; ex();
assign "?B_1" "?B";
up(); ri "B4d"; ri "RIGHT@B4"; ri "ABSORB"; ex();
ri "DEGFORCE"; ex();
ri "TOPDOWN@D1**D14"; ri "EVERYWHERE@ $D14"; ex();
p "Q2d2"; 

s "?A";
initializecounter(); rri "D10a"; ex();
assign "?B_1" "?B/?A";
ri "LEFT@ $DEGFORCE"; ex();
p "INSERTFORCE@?B";


s "V@((?A^?B)&(?B^?A)/V@?C)";
ri "ANDDEGREE**($VFORCE)**($FORCEV)"; ex();
ri "RIGHT@D14**(LEFT@DEGFORCESYM)"; ex();
ri "SMALLERFORCE"; ex();
saveenv "LemmaA";

s "V@(((?B ^ ?A) / V @ ?C) * V @ ?C / ?C / ?A ^ ?B)";
ri "D4"; ri "D6"; ex();
left(); ri "D1"; ri "D14"; ex();
up(); right(); ri "D14**(LEFT@DEGFORCESYM)**(RIGHT@D1)** $D14"; ex();
up(); ri "D11b"; ex();
saveenv "LemmaD";



s "(?B ^ ?A) / V @ ?C";
initializecounter();rri "D10a"; ex();
assign "?B_1" "?C/?C/?A^?B";
right(); ri "TOPDOWN@D14"; ex();
right();right(); applyconvenv "LemmaD";
assign "?C_29" "?C";
up(); up(); ri "EVERYWHERE@ $D14"; ex();
up(); rri "D15"; ex();
p "SOMESOME";

s "((?A^?B)/V@?C)&(?A&?B)/V@?C";
left();left();rri "ABSORB"; ex();
upto "?x/?y"; ri "Q3"; ex();
up(); ri "B4"; ri "RIGHT@B4d"; ex();
right();left();left(); ri "LEFT@($SELFFORCE)**($FORCEV)";
ri "FORCEASSOC"; ex();
right(); ri "LEFT@ANDDEGREE"; ri "VFORCE"; ex();
right(); ri "FORCEASSOC**CANCELFORCE"; ex();
up(); rri "ANDDEGREE"; ex();
up(); ri "FORCEV**SELFFORCE"; ex();
top(); ri "ABSORBd"; ex();
rri "FORCEV"; ex();
right(); ri "D14"; ex();
left(); right(); ri "RIGHT@B4"; rri "FORCEV"; ri "RIGHT@ANDDEGREE"; 
ri "FORCEV"; ri "CANCELFORCE"; ex(); 
up(); rri "ANDDEGREE"; ex();
up(); rri "D14"; ex();
up(); ri "FORCEV**SELFFORCE"; ex();
wb();
p "TAKESOMEOUT";

s "((?A^?B)&(?B^?A)/V@?C)/V@?C";
ri "TAKESOMEOUT"; ex();
right(); ri "LEFT@B4"; ri "TAKESOMEOUT"; ex();
top(); rri "B5"; ri "B4"; ex();
right();left();left(); rri "FORCEV"; ex();
right(); ri "D14"; ex();
left(); ri "DEGFORCESYM"; ex();
up(); rri "D14"; ex();
up(); ri "FORCEV**SMALLERFORCE"; ex();
up();up();right();left(); ri "DEGFORCE"; ex();
right(); ri "TOPDOWN@D1**D14"; ex();
ri "RIGHT@LEFT@DEGFORCESYM"; ex();
ri "EVERYWHERE@ $D14"; ex();
ri "MINSYM"; ex();
uptors "SOMESOME"; rri "SOMESOME"; ex();
top(); ri "LEFT@LEFT@B4"; ex();
p "QTEST6a";

s "((?A^?B)/V@?C)&(?B^?A)/V@?C";
initializecounter(); rri "D10a"; ex();
assign "?B_1" "?C/?C/?A^?B";
left();left();right(); ri "SOMESOME"; ex();
up();up();rri "B8"; ri "PAD2b"; ex();

s "((?A^?B)&(?B^?A)/V@?C)/V@?C";
left(); ri "ANDONEFORCE"; ex();
right(); ri "DEGFORCE"; ex();
right(); ri "TOPDOWN@D1**D14"; ex();
ri "RIGHT@LEFT@DEGFORCESYM"; ri "EVERYWHERE@ $D14"; ri "MINSYM"; ex();
upto "?x&?y"; ri "B4"; ex();
saveenv "Temp";
up(); ri "TAKESOMEOUT"; ex();
right(); applyconvenv "Temp";
up(); left(); left(); rri "FORCEV";ex();
right(); initializecounter(); applyconvenv "LemmaD";
assign "?C_1" "?C";
up(); ri "FORCEV**SELFFORCE"; ex();
uptors "SOMESOME"; rri "SOMESOME"; ex();
p "EXTRACTLEMMA";

s "((?A^?B)/V@?C)&(?B^?A)/V@?C";
left();left();initializecounter();
rri "SMALLERFORCE"; rri "FORCEV";ex();
assign "?B_1" "V@?C";
right(); ri "D14";
ri "LEFT@DEGFORCESYM"; rri "D14"; ex();
up(); ri "FORCEV"; rri "CASES"; ex();
up(); ri "Q3"; ex();
up(); ri "B4"; ri "B6"; ex();
left();right();left(); rri "FORCEV"; ex();
right(); ri "ANDDEGREE"; ex();
right(); rri "FORCEV"; ri "RIGHT@D2"; ri "FORCEV"; ex();
up(); rri "ANDDEGREE"; ex();
up(); ri "FORCEV**SELFFORCE"; ex();
up();up(); rri "EXTRACTLEMMA"; ex();
saveenv "MainProof";
upto "?x|?y";right();right();left(); rri "FORCEV"; ex();
right(); ri "ANDDEGREE"; ex();
right(); rri "FORCEV"; ri "RIGHT@ $D2"; ri "FORCEV"; ex();
up(); rri "ANDDEGREE"; ex();
up(); ri "FORCEV**SELFFORCE"; ex();
ri "B4"; ex();
up(); ri "TAKESOMEOUT"; ex();
left(); left(); ri "DEGFORCE"; ex();
right();ri "TOPDOWN@D1**D2**D14"; ex();
ri "RIGHT@LEFT@DEGFORCESYM"; ex();
ri "EVERYWHERE@ $D14"; ri "MINSYM"; ex();
up();up(); ri "D15"; ex();
right(); ri "TOPDOWN@D2**D4**D14"; ex();
right(); right(); ri "EVERYWHERE@($D4)**($D14)"; ex();
applyenv "LemmaD";
up(); up(); ri "EVERYWHERE@ $D14"; ex();
uptols "D10a"; ri "D10a"; ex();
up();up(); rri "B5"; ri "LEFT@B9"; ri "B4"; ri "B7"; ex();
up(); ri "B8d"; ex();
rri "FORCEV"; ex();
right(); ri "($VFORCE)**($FORCEV)"; ex();
left();ri "D14"; ex();
left();ri "ANDDEGREE** $VFORCE"; ex();
left();ri "D2"; ex();
up(); ri "VFORCE** $ANDDEGREE"; ri "RIGHT@B4"; ex();
up(); rri "D14"; ex();
up(); right();
ri "D14**(LEFT@DEGFORCESYM)** $D14"; ex();
ri "D14"; ex();
initializecounter();
left(); applyconvenv "LemmaA";
assign "?C_1" "?C";
up(); rri "D14"; ex();
up(); ri "SELFFORCE"; ex();
up(); ri "FORCEV**SELFFORCE"; ex();
p "QTEST6";

(* this definition will certainly appear *)

defineconstant "Eq@?A,?B,?C" "(V@?A)*(%V@?B*?C)/V@?C";

(* degree computation for Eq *)

s "V@Eq@?A,?B,?C";
right(); ri "Eq"; 
up(); ri "D4"; ex();
left(); ri "D1"; ex();
up(); right(); ri "D14"; ex();
right(); ri "D1"; ex();
up(); left(); ri "D3"; ex();
right(); ri "D1"; ri "D4"; ex();
up(); left(); ri "D1"; ri "D4"; ex();
up(); rri "D5"; ex();
left();left();rri "D4"; ex();
up(); rri "D4"; ex();
up();up(); ri "D10"; ex();
up(); rri "D4"; ex();
right(); right(); ri "D5"; ex();
p "EQDEGREE";

s "Eq@(V@?A),(V@?B),V@?C";
ri "Eq"; ex();
ri "EVERYWHERE@($D4)**($D14)"; ex();
ri "EVERYWHERE@D1"; ex();
rri "Eq"; ex();
p "EQV";

s "V@(%V@?B*?C)/?B*?C*?B";
ri "TOPDOWN@D1**D3**D4**D14"; ex();
left(); ri "RL@D6"; ri "D5"; ri "RIGHT@EVERYWHERE@($D4)"; ex();
up(); ri "RIGHT@EVERYWHERE@($D4)"; ri "D10"; ex();
saveenv "Lemma";

s "Eq@?A,?B,?C";
ri "Eq"; ex();
right(); right(); initializecounter(); applyconvenv "Lemma";
assign "?B_1" "?B";
top(); rri "D10b"; ex();
right(); applyenv "Lemma";
p "EQALTDEF";

dropenv "Lemma";

s "(Eq@?A,?B,?C)/V@?B/?D";
ri "LEFT@EQALTDEF"; ri "D13x"; ex();
left();right();right();ri "D4"; ex();
left(); initializecounter(); rri "D12"; ex();
assign "?B_1" "?D";
up(); ri "EVERYWHERE@ ($D4)**($D14)"; ri "RIGHT@D5"; ex();
top(); ri "RIGHT@ $D4"; rri "EQALTDEF"; ex();
p "EQSLASH";



(* subcases of definition *)

s "Eq@V0,?A,V0";
ri "Eq"; ri "EVERYWHERE@VV0**D8c**D8b**D8a"; ex();
p "Eq1";

s "Eq@V0,?A,?B";
ri "Eq"; ri "EVERYWHERE@VV0**D8c**D8b**D8a"; ex();
p "Eq2";

s "Eq@?A,?B,V0";
ri "Eq"; ri "EVERYWHERE@VV0**D8c**D8b**D8a"; ex();
p "Eq3";

s "Eq@?A,V0,?B";
ri "Eq";ri "EVERYWHERE@VV0**D8c**D8b**D8a"; ex();
right();downtoleft "V@?B";rri "SELFFORCE"; ex();
top(); downtoright "V@?B";rri "SELFFORCE"; ex();
uptors "AND"; rri "AND"; ri "B10"; ex();
p "Eq4";


(* separation of equality (on a universe) from the content *)

axiom "E1a" "%?A" "(%V@?A)&?A*V@?A";
axiom "E1b" "%?A" "(%V@?A)&(V@?A)*?A";

s "?A& %V@?A";
ri "B4"; ex();
ri "ANDONEFORCE"; ex();
right(); ri "DEGFORCE"; ex();
ri "TOPDOWN@D1**D3**D14"; ri "RIGHT@D10a"; ex();
top(); rri "E1a"; ex();
ri "E1b"; ex();
ri "B4"; ex();
p "EQMOVE1";

s "(% V @ (?B ^ ?C) * ?D)^?C^?B";
rri "FORCEV"; ex();
right(); ri "DEGFORCESYM"; ex();
initializecounter(); rri "D10a"; ex();
assign "?B_1" "(?D*(?B^?C)*?D)";
left(); ri "TOPDOWN@D1**D4**D14"; ex();
rri "D5"; ri "RL@($D4)**($D1)"; rri "D3"; ex();
up();rri "D14"; ex();
up();ri "FORCEV**SMALLERFORCE"; ex();
saveenv "LemmaF";

s "(?C ^ ?B) ^ (% V @ (?B ^ ?C) * ?D) / V @ ?D";
initializecounter(); rri "D10a"; ex();
assign "?B_1" "?D";
left();left();right();rri "Eq2"; ex();
up(); rri "FORCEV"; ri "RIGHT@EQDEGREE"; ex();
ri "FORCEV"; ri "DEGFORCE"; ex();
up(); ri "D5"; ex();
right(); ri "D6"; ex();
ri "EVERYWHERE@D8b"; ri "TOPDOWN@D1**D4**D14"; ex();
ri "RIGHT@RIGHT@DEGFORCESYM"; ex();
right(); ri "(LEFT@ $D5)**D10a"; ex();
up(); initializecounter(); rri "D10a"; ex(); assign "?B_1" "?B^?C";
ri "RIGHT@DEGFORCESYM"; ex();
left(); ri "D5"; ri "RIGHT@D5"; ex();
rri "D5"; ri "RL@D6**($D4)**($D1)"; rri "D3"; ex();
up(); rri "D14";ex();
up(); rri "DEGFORCE"; ex();
saveenv "LemmaG";


s "(% V @ (?B ^ ?C) * ?D) & (?C ^ ?B)*V@?D ";
ri "ANDONEFORCE"; ex();
right(); ri "DEGFORCE"; ex();
right(); ri "TOPDOWN@D1**D3**D4**D14"; ri "LEFT@ $D5"; 
ri "EVERYWHERE@ ($D4)**($D14)"; 
ri "CANCEL"; ex();
ri "D14**(RIGHT@DEGFORCESYM)**(LEFT@D4)**D10a"; ex();
up();ri "D5"; ex();
right(); initializecounter(); rri "D10a"; ex(); assign "?B_1" "?B^?C";
left(); ri "EVERYWHERE@D4"; ri "D5"; ri "RIGHT@D5"; ex();
rri "D5"; ri "RL@D6**($D4)**($D1)"; rri "D3"; ex();
up(); ri "RIGHT@DEGFORCESYM"; rri "D14"; ex();
up(); rri "DEGFORCE"; ex();
up(); rri "ANDONEFORCE"; ex();
saveenv "LemmaH";

s "V@(((V @ (?C ^ ?B) * V @ ?D) * ?C ^ ?B) * V @ ?D)";
 ri "TOPDOWN@D1**D4**D14"; ex();
ri "D5"; ex();
ri "RL@(RIGHT@ $D1)**($D4)**($D1)"; rri "D3"; ex();
saveenv "LemmaI";


s "(% V @ (?C ^ ?B) * V @ ?D) & ((((V @ (?C ^ ?B) * V @ ?D) * ?C ^ ?B) * V @ ?D) / V @ ?D)";
ri "ANDONEFORCE"; ex();
right(); ri "DEGFORCE"; ex();
right(); ri "RIGHT@RIGHT@D10a"; ex();
ri "D14"; ex();
left(); applyconvenv "LemmaI"; ex();
up(); ri "TOPDOWN@D1**D4**D14"; ri "EVERYWHERE@D1"; ex();
left();ri "LEFT@EVERYWHERE@($D4)**($D14)"; ri "D6"; ex();
up(); ri "RIGHT@EVERYWHERE@($D4)**($D14)"; ri "D10a"; ex();
saveenv  "LemmaJ";



(* setup for more general movement theorem *)

s "(Eq@?A,(?B^?C),?D)&(V@?A)*?C^?B";
ri "LEFT@Eq"; rri "PAD2a"; ex();
right(); ri "ANDONEFORCE"; ex();
right(); applyenv "LemmaG";
up();left();left(); applyconvenv "LemmaF";
uptols "QTEST6"; ri "QTEST6"; ex();
saveenv "MainProof";
dlrs "}LemmaG"; applyconvenv "LemmaG";
up();left(); applyenv "LemmaF";
up(); ri "ANDONEFORCE"; ex();
right(); ri "FORCEASSOC** $FORCEV"; ex();
right(); ri "DEGFORCESYM"; ri "RIGHT@SMALLERFORCE"; ex();
up(); ri "FORCEV"; ex();
up(); rri "ANDONEFORCE"; ex();
applyconvenv "LemmaH";
left(); right(); ri "D4"; ri "(LEFT@DEGFORCESYM)**(RIGHT@ $D1)"; 
rri "D4"; ex();
upto "?x&?y"; ri "B4"; ri "EQMOVE1"; ex();
saveenv "MainProof";
left(); rri "D5"; ex();
left(); initializecounter(); rri "D10a"; ex();
assign "?B_1" "?D";
upto "?x&?y"; ri "B4"; ex();
applyconvenv "LemmaJ";
left(); ri "($SELFFORCE)** $FORCEV"; ex();
right(); applyconvenv "LemmaI";
up(); ri "FORCEV"; ex();
up();right();left();
ri "($SELFFORCE)**($FORCEV)"; ex();
right(); applyenv "LemmaI";
up(); ri "FORCEV"; ex();
uptors "QTEST6"; rri "QTEST6"; ex();
left();left();rri "FORCEV"; ex();
right(); applyenv "LemmaI";
up(); ri "FORCEV**SELFFORCE"; ex();
top();right();right();left();rri "FORCEV"; ex();
right();applyconvenv "LemmaI";
up();ri "FORCEV**SELFFORCE"; ex();
up(); ri "D10a"; ex();
top(); ri "TOPDOWN@D1**D4**D14"; ri "EVERYWHERE@DEGFORCESYM"; ex();
ri "EVERYWHERE@($D4)**($D14)"; ex();
ri "PAD2a"; ex();
ri "LEFT@ $Eq"; ex();
right(); rri "D5"; ri "LEFT@ $D4"; ex();

(* correction of silly setup with ?B^?C and ?C^?B *)

assign "?C" "?B";
top();
ri "EVERYWHERE@SELFFORCE"; ex();
wb();
ri "EVERYWHERE@SELFFORCE"; ex();
wb();

p "EQMOVE";


(* here are the old axioms of equality; I don't know whether these
are adequate *)


(* ABCBDb *)  (* b is same length as B but not necessarily equal *)

defineconstant "Eq3a@?A,?B,?C,?D" "(Eq@?A,?B,?C)*V@?D*?B";

(* the final product is actually not strictly necessary in E2 *)

(* ABCbDB *)

defineconstant "Eq3b@?A,?B,?C,?D" "Eq@?A,?B,?C*?B*?D";

(* AbCBDB *)

defineconstant "Eq3c@?A,?B,?C,?D" "Eq@(?A*?B*?C),?B,?D";

(* transitivity of equality; any two of the concepts above imply the
third *)

axiom "E2a" "(Eq3b@?A,?B,?C,?D)&Eq3c@?A,?B,?C,?D" 
"(Eq3a@?A,?B,?C,?D)&(Eq3b@?A,?B,?C,?D)&Eq3c@?A,?B,?C,?D";
axiom "E2b" "(Eq3a@?A,?B,?C,?D)&Eq3c@?A,?B,?C,?D" 
"(Eq3a@?A,?B,?C,?D)&(Eq3b@?A,?B,?C,?D)&Eq3c@?A,?B,?C,?D";
axiom "E2c" "(Eq3a@?A,?B,?C,?D)&Eq3b@?A,?B,?C,?D" 
"(Eq3a@?A,?B,?C,?D)&(Eq3b@?A,?B,?C,?D)&Eq3c@?A,?B,?C,?D";

(* quantification over a variable identified with a variable which
remains free commutes with boolean operations *)

defineinfix "FORCELESS" "?A/:?B" "?A/V@?A/?B";
(* ?A/:?B will have degree no greater than that of ?B *)

axiom "E3" "((Eq@?A,?B,?C)& ~?D/:Eq@?A,?B,?C)/V@?B/?E"
"((Eq@?A,?B,?C)/V@?B/?E)& ~((Eq@?A,?B,?C)&?D/:Eq@?A,?B,?C)/V@?B/?E";

axiom "E4" "((Eq@?A,?B,?C)&(?D/:Eq@?A,?B,?C)&?E/:Eq@?A,?B,?C)/V@?B/?E"
"(((Eq@?A,?B,?C)&(?D/:Eq@?A,?B,?C))/V@?B/?E)&((Eq@?A,?B,?C)&(?E/:Eq@?A,?B,?C))/V@?B/?E";

(* equalities of blocks are conjunctions of equalities of subblocks *)

axiom "E5" "Eq@?A,(?B*?C),?D" "(Eq@?A,?B,?C*?D)&Eq@(?A*?B),?C,?D*?B";

(* definition of Tarski cylindrification operation *)

defineconstant "Cyl@?A,?B,?C" 
"(((V@?C^?A*?B)*?C^?A*?B)&(Eq@V0,?A,?B*?C/?A*?B)&(Eq@(?A*?B),(?C/?A*?B),?A*?B))/V@?C^?A*?B";

(* lemmas on degree computation are needed *)

(* these are handled as saved environments rather than theorems *)

s "V@?C^?A*?B";
ri "FORCEDEGREE"; ex();
ri "TOPDOWN@D4**D14"; ex();
saveenv "Lemma0";

s "V@?C^?A*?B";
ri "DEGFORCESYM";
ri "FORCEDEGREE"; ex();
ri "TOPDOWN@D4**D14"; ex();
saveenv "Lemma1";

s "V@Eq@(?A*?B),(?C/?A*?B),?A*?B";
ri "EQDEGREE"; ex();
ri "TOPDOWN@D4**D14"; ex();
rri "D5"; ex();
left(); applyconvenv "Lemma1";
up(); right(); applyconvenv "Lemma1";
saveenv "Lemma2";

s "V@Eq@V0,?A,?B*?C/?A*?B";
ri "EQDEGREE"; ex();
ri "TOPDOWN@D4**D14"; ex();
ri "(LEFT@VV0)**D8b"; ex();
rri "D5"; ex();
left(); rri "D5"; ex(); applyconvenv "Lemma1";
saveenv "Lemma3"; 

(* degree of cylindrifications *)

s "V@Cyl@?A,?B,?C";
right(); ri "Cyl"; ex();
up(); ri "D14"; ex();
left(); ri "TOPDOWN@ $ANDDEGV"; ex();
downtoleft "V@Eq@?u"; applyenv "Lemma3";
top(); downtoleft "V@Eq@?u"; applyenv "Lemma2";
top();left();right();left(); ri "D4"; ri "LEFT@D1"; ex();
up(); right(); ri "ANDDEGREE"; ri "FORCEDEGREE"; ex();
right();right(); ri "RIGHT@D6"; ri "D13"; ri "LEFT@D10"; ex();
left(); ri "DEGFORCESYM**FORCEDEGREE"; ex();
ri "D4"; ri "LEFT@D4"; ri "D5**(RIGHT@ $D4)**D6";ex();
up(); ri "D10"; ex(); 
up(); ri "D5"; ex(); 
right(); ri "TOPDOWN@D4**D14**D1"; rri "D5"; ex();
applyconvenv "Lemma1";
up();up();ri "D4**RL@D1"; ex();
up(); ri "B10"; ex();
up(); ri "D4**RL@D1";
up(); ri "(RIGHT@D1)**D10"; ex();
p "CYLDEGREE";


s "Cyl@?A,?B,Null@?C";
ri "Cyl"; ex();
left();left();right();
ri "DEGFORCE"; ex();
ri "LEFT@ $D9b"; ri "D5"; ex();
up(); rri "D5"; ri "LEFT@D9a** $D9b"; ri "D5"; ri "D9b"; ex();
up(); ri "B4"; ri "B7"; ex();
ri "Null**(RIGHT@ $D1)** $Null"; ex();
right(); ri "FORCEDEGREE"; ex();
ri "D4"; ex();
left(); ri "ANDDEGREE"; ri "FORCEDEGREE"; ex();
ri "D4"; ex();
left(); applyenv "Lemma3";
up(); right(); ri "D14"; ex();
left(); applyenv "Lemma2";
up(); right(); applyenv "Lemma3";
up();left();right(); ri "DEGFORCESYM**FORCEDEGREE"; ex();
ri "TOPDOWN@D4"; ri "D5"; ex();
up(); rri "D5"; ex();
up(); ri "EVERYWHERE@ $D4"; ri "LEFT@D4"; ex();
ri "(LEFT@D6)**D10"; ex();
up();up();right(); ri "D14"; ex();
right();ri "ANDDEGREE"; ri "FORCEDEGREE"; ex();
ri "D4"; ex();
left(); applyenv "Lemma3";
up(); right(); ri "D14"; ex();
left(); applyenv "Lemma2";
up(); right(); applyenv "Lemma3";
up();left();right(); ri "DEGFORCESYM**FORCEDEGREE"; ex();
ri "TOPDOWN@D4"; ri "D5"; ex();
up(); rri "D5"; ex();
up(); ri "EVERYWHERE@ $D4"; ri "LEFT@D4"; ex();
ri "(LEFT@D6)**D10"; ex();
up();up();left(); ri "D4"; ri "LEFT@D1"; ex();
right(); ri "TOPDOWN@D4**D14"; ex(); 
ri "TOPDOWN@D4**D14"; ri "EVERYWHERE@D1"; ex();
ri "LEFT@ $NULLDEGREE"; ex(); applyconvenv "Lemma0";
up();up();right(); ri "D5"; ex();
right();right(); ri "TOPDOWN@D4**D14"; ex();
up(); rri "D5"; ex(); applyconvenv "Lemma1";
up();up(); ri "(RL@ $D4)**($D14)**V0Def"; ex();
up();ri "D8a"; ex();
top(); left();right();ri "D5"; ex();
ri "RIGHT@ $D4"; ex(); ri "D6"; ex();
top(); ri "RIGHT@ $D1"; ri "NULLQUOT"; ex();
right(); ri "TOPDOWN@D4**D14"; ex(); rri "D5"; ex();
applyconvenv "Lemma1";
top();ri "Null**(RIGHT@D1)** $Null"; ex(); 
p "C1";

(* restore old version of Q3 *)

(* s "(?A&?B)/V@?C" *)  (* target is "((?A&?B)/V@?C)&(?A^?B)/V@?C"; *)

s "((?A&?B)/V@?C)&(?A^?B)/V@?C";
right();left(); rri "ABSORB"; ex();
up(); ri "Q3"; ri "B4d"; ex();
left();left(); rri "B8"; ri "B5"; ri "RIGHT@B4"; rri "B5"; 
ri "LEFT@B8**SELFFORCE"; ex();
uptols "ABSORBd"; ri "ABSORBd"; ex();
rri "FORCEV"; ex();
right(); ri "D14"; ex();
left(); right(); ri "RIGHT@B4"; rri "FORCEV"; ex();
ri "RIGHT@ANDDEGREE"; ri "FORCEV**CANCELFORCE"; ex();
up(); rri "ANDDEGREE"; ex();
up(); rri "D14"; ex();
up(); ri "FORCEV**SELFFORCE"; ex();
wb();
p "OLDQ3";


s "?C^?A*?B";
rri "SELFFORCE"; rri "B8"; ri "AND"; ex();
right(); rri "FORCEV"; ri "SELFFORCE"; ex();
up();left();right();ri "FORCEV"; ri "SELFFORCE"; ex();
up(); ri "E1b"; ri "B4"; ex();
right(); ri "RIGHT@ $D1"; rri "Eq1"; ex();
right();right();left();
applyenv "Lemma1";
up(); up();up();ri "E5"; ex();
left(); ri "E5"; ex();
up(); ri "EVERYWHERE@D8a**D8b"; ex();
ri "EVERYWHERE@($D4)** $D14"; ex();
ri "EVERYWHERE@ $VV0";
ri "EVERYWHERE@EQV"; ex();
ri "B5"; ex();
right(); ri "B4"; ex();
up();up(); rri "B5"; rri "B5"; ri "LEFT@B5"; ex();
up();
saveenv "Lemma4";
top(); ri "OLDQ3"; ex();
left(); applyconvenv "Lemma4";
up();right();left();
rri "FORCEV"; ex();
right(); ri "EQDEGREE"; ex();
ri "TOPDOWN@D4**D14"; ex();
right();right(); ri "D5"; ex();
up();up(); rri "D5"; ex();
rri "D5"; ex(); left(); applyconvenv "Lemma1";
up();up(); rri "B8"; ri "B4";  ex();
rri "B5"; ex();
left(); ri "B4"; ri "B8"; ex();
ri "DEGFORCE"; ex();
right(); ri "D14"; ex();
right(); ri "D4"; ri "LEFT@ D1"; ex();
right(); applyenv "Lemma1";
up();up();
left(); ri "TOPDOWN@D4**D1"; ex();
up(); right(); rri "D5"; ex();ri "RL@EVERYWHERE@($D4)**($D14)"; ex();
ri "D6"; ex(); ri "RL@TOPDOWN@D4**D14"; ex();
up(); ri "D13"; ex();
left(); ri "EVERYWHERE@($D4)**($D14)"; ri "V0Def"; ex();
up(); ri "RIGHT@EVERYWHERE@($D4)**($D14)"; ri "QUOTOFV0"; ex();
up(); ri "D8a"; ex();
top(); right(); rri "Cyl"; ex();
p "C2";

(* miscellaneous results from concepts2 *)

s "(V@(?A^?B))/V@?B";
left(); ri "DEGFORCESYM"; ri "FORCEDEGREE"; ex();
ri "D4"; ri "D6"; up(); ri "D10"; ex();
p "FORCEQUOTLEMMA";

s "Cyl@?A,?B,?C^?D";
ri "Cyl"; ex();
ri "EVERYWHERE@($EQV)"; ex();
ri "TOPDOWN@D1**D4**D14"; ex();
ri "EVERYWHERE@ $VFORCE"; ex();
left();right(); ri "EVERYWHERE@VFORCE"; ex();
top(); ri "EVERYWHERE@DEGFORCESYM"; ex();
ri "EVERYWHERE@VFORCE"; ex();
ri "EVERYWHERE@ ($D14)**($D4)"; ex();
ri "EVERYWHERE@EQV"; ex();
p "CounterCyl";

(* next target: *)

(* degree independence of Cyl *)

s "Cyl@?A,?B,?C^?C*?D";
ri "Cyl"; ex();

(* next target is C3 *)

(* another approach; define Cyl differently so as to be able to take
advantage of properties of permutations *)

(* under construction

approach for C3:  pi-(pi(A)/C) & pi-(pi(B)/C) = pi-((pi(A) & pi(B)/C)/C) by
known result; this is pi-(pi(A & pi-(pi(B)/C))/C), giving C3 as a trivial
consequence of the properties of pi and pi-. 


this isn't right.  quantification is pi-(pi(A)/C)


defineconstant "Perm@?A,?B,?C"
"((V@(?C^?A*?B)*?B)*(?C^?A*?B)*V@?B)&(Eq@V0,?A,?B*(?C/?A*?B)*?B)&(Eq@?A,?B,(?C/?A*?B)*?B*?C^?A*?B)&(Eq@?A*?B,?C/?A*?B,?B*?A)

*)

quit();