(* ======== Robbins Conjecture proof from John ============================= *)

hide_constant "+";;
horizon := 0;;
timeout := 2;; (* John apparently has a faster computer :-) *)

let ROBBINS = thm `;
  
  let (+) be A->A->A;
  let n be A->A;
  
  assume !x y. x+y = y+x [COM];
  assume !x y z. x+(y+z) = (x+y)+z [ASS];
  assume !a b. n(n(a+b)+n(a+n(b))) = a [ROB];
  
  consider x such that x:A = x;
  
  set u = n(x+n(x)) [U];
  set d = x+u [D];
  set c = x+x+x+u [C];
  set j = n(c+d) [J];
  set e = u+n(x+x)+n(c) [E];
  
  n(u+n(x+x)) = x [0]
  proof n(u+n(x+x))
      = n(n(x+n(x))+n(x+x)) by U;
     .= x by ROB,COM;
  qed by -;
  
  n(x+u+n(x+u+n(x+x)+n(c))) = n(c) [1]
  proof n(x+u+n(x+u+n(x+x)+n(c)))
      = n((x+u)+n(x+u+n(x+x)+n(c))) by ASS,COM;
     .= n(n(n((x+u)+x+x)+n((x+u)+n(x+x)))+n(x+u+n(x+x)+n(c))) by ROB;
     .= n(n(n(x+u+x+x)+n(x+u+n(x+x)))+n(x+u+n(x+x)+n(c))) by ASS;
     .= n(n(n(x+x+x+u)+n(x+u+n(x+x)))+n(x+u+n(x+x)+n(c))) by ASS,COM; // slow
     .= n(n(n(c)+n(x+u+n(x+x)))+n(n(c)+x+u+n(x+x))) by ASS,COM,C;
     .= n(c) by ROB,ASS,COM;
  qed by -;                                   
                                  
  n(u+n(c)) = x [2]     
  proof n(u+n(c))
      = n(u+n(x+x+u+x)) by C,ASS,COM;                                           
     .= n(u+n(x+x+u+n(u+n(x+x)))) by 0;                    
     .= n(n(n(u+x+x)+n(u+n(x+x)))+n(x+x+u+n(u+n(x+x)))) by ROB;
     .= n(n(x+x+u+n(u+n(x+x)))+n(n(u+x+x)+n(u+n(x+x)))) by COM;
     .= n(n((x+x+u)+n(u+n(x+x)))+n(n(u+x+x)+n(u+n(x+x)))) by ASS;
     .= n(n(n(u+n(x+x))+u+x+x)+n(n(u+n(x+x))+n(u+x+x))) by ASS,COM;
     .= n(u+n(x+x)) by ROB;
     .= x by 0;
  qed by -;
  
  n(j+u) = x [3]
  proof n(j+u)
      = n(n(x+c+u)+u) by J,D,COM,ASS;
     .= n(n(x+c+u)+n(n(u+c)+n(u+n(c)))) by ROB;
     .= n(n(x+c+u)+n(x+n(c+u))) by 2,COM;
     .= x by ROB;
  qed by -;
  
  n(x+n(x+n(x+x)+u+n(c))) = n(x+x) [4]
  proof n(x+n(x+n(x+x)+u+n(c)))
      = n(n(n(x+n(u+n(c)))+n(x+u+n(c)))+n(x+n(x+x)+u+n(c)))
            by ROB,ASS,COM;
     .= n(n(n(x+x)+n(x+u+n(c)))+n(n(x+x)+x+u+n(c))) by 2,ASS,COM;
     .= n(n(n(x+x)+x+u+n(c))+n(n(x+x)+n(x+u+n(c)))) by ASS,COM;
     .= n(x+x) by ROB,COM;
  qed by -;
  
  n(x+n(c)) = u [5]
  proof n(x+n(c))
      = n(x+n(x+u+n(x+u+n(x+x)+n(c)))) by 1;
     .= n(n(u+n(x+x))+n(x+u+n(x+u+n(x+x)+n(c)))) by 0;
     .= n(n(u+n(x+x))+n(u+x+n(x+e))) by E,COM,ASS;
     .= n(n(u+n(x+n(x+n(x+x)+u+n(c))))+n(u+x+n(x+e))) by 4;
     .= n(n(u+n(x+n(x+(u+n(c))+n(x+x))))+n(u+x+n(x+e))) by COM;
     .= n(n(u+n(x+n(x+u+n(c)+n(x+x))))+n(u+x+n(x+e))) by ASS;
     .= n(n(u+n(x+n(x+u+n(x+x)+n(c))))+n(u+x+n(x+e))) by COM;
     .= n(n(u+n(x+n(x+e)))+n(u+x+n(x+e))) by E;
     .= u by ROB,COM;
  qed by -;
  
  n(j+x) = u [6]
  proof n(j+x)
      = n(j+n(n(x+c)+n(x+n(c)))) by ROB;
     .= n(j+n(n(x+c)+u)) by 5;
     .= n(n(u+x+c)+n(u+n(x+c))) by J,D,COM,ASS;
     .= u by ROB;
  qed by -;
  
  n(c+d) = n(c)
  proof n(c+d)
      = j by J;
     .= n(n(j+n(x+n(c)))+n(j+x+n(c))) by ROB,COM;
     .= n(n(j+u)+n(j+x+n(c))) by 5;
     .= n(x+n(j+x+n(c))) by 3;
     .= n(n(n(c)+u)+n(n(c)+j+x)) by 2,COM,ASS;
     .= n(n(n(c)+n(j+x))+n(n(c)+j+x)) by 6;
     .= n(c) by ROB,COM;
  qed by -;
  
  thus ?c d. n(c+d) = n(c) by -`;;

timeout := 1;;

(* ======== REWRITE version ================================================ *)

let old_default_prover = !default_prover;;
default_prover := "REWRITE_TAC",REWRITE_TAC;;

let ROBBINS = thm `;
  
  let (+) be A->A->A;
  let n be A->A;
  
  assume !x y. x+y = y+x [COM];
  assume !x y z. x+(y+z) = (x+y)+z [ASS];
  assume !a b. n(n(a+b)+n(a+n(b))) = a [ROB];
  
  !x y z. x+y = y+x /\ (x+y)+z = x+(y+z) /\ x+(y+z) = y+(x+z) [AC]
    by MESON_TAC,COM,ASS;
  
  consider x such that x:A = x;
  
  set u = n(x+n(x)) [U];
  set d = x+u [D];
  set c = x+x+x+u [C];
  set j = n(c+d) [J];
  set e = u+n(x+x)+n(c) [E];
  
  n(u+n(x+x)) = x [0]
  proof n(u+n(x+x))
      = n(n(x+x)+n(x+n(x))) by U,AC;
     .= x by ROB;
  qed by -;
  
  n(x+u+n(x+u+n(x+x)+n(c))) = n(c) [1]
  proof n(x+u+n(x+u+n(x+x)+n(c)))
      = n((x+u)+n(x+u+n(x+x)+n(c))) by AC;
     .= n(n(n((x+u)+x+x)+n((x+u)+n(x+x)))+n(x+u+n(x+x)+n(c))) by ROB;
     .= n(n(n(c)+x+u+n(x+x))+n(n(c)+n(x+u+n(x+x)))) by C,AC;
     .= n(c) by ROB;
  qed by -;
  
  n(u+n(c)) = x [2]
  proof n(u+n(c))
      = n(u+n(x+x+u+n(u+n(x+x)))) by 0,C,AC;
     .= n(n(n(u+x+x)+n(u+n(x+x)))+n(x+x+u+n(u+n(x+x)))) by ROB;
     .= n(n(n(u+n(x+x))+u+x+x)+n(n(u+n(x+x))+n(u+x+x))) by AC;
     .= n(u+n(x+x)) by ROB;
     .= x by 0;
  qed by -;
  
  n(j+u) = x [3]
  proof n(j+u)
      = n(n(x+c+u)+u) by J,D,AC;
     .= n(n(x+c+u)+n(n(u+c)+n(u+n(c)))) by ROB;
     .= n(n(x+c+u)+n(x+n(c+u))) by 2,AC;
     .= x by ROB;
  qed by -;
  
  n(x+n(x+n(x+x)+u+n(c))) = n(x+x) [4]
  proof n(x+n(x+n(x+x)+u+n(c)))
      = n(n(n(x+u+n(c))+n(x+n(u+n(c))))+n(x+n(x+x)+u+n(c))) by ROB;
     .= n(n(n(x+x)+x+u+n(c))+n(n(x+x)+n(x+u+n(c)))) by 2,AC;
     .= n(x+x) by ROB;
  qed by -;
  
  n(x+n(c)) = u [5]
  proof n(x+n(c))
      = n(n(u+n(x+x))+n(x+u+n(x+u+n(x+x)+n(c)))) by 0,1;
     .= n(n(u+n(x+n(x+n(x+x)+u+n(c))))+n(u+x+n(x+e))) by 4,E,AC;
     .= n(n(u+x+n(x+e))+n(u+n(x+n(x+e)))) by E,AC;
     .= u by ROB;
  qed by -;
  
  n(j+x) = u [6]
  proof n(j+x)
      = n(j+n(n(x+c)+n(x+n(c)))) by ROB;
     .= n(n(u+x+c)+n(u+n(x+c))) by 5,J,D,AC;
     .= u by ROB;
  qed by -;
  
  n(c+d) = n(c)
  proof n(c+d)
      = j by J;
     .= n(n(j+x+n(c))+n(j+n(x+n(c)))) by ROB;
     .= n(n(u+n(c))+n(j+x+n(c))) by 2,3,5,AC;
     .= n(n(n(c)+j+x)+n(n(c)+n(j+x))) by 6,AC;
     .= n(c) by ROB;
  qed by -;
  
  thus ?c d. n(c+d) = n(c) by MESON_TAC,-`;;

unhide_constant "+";;
default_prover := old_default_prover;;