// JavaScript Program to implement an equational decision procedure for lattice-ordered groups
// version of 11 Feb 2003, by Peter Jipsen, http://www.chapman.edu/jipsen

// The code has three main parts to it:
// 1. Handling formulas (actually only the part about equations and inequations is used)
//      parsing the ascii input and writing html output.
// 2. Implementing the decision procedure.
// 3. Administering the l-group quiz

// Part 1. Handling formulas
//check if the symbol font is available
symb = navigator.appVersion.lastIndexOf('Win')!=-1 ||
    navigator.appVersion.lastIndexOf('Mac')!=-1;

function out(col,str,alt,sp) {
  return sp+"<font"+(col==""?"" : " color="+col)+
    (alt==""?">"+str : (symb?" >"+str : ">"+alt))+"</font>"+sp;
}

bl="&nbsp;";

avar = {name:"a", arity:0, output:"<i>a</i>"};
bvar = {name:"b", arity:0, output:"<i>b</i>"};
cvar = {name:"c", arity:0, output:"<i>c</i>"};
dvar = {name:"d", arity:0, output:"<i>d</i>"};
Avar = {name:"A", arity:0, output:"<i>A</i>"};
Bvar = {name:"B", arity:0, output:"<i>B</i>"};
Cvar = {name:"C", arity:0, output:"<i>C</i>"};
Dvar = {name:"D", arity:0, output:"<i>D</i>"};
xvar = {name:"x", arity:0, output:"<i>x</i>"};
yvar = {name:"y", arity:0, output:"<i>y</i>"};
zvar = {name:"z", arity:0, output:"<i>z</i>"};
Xvar = {name:"X", arity:0, output:"<i>X</i>"};
Yvar = {name:"Y", arity:0, output:"<i>Y</i>"};
Zvar = {name:"Z", arity:0, output:"<i>Z</i>"};

vari = [ avar, Avar, bvar, Bvar, cvar, Cvar, dvar, Dvar, xvar, Xvar, yvar, Yvar, zvar, Zvar ];

unit = {name:"e", arity:0, output:"<i>e</i>"};

cons = [unit];

meet = {name:"^", arity:2, priority:6, output:out("Blue","&and;","^",bl),
   infix:true, paren:true};
join = {name:"v", arity:2, priority:6, output:out("Blue","&or;","v",bl),
   infix:true, paren:true};
times = {name:"*", arity:2, priority:8,
   output:out("Blue","*","*",""), infix:true, paren:true};
over = {name:"/", arity:2, priority:8,
   output:'<font color="Blue">/</font>', infix:true, paren:true};
under = {name:"\\", arity:2, priority:8,
   output:'<font color="Blue">\\</font>', infix:true, paren:true};

oper = [ meet, join, times, over, under ];

eq   = {name:"=",  arity:2, output:'<font color="Red"> = </font>', infix:true, priority:4};
leq  = {name:"<=", arity:2, output:out("Red","&le;","&lt;=",bl),
  infix:true,  priority:4};
geq  = {name:">=", arity:2, output:out("Red","&ge;","&gt;=",bl),
  infix:true,  priority:4};

pred = [ eq, leq, geq ];

for (var i=0; i<vari.length; i++) vari[i].vari=true;
for (var i=0; i<cons.length; i++) cons[i].cons=true;
for (var i=0; i<oper.length; i++) oper[i].oper=true;
for (var i=0; i<pred.length; i++) pred[i].pred=true;

notSymbol = {name:"~",  arity:1,
  output:'<font color="Blue">~</font>'};
impSymbol = {name:"->", arity:2, priority:1,
  output:'&nbsp;<font color="Blue">==></font>&nbsp;',
  infix:true,paren:true};
andSymbol = {name:"and", arity:2, priority:3,
  output:'&nbsp;<font color="Blue"> and </font>&nbsp;',
  infix:true,paren:true};
orSymbol = {name:"or", arity:2, priority:2,
  output:'&nbsp;<font color="Blue"> or </font>&nbsp;',
  infix:true,paren:true};
iffSymbol = {name:"iff", arity:2, priority:0,
  output:'&nbsp;&nbsp;<font color="Blue"> iff </font>&nbsp;&nbsp;',
  infix:true,paren:true};
allSymbol = {name:"A",  arity:2, 
  output:'<font face="Symbol" color="Blue">"</font>'};
exSymbol = {name:"E",  arity:2, 
  output:'<font face="Symbol" color=Blue>$</font>'};

conn = [notSymbol, andSymbol, orSymbol, impSymbol, iffSymbol, allSymbol, exSymbol];

comma = {name:",", punc:true};
leftBracket = {name:"(", punc:true};
rightBracket = {name:")", punc:true};
leftSqBracket = {name:"[", punc:true};
rightSqBracket = {name:"]", punc:true};

punc = [comma, leftSqBracket, rightSqBracket, leftBracket, rightBracket ];


function add(arr, elt){    // the push method is not supported in IExpl*der
  arr[arr.length]=elt;
}

function Expr(symbol, arg, priority){ // third argument only used during parsing
  this.symbol = symbol;
  this.arg = arg;
  this.priority = priority;
}

function randomInt(n) {
  return Math.floor(n*Math.random());
}

function randomElt(a) {
  return a[Math.floor(a.length*Math.random())];
}

function randomVari(){
  return new Expr(randomElt(vari.slice(8)), [])
}

function randomList(len,max){
//random list of values in [0..max-1] with one of them = max-1
  var l=[];
  for (var i=0; i<len; i++)
    add(l,randomInt(max));
  l[randomInt(len)]=max-1;
  return l;
}

function randomTerm(depth){
  if (depth > 0) {
    var op=randomElt(oper);
    var dep=randomList(op.arity,depth);
    var arg=[];
    for (var i=0; i<op.arity; i++)
      add(arg,randomTerm(dep[i]));
    return new Expr(op, arg);
  }
  if (Math.random()<0.7) 
    return new Expr(randomElt(vari.slice(8)), []);
  return new Expr(randomElt(cons), []);
}

function randomFormula(fDepth,tDepth){
  if (fDepth > 0) {
    var co=randomElt(conn);
    if (co==allSymbol || co==exSymbol){ 
      var arg = [randomVari(), randomFormula(fDepth-1,tDepth)];
      return new Expr(co, arg);
    }
    var dep=randomList(co.arity,fDepth);
    var arg=[];
    for (var i=0; i<co.arity; i++)
      add(arg,randomFormula(dep[i],tDepth));
    return new Expr(co, arg);
  }
  var pr=randomElt(pred);
  var dep=randomList(pr.arity,tDepth);
  var arg=[];
  for (var i=0; i<pr.arity; i++)
    add(arg,randomTerm(dep[i]));
  return new Expr(pr, arg);
}

function e2s(q) {//convert expression to string
  if (q.arg.length==0) return q.symbol.output;
  if (q.symbol==allSymbol || q.symbol==exSymbol)
    return q.symbol.output + e2s(q.arg[0]) + "&nbsp;" + e2s(q.arg[1]);
  else if (q.symbol.infix)
    if (q.symbol.paren) return "(" + e2s(q.arg[0]) + 
      q.symbol.output + (q.arg.length==2?e2s(q.arg[1]):"") + ")";
    else return e2s(q.arg[0]) + q.symbol.output + (q.arg.length==2?e2s(q.arg[1]):"");
  var st = "";
  for (var i = 0; i < q.arg.length-1; i = i+1)
    st = st + e2s(q.arg[i]) + ",";
  st = st + e2s(q.arg[q.arg.length-1]);
  if (q.symbol.paren) return q.symbol.output + "(" + st + ")";
  else return q.symbol.output + st;
}

//Parsing ascii strings into expressions

//First we concatenate all the symbol arrays

function compareNames(s1,s2) {
  if (s1.name > s2.name) return 1
  else return -1;
}

symbols = vari.concat(cons, oper, pred, conn, punc);
symbols.sort(compareNames);
names = [];
for (var i=0; i<symbols.length; i++) names[i] = symbols[i].name;

maxPriority=0;
for (var i=0; i<symbols.length; i++)
  if (symbols[i].priority && symbols[i].priority>maxPriority)
    maxPriority = symbols[i].priority;
maxPriority++;

//names should contain no blanks

function removeCharsAndBlanks(str,n) {
  var st = str.slice(n);
  for (var i=0; i<st.length && st.charAt(i)==" "; i=i+1);
  return st.slice(i);
}

function position(arr, str, n) { // assumes arr is sorted
  for (var i=n; i<arr.length && arr[i]<str; i++);
  return i; // i=arr.length || arr[i]>=str
}

function getSymbol(str) {
  var k=0;
  var j=0;
  var st="";
  var oldst="";
  var more = true;
  for (var i=1; i<=str.length && more; i++) {
    oldst=st;
    st=str.slice(0,i);
    j=k;
    k=position(names, st, j);
    more = (k<names.length && st==names[k].slice(0,i))
  }
  if (k==names.length) return null;
  if (!more) st=oldst;
  else j=k;
  if (st==names[j]) return symbols[j]; //maximal substring that appears in names
  else return null;
}

aSymbols = symbols.concat([{name:"  ", output:" &nbsp; "}]);
aSymbols.sort(compareNames);
aNames = [];
for (var i=0; i<aSymbols.length; i++) aNames[i] = aSymbols[i].name;

function a2h(str) {
  var j,k;
  var st,oldst,hstr;
  var more;
  while (str!="") {
    k=0;
    st="";
    more=true;
    for (var i=1; i<=str.length && more; i++) {
      oldst=st;
      st=str.slice(0,i);
      j=k;
      k=position(aNames, st, j);
      more = (k<aNames.length && st==aNames[k].slice(0,i));
    }
    if (!more) st=oldst;
    else j=k;
    if (st==aNames[j]) {
      hstr = hstr.concat(aSymbols[j].output);
      str = str.slice(st.length);
    } else {
      hstr = hstr.concat(st.charAt(0));
      str = str.slice(1);
    }
  }
  return hstr;
}

/*
blanks ( ) [ ] , are seperators (not allowed in names of symbols)
Arguments may be separated by spaces or single commas.
Parenthesis must be balanced.

Symbols are either terminal (arity==0) or prefix or infix (unary infix defaults to postfix)

expr ::= terminal | prefix expr1 ... exprN | prefix(expr1, ... , exprN) | 

         expr infix | expr1 infix exprN | (expr) | [expr]

Expressions are read from left to right, choosing the longest initial substring
that matches the name of a symbol. Symbol priority is taken into account.
*/

function str2expr(str) { //builds expr and returns [expr,substring]
// If returned substring starts with "Error: ..." it contains information about a parsing error
  var arg=[];
  var token="";
  var symbol;
  var nextsymbol;
  var expr;
  var estr;
  str=removeCharsAndBlanks(str,0);
  symbol=getSymbol(str); //either a symbol or a bracket or empty
  if (symbol==null||symbol==rightBracket||symbol==rightSqBracket) 
    return [null,"Error, '(', '[' or symbol expected: "+str];
  str=removeCharsAndBlanks(str,symbol.name.length); 

  if (symbol==leftBracket) {                        //read (expr)
    estr=str2expr(str);expr=estr[0];str=estr[1];
    expr.priority = maxPriority;
    if (str.slice(0,5)=="Error") return [null,str];
    symbol=getSymbol(str);
    str=removeCharsAndBlanks(str,symbol.name.length); 
    if (symbol!=rightBracket) return [null,"Error, ')' expected : "+str];

  } else if (symbol==leftSqBracket) {               //read [expr]
    estr=str2expr(str);expr=estr[0];str=estr[1];
    expr.priority = maxPriority;
    if (str.slice(0,5)=="Error") return [null,str];
    symbol=getSymbol(str);
    str=removeCharsAndBlanks(str,symbol.name.length); 
    if (symbol!=rightSqBracket) return [null,"Error, ']' expected: "+str];

  } else if (symbol==null) {
    return [null,"Error, incorrect symbol : "+symbol.name+" "+str];

  } else if (symbol.arity==0) {                     //read terminal
    expr=new Expr(symbol,[], maxPriority);

  } else {                          //read prefix expr1 ... exprN or prefix(...)
    if (symbol.infix) return [null,"Error, misplaced infix symbol: "+symbol.name+" "+str];
    var more = true;
    nextsymbol = getSymbol(str);
    var commas=false;
    if (nextsymbol==leftBracket) {
      str = removeCharsAndBlanks(str,symbol.name.length);
      commas=true;
    }
    while (str!="" && more) {
      nextsymbol = getSymbol(str);
      if (nextsymbol==null) return [null,"Error, incorrect symbol: "+str];
      estr=str2expr(str);expr=estr[0];str=estr[1];
      if (str.slice(0,5)=="Error") return [null,str];
      add(arg,expr);
      if (commas)
        if (str=="") return [null,"Error, ')' expected: "+str];
        else if (str.charAt(0)==",") str=removeCharsAndBlanks(str,1);
        else if (str.charAt(0)==")") {
          more = false;
          str=removeCharsAndBlanks(str,1);
        }
    }
    expr=new Expr(symbol, arg, maxPriority);
  }

//parse right argument of infix operation
  symbol = getSymbol(str);
  var insert=null;
  if (symbol==null || !symbol.infix) return [expr,str];
  str = removeCharsAndBlanks(str,symbol.name.length);
  if (str=="" || str.charAt(0)==")" || str.charAt(0)=="]") { //unary infix symbol
    expr=new Expr(symbol, [expr], maxPriority); 
//document.write(symbol.name+expr);
    return [expr,str];
  }
  var right=null;
  estr = str2expr(str);right=estr[0];str=estr[1];
  if (str.slice(0,5)=="Error") return [null,str];
  if (right.priority>symbol.priority || 
      (right.priority==symbol.priority && right.symbol.rightparen)) {
    expr=new Expr(symbol, [expr,right], symbol.priority); 
  } else {
    insert=right;
    while (insert.arg[0].priority && insert.arg[0].priority<symbol.priority) 
      insert=insert.arg[0];
    if (insert.arg[0].priority>symbol.priority || insert.arg[0].symbol.rightparen) {
      expr=new Expr(symbol, [expr,insert.arg[0]], symbol.priority);
      insert.arg[0]=expr;
    } else {
      expr=new Expr(symbol, [expr,insert.arg[0].arg[0]], symbol.priority);
      insert.arg[0].arg[0]=expr;
    }
    expr=right;
  }
  return [expr,str];
}

function parse(str) {
  var temp = str2expr(str);
  if (temp[1].slice(0,5)=="Error") document.write("<P>"+temp[1]+"<P>");
  else if (temp[1].slice(0,5)!="") document.write("<P>Parse Leftover: "+temp[1]+"<P>");

//still have to check arities of expressions

  return temp[0];
}

function outputList(li) {
  for (var i=0; i<li.length; i=i+1)
    document.write(" &nbsp;"+li[i].output);
}

function symbolString(li) {
  var st="";
  for (var i=0; i<li.length; i=i+1)
    st=st+" &nbsp;"+li[i].output;
  return st;
}

//*******************************************************
// Part 2. Implementing the decision procedure.

function position1(arr, str) { // does not assume arr is sorted
  for (var i=0; i<arr.length && arr[i]!=str; i++);
  return i; // i=arr.length || arr[i]>=str
}

function inverse(v) {
  if (v=="x") return "X";
  if (v=="X") return "x";
  if (v=="y") return "Y";
  if (v=="Y") return "y";
  if (v=="z") return "Z";
  if (v=="Z") return "z";
  if (v=="a") return "A";
  if (v=="A") return "a";
  if (v=="b") return "B";
  if (v=="B") return "b";
  if (v=="c") return "C";
  if (v=="C") return "c";
  if (v=="d") return "D";
  if (v=="D") return "d";
  return "Error";
}

function invert(t) {
  if (t.symbol==unit) return t;
  if (t.symbol.name=="A") return new Expr(vari[0], []);
  if (t.symbol.name=="a") return new Expr(vari[1], []);
  if (t.symbol.name=="B") return new Expr(vari[2], []);
  if (t.symbol.name=="b") return new Expr(vari[3], []);
  if (t.symbol.name=="C") return new Expr(vari[4], []);
  if (t.symbol.name=="c") return new Expr(vari[5], []);
  if (t.symbol.name=="D") return new Expr(vari[6], []);
  if (t.symbol.name=="d") return new Expr(vari[7], []);
  if (t.symbol.name=="X") return new Expr(vari[8], []);
  if (t.symbol.name=="x") return new Expr(vari[9], []);
  if (t.symbol.name=="Y") return new Expr(vari[10], []);
  if (t.symbol.name=="y") return new Expr(vari[11], []);
  if (t.symbol.name=="Z") return new Expr(vari[12], []);
  if (t.symbol.name=="z") return new Expr(vari[13], []);
  if (t.symbol==meet) 
    return new Expr(join,[invert(t.arg[0]),invert(t.arg[1])]);
  if (t.symbol==join) 
    return new Expr(meet,[invert(t.arg[0]),invert(t.arg[1])]);
  if (t.symbol==times) 
    return new Expr(times,[invert(t.arg[1]),invert(t.arg[0])]);
  if (t.symbol==over) 
    return new Expr(times,[t.arg[1],invert(t.arg[0])]);
  if (t.symbol==under) 
    return new Expr(times,[invert(t.arg[1]),t.arg[0]]);
}

function trou(t) {
  if (t.symbol==unit || t.symbol.vari) return t;
  if (t.symbol==meet || t.symbol==join || t.symbol==times) 
    return new Expr(t.symbol,[trou(t.arg[0]),trou(t.arg[1])]);
  if (t.symbol==over) 
    return new Expr(times,[trou(t.arg[0]),invert(trou(t.arg[1]))]);
  if (t.symbol==under) 
    return new Expr(times,[invert(trou(t.arg[0])),trou(t.arg[1])]);
alert("error "+t.symbol);
}

function negcone(t) {
  if (t.symbol==unit) return t;
  if (t.symbol.vari) return new Expr(meet, [t,new Expr(unit,[])]);
  if (t.symbol==over) 
    return new Expr(meet,
      [new Expr(over,[negcone(t.arg[0]),negcone(t.arg[1])]),new Expr(unit,[])]);
  if (t.symbol==under) 
    return new Expr(meet,
      [new Expr(under,[negcone(t.arg[0]),negcone(t.arg[1])]),new Expr(unit,[])]);
  if (t.symbol==times) 
    return new Expr(times,[negcone(t.arg[0]),negcone(t.arg[1])]);
  if (t.symbol==join) 
    return new Expr(join,[negcone(t.arg[0]),negcone(t.arg[1])]);
  if (t.symbol==meet) 
    return new Expr(meet,[negcone(t.arg[0]),negcone(t.arg[1])]);
}

function gmv(t) {
  if (t.symbol==unit) return t;
  if (t.symbol.vari) return new Expr(join, [t,new Expr(vari[6],[])]);
  if (t.symbol==over) 
    return new Expr(over,[gmv(t.arg[0]),gmv(t.arg[1])]);
  if (t.symbol==under) 
    return new Expr(under,[gmv(t.arg[0]),gmv(t.arg[1])]);
  if (t.symbol==times) 
    return new Expr(join,
      [new Expr(times,[gmv(t.arg[0]),gmv(t.arg[1])]),new Expr(vari[6],[])]);
  if (t.symbol==join) 
    return new Expr(join,[gmv(t.arg[0]),gmv(t.arg[1])]);
  if (t.symbol==meet) 
    return new Expr(meet,[gmv(t.arg[0]),gmv(t.arg[1])]);
}

function objToString(a) {
  var st="";
//document.write("\n<br> type=",typeof a);
  if (typeof a =="string") st="\""+a+"\"";
  else if (a.length>0) {
    for (var i=0; i<a.length; i++)
      st=st+objToString(a[i])+(i==a.length-1?"":", ");
    st="["+st+"]";
  }
  else st=a.toString();
  return st;
}

function assignmentsList(a,i,w,v) {
  var k=0;
  var l=a.length;
//document.write("\n<br>AssignmentsList w="+w+" v="+v+" a.length="+a.length);
  for (j=i+1; j<a.length; j++) {
    var n=a[j].length;
    if (a[j].charAt(n-1)==inverse(v)) {
      l=position1(a,a[j].slice(0,n-1));
      break;
    } 
    else {
      l=position1(a,a[j]+v);
//document.write(" l=",l);
      if (l!=a.length) break;
    }
  }
  for (j=i-1; j>=0; j--) {
    var n=a[j].length;
    if (a[j].charAt(n-1)==inverse(v)) {
      k=position1(a,a[j].slice(0,n-1))+1;
      break;
    } 
    else {
      k=position1(a,a[j]+v)+1;
      if (k!=a.length+1) break;
    }
  }
  if (k==a.length+1) k=0;
  var al=[];
  for (j=k; j<=l; j++)
    add(al,[a.slice(0,j).concat([w],a.slice(j)),j]);
//document.write(" al=",objToString(al));
  return al;
}

function evaluateLGterm(t,a,i) {
  var al,bl;
//parent.output.document.writeln(e2s(t)+"\n");
  if (t.symbol==unit) return [[a,i]];
//document.write("\n<br>evaluateLGterm t.symbol.name="+t.symbol.name);
  if (t.symbol.vari) {
    var n=a[i].length;
    var w;
    if (n>0 && t.symbol.name==inverse(a[i].charAt(n-1))) 
      w=a[i].slice(0,n-1);
    else
      w=a[i]+t.symbol.name;
    j=position1(a,w);
    if (j!=a.length) return [[a,j]];
    else return assignmentsList(a,i,w,t.symbol.name);
  }
  if (t.symbol==times) {
    al=evaluateLGterm(t.arg[0],a,i);
    bl=[];
    for (var k=0; k<al.length; k++) {//***eliminate duplicates
      bl=bl.concat(evaluateLGterm(t.arg[1],al[k][0],al[k][1])); 
    }
    return bl;
  }
  if (t.symbol==join||t.symbol==meet) {
    al=evaluateLGterm(t.arg[0],a,i);
    var cl=[];
    for (var m=0; m<al.length; m++) {
      var i1=position1(al[m][0],a[i]);
      bl=evaluateLGterm(t.arg[1],al[m][0],i1);
      for (var n=0; n<bl.length; n++) {
        j1=position1(bl[n][0],al[m][0][al[m][1]]);
        if (t.symbol==join)
          if (j1<=bl[n][1]) add(cl,bl[n]);
          else add(cl,[bl[n][0],j1]);
        else
          if (j1>=bl[n][1]) add(cl,bl[n]);
          else add(cl,[bl[n][0],j1]);
      }
    }
    return cl;
  }
}

function isTermPositive(t) {
  var al=evaluateLGterm(t,[""],0);
//document.write("\n<br>Number of diagrams checked = ",al.length);
//               " al=",objToString(al));
  for (var i=0; i<al.length; i++)
    if (position1(al[i][0],"")>al[i][1]) {
//document.write(", fails at ",objToString(al[i]));
      return [false,al,i,t];
    }
  return [true,al,0,t];
}

function isTermIdentity(t) {
  var al=evaluateLGterm(t,[""],0);
//document.write("\n<br>Number of diagrams checked = ",al.length);
  for (var i=0; i<al.length; i++)
    if (position1(al[i][0],"")!=al[i][1]) {
//document.write(", fails at ",objToString(al[i]));
      return [false,al,i,t];
    }
  return [true,al,0,t];
}

function checkEquation(t) {
//parent.output.document.write(e2s(trou(t.arg[0])));
  if (t.symbol==eq)
    return isTermIdentity(new Expr(times, [trou(t.arg[0]),invert(t.arg[1])]));
  if (t.symbol==leq)
    return isTermPositive(new Expr(times, [trou(t.arg[1]),invert(t.arg[0])]));
  if (t.symbol==geq)
    return isTermPositive(new Expr(times, [trou(t.arg[0]),invert(t.arg[1])]));
  return ["Error, not an equation or inequality",[],0];
}

function checkNegConeEquation(t) {
  return checkEquation(new Expr(t.symbol, [negcone(t.arg[0]),negcone(t.arg[1])]));
}

function checkGMVEquation(t) {
  return checkEquation(new Expr(t.symbol, [negcone(gmv(t.arg[0])),negcone(gmv(t.arg[1]))]));
}


//**************************************
// Part 3. Administering the LG quiz

//generate inequations for quiz
inequations=[];
for (var i=0; i<5; i=i+1)
  add(inequations,new Expr(leq,[randomTerm(2),randomTerm(2)]));

function correct(win, score, st) {
  win.document.write("<font color=Green>Correct, "+st+", 1 point.</font>");
  return score+1;
}

function wrong(win, score, st) {
  win.document.write("<font color=Red>Wrong, "+st+", -1 point.</font>");
  return score-1;
}

function comment(win, st) {
  win.document.write("<center><font color=Blue>"+st+"</font></center>");
}

function check(frm) { //analyse the radio buttons and output results
  win=open("", "resultWindow", "height=450,width=750,menubar=yes,resizable=yes,scrollbars=yes");
  win.document.open();
  var score=0;
  win.document.write("<html><head><title>Quiz Results");
  win.document.write("</title></head><body><h3 align=center>"+
    "Results for your personalised Quiz 1</h3>");
  for (var i=0; i<inequations.length; i=i+1){
    win.document.write((i+1)+". &nbsp; "+
      e2s(inequations[i])+"&nbsp;&nbsp; ");
    proof=[];
    proofattempt=[];
    var ans=checkEquation(inequations[i])[0];
    if (!frm.elements[2*i].checked && !frm.elements[2*i+1].checked)
      win.document.write("Undecided, 0 points");
    else if (ans)
      if (frm.elements[2*i].checked)
        score=correct(win, score, "this is True in LG");
      else
        score=wrong(win, score, "this is True in LG");
    else if (frm.elements[2*i+1].checked)
      score=correct(win, score, "this is False in LG");
    else
      score=wrong(win, score, "this is False in LG");
  win.document.write("<br>");
  }
  win.document.write("<h3 align=center><font color=Red>"+
    "Your Score is "+score+"/"+inequations.length+"</font></h3>");
  if (score<1) comment(win,"Guessing will get you nowhere :-)");
  else if (score<inequations.length/2) 
    comment(win,"You need to practise your l-group derivations :-)");
  else if (score<0.75*inequations.length) comment(win,"l-group inequations can be quite tricky.");
  else if (score<inequations.length) 
    comment(win,"Pretty good, you seem to know what you are doing.");
  else comment(win,"Congratulations, you're an expert!");
  win.document.write('<p><center>Click the X in the top right '+
    'hand corner to close this window</center>');
  win.document.write('<p>Here are the lgroup diagrams '+
    'for the above inequalities:');
  for (var i=0; i<inequations.length; i=i+1){
    win.document.write("<p><b>"+(i+1)+". &nbsp; "+e2s(inequations[i])+"</b><p>"+
       objToString(checkEquation(inequations[i])[1]));
  }
  win.document.write("</body></html>");
  win.document.close();  
}