/* ___________________________________________________

derivationFill.js

DESC: 	This is the collection of functions for use in derivations.
						SL DERIVATIONS ONLY
______________________________________________________ */

//sets timeout for ie5
function checkJ(value,n) {
	v1=value; n1=n; elmtFocus=''
	setTimeout("checkJ1(v1,n1)",1)
	if (window.status.indexOf("the justification")>-1) window.status=''
}
// This is the test of a justification.
function checkJ1(value,n) {
	value =  deSpace(value.toUpperCase()); 
	var ll = value.length
	var valL = value.charAt(ll -1); var valSL = value.charAt(ll -2)
	if ( valSL == '7' && (valL == 'I' || valL == 'E') ){
   	value = value.substring(0,ll-2) + '&' + valL
	}
for ( var i=0; i<ll; i++ ) {
	var valu = value.charAt(i)
   	if (  valu== 'V' ) {
   		value = value.substring(0,i) + 'v' + value.substring(i+1)
		}
   	else if ( valu == '`' ) {
   		value = value.substring(0,i) + '~' + value.substring(i+1)
		}
   	else if ( valu == '.' ) {
   		value = value.substring(0,i) + '>' + value.substring(i+1)
		}
	}
  document.der.elements["j"+n].value = value;
j[n] = value; var a = value.charAt(0);
 if ( a == 'P' ) {
     rule[n] = 'Premise';
     document.der.elements['j' + n].value = "Premise";
     document.der.elements['s' + n + '1'].focus();
 }
 else if ( value == '') {
 rule[n] = null
 thm[n] = null
 document.der.elements['s' + n + level[n] ].value = ''
     for (var i = n+1; i<=derLength; i++) { // check dependence for an empty theorem...
          if ( thm[i] != null && thm[i] != '' && ( between(n,j1[i]) || between(n,j2[i]) || between(n,j3[i]) ) ) {
               document.der.elements['s'+i+level[i]].value += '??'
               thm[i]='?'
				}
		}
 }
else if ( value.charAt(value.length-1) == '?' ) {}
 else if (  a == 'A' ) {
 	  rule[n] = 'Assumption'; level[n] = level[n-1] + 1;
     document.der.elements['j' + n].value = "Assumption";
	document.der.elements['s' + n + level[n-1] ].value = "....what if?..............................................."
     document.der.elements['s' + n + (level[n-1] + 1) ].focus();
 }
 else if ( num.indexOf(value.charAt(0))<0 ) {
 	wrong("j", n, "")
   alertX("You need to give a line number to begin the current justification.")
} 
 else if ( num.indexOf(value.charAt(j[n].length-3)) < 0 ) {
 	wrong('j',n, "");
   alertX("You need to give a proper justification: a line number, or line numbers separated by commas, or a range of numbers; and this followed by the rule name.<p>Something like \'1,2 MP\' or \'1 &E\' or \'3-4 RD\'.  But NOT: \'1,2, MP\'; in this latter, the second comma will not be understood.")
 }
  else {
   numplus = num + '-,'; stop = false
   for ( var i=0; i<value.length-2; i++ ) {
   	if ( numplus.indexOf(value.charAt(i)) < 0 ) {
   	stop = true
   	break;
		}
	}
   if ( stop ) {
	wrong('j',n, "");
   alertX("You need to give a proper justification: a line number, or line numbers separated by commas, or a range of numbers; and this followed by the rule name.  Something like \'1,2 MP\' or \'1 &E\' or \'3-4 RD\'. But NOT: \'3&5 MP\' or \'3# &E\' or the like.")
}
	else   {
		if ( value.charAt(value.length-1) == 'R' && value.charAt(value.length-2)!='T' ) {
   		rule[n] = 'R'; var rl = 'R'
   		value = value.substring(0,value.length-1) + ' R' 
}
		else {
	var rl = value.substring(value.length-2)
   rule[n] = rl ;
}
if ( rules.indexOf(rl)<0 ) wrong('j',n, "");
else {
   var js = value.substring(0, value.length-2);
   var jArray = js.split(',');
   j1[n] = jArray[0]; j2[n] = jArray[1]; j3[n] = jArray[2];
 
   if ( j1[n] >= n || j2[n] >= n || j3[n] >= n ) {
    wrong('j',n, "");alertX("You need to cite line numbers less than the number of the current line.");
   }
   else if ( term[j1[n]] || term[j2[n]] || term[j3[n]]) {
    wrong('j',n, "");alertX("A line number cited is not accessible, it is in a terminated (sub)derivation.");
   }
   else if ( (rl == '&E' || rl  == 'vI') && (j2[n] != null || isIn('-',j1[n]))) {
               wrong('j',n,'')
               alertX("You need to cite one individual line for " + rl)
   }
          else if ( (rl == 'MP' || rl == '>E' || rl == '=E' || rl == '&I' || rl == '=I' || rl == 'DS' || rl == 'MT' || rl == 'HS' ) && (j2[n] == null || j3[n] != null) ) {
               wrong('j',n,'')
               alertX("You need to cite two lines for " + rl + ".")
          } 
		else if ( (rl == 'MP' || rl == '>E' || rl == '=E' || rl == '&I' || rl == '=I' ) && (j2[n] == null || j3[n] != null) ) {
			wrong('j',n,'')
			alertX("You need to cite two lines for " + rl)
		} 
		else if ( (rl == 'vE' ) && (j3[n] == null || j1[n].indexOf('-')>-1 || j2[n].indexOf('-')>-1 || j3[n].indexOf('-')>-1 ) ){
			wrong('j',n,'')
			alertX("You need to cite three individual lines for vE")
		} 
		else if ( (rl == '>I' || rl == '~I' || rl == '~E' || rl == 'RD') && (j1[n].indexOf('-')<0 || j2[n] != null) ) {
			wrong('j',n, '')
			alertX("For " + rl + " you need to cite a single subderivation, something of the form \'a - b\'.")
		}
else {
   if ( value.substring(value.length-2)!=' R' ) {
   value = value.substring(0,value.length-2) + ' ' + 	value.substring(value.length-2);
   }
 	document.der.elements["j"+n].value = value;

   
   if ( rl == '>I' || rl == '~I' || rl == '~E' || rl == 'RD') {
		var ls = level[j1[n].substring(0,j1[n].indexOf('-'))]
   	level[n] = ( ls > 1 ) ? ls - 1 : level[n-1];
	}
		else {
   		level[n] = level[n-1];
		}
	if ( level[n] < 1 ) {
  	 wrong('j',n, "");
	}
   document.der.elements["s"+n+level[n]].focus()
		}
  }
 }
}}

// Here begins the test of a line for theoremhood.
subs = new Array; subT = new Array; term = new Array; thm = new Array;
var cmp1; var cmp2; var replace = false // replace is true just in case we want to leave the "replace and erase question marks" message on status.
function checkL(value,n,l) {
	var1=value; num1=n;limp=l;elmtFocus=''
	if (value.substring(value.length-3,value.length) != '...' ) setTimeout("checkL2(var1,num1,limp)",1)
}
var wrongLine
function checkL2(value, n, l){
	wrongLine = false; replace = false // to reset these values
	checkDependence(n,l,derLength)
	level[n] = l;  var rl = rule[n]
	value = deSpace(value.toUpperCase()); 
	value = dropParen(rewrite(value))
	document.der.elements['s'+n+l].value = value;
	thm[n] = value; var th = value
if ( th.charAt(th.length-1) == '?' || th == '' ) {}
else {
	document.der.elements['j'+(n+1)].focus()
 if ( level[j1[n]] > l || level[j2[n]] > l || level[j3[n]] > l  ) {
   wrong('j',n,"");wrong('s',n,l);
   alertX("One of the lines cited is not accessible.");
}
else if ( thm[n] == "'" ) {
	if ( rl == 'Assumption' && typeof goal == 'string' && goal.charAt(0)!= '*' && goal.indexOf('!')==-1 ) {
		var mcon = mainConn(goal), asm // main connective of goal and appropriate assumption
		if (mcon == '>') asm = goal.substring(0,p)
		else if (mcon == '~') asm = goal.substring(1)
		else asm = (mcon != null) ? '~(' + goal + ')' :'~' + goal
		document.der.elements['s' + n + l].value = asm;
		checkL(asm, n, l)
		}
	else if ( thm[j1[n]] == null) {wrong('s',n,l)}
	else {
		var y = thm[j1[n]]
		document.der.elements['s' + n + l].value = y;
		checkL(y, n, l)
		}
	}
else if ( rl == 'Premise' ) {
   if ( l != 1 || !isSL(th) ) {
   wrong('s',n,l);
	}

}
else if ( rl == 'Assumption' ) {
   if ( l == 1 ) {
		wrong('s',n,l);
		alertX("An assumption must be within a subderivation: this entry must be in the next column to the right.");
	}
	else if ( th == '*' || th == '8' ) {
		if ( !term[n] && subT[n] != null ) {
			alertX("This trick only works for terminated subderivations...")
			wrong('s',n,l)
			}
		else {
		var eend = subT[n]
		for (var i=n;i<=eend;i++) {
			term[i]=false
			thm[i]= null
			document.der.elements['s'+i+l].value = ''
				var ppos = '' + (l-1) // ppos is the level -1 so that we erast the "then..."
			if (i>n) {
				document.der.elements['j'+i].value = ''
				document.der.elements['s'+i+ppos].value = ''
				for (var k=l;k<=derWidth;k++) document.der.elements['s'+i+k].value = ''
				}
			j[i]=null
			j1[i]=null
			j2[i]=null
			j3[i]=null
			}
		subT[n]=null
		document.der.elements['s'+n+l].focus()
		}
	}
	else if ( !isSL(th) ) {
   wrong('s',n,l);
	}
	else { 
		if ( subs[l] != null && subs[l] != n ) {
   	var y = termQ(subs[l],n,n);
   		if ( y == null ) {
   			wrong('s',n,l);wrong('j',n,'')
			}	
		else {subs[l] = n;document.der.elements['j'+(n+1)].focus()}
		}
		else {subs[l] = n;document.der.elements['j'+(n+1)].focus()}
	}
}
 
else {
 if ( l < level[n-1] && thm[n-1]!=null ) {  //In case one moves to the left of a "live" sentence.
   y = termQ(subs[level[n-1]],n,n);
   document.der.elements['j'+(n+1)].focus()
}
if (th.charAt(0)!='/' && !isSL(th)) {wrong('s',n,l); alertX(th + ' is not a sentence of SL.')}

else if ( rl == '&E' ) {
   if ( j2[n] != null || mainConn(thm[j1[n]]) != '&') {
    wrong('s',n,l); wrong('j',n,'');
	}
	else {
	ans = dropParen(thm[j1[n]].substring(0,p)); ans2 = dropParen(thm[j1[n]].substring(p+1))
	if ( th == '/' ) {th = ans; thm[n]= ans; document.der.elements['s' + n + l].value = ans }
	else if ( th == '//' ) {th = ans2; thm[n]= ans2; document.der.elements['s' + n + l].value = ans2 }
	else if ( th != ans && th != ans2) {
   wrong('s',n,l);
	}}
}
else if ( rl == '&I' && j2[n] != null && j3[n] == null ) {
	th1 = thm[j1[n]] ; th2 = thm[j2[n]] ; var th1a=th1; var th2a = th2
	if ( biC.indexOf(mainConn(th1)) >-1 ) { th1 = '(' + th1 + ')'; th1a = '[' + thm[j1[n]] + ']'} // add parens and brackets as needed
	if ( biC.indexOf(mainConn(th2)) >-1 ) { th2 = '(' + th2 + ')'; th2a = '[' + thm[j2[n]] + ']'}
	ans = th1 + '&' + th2; ans2 = th2 + '&' + th1; ans1a = th1a + '&' + th2a; ans2a = th2a + '&' + th1a; ans1b = th1 + '&' + th2a; ans2b = th2 + '&' + th1a; ans1c = th1a + '&' + th2; ans2c = th2a + '&' + th1 // the possible answers
	if ( th == '/' )  {th = ans; thm[n]= ans; document.der.elements['s' + n + l].value = ans }
	else if ( th == '//' )  {th = ans2; thm[n]= ans2; document.der.elements['s' + n + l].value = ans2 }
  	else if ( mainConn(th) != '&' ) {
   	wrong('s',n,l)
   	alertX("The sentence entered does not have main connective \'&\'.")
	}	
	else if ( th != ans && th != ans2 &&  th != ans1a && th != ans2a && th != ans1b && th != ans2b && th != ans1c && th != ans2c  ) {
   	wrong('s',n,l)
	}
}

else if ( rl == '>I' ) {
   x = j1[n]; Start = parseInt(x.substring(0,x.indexOf('-'))); Stop = parseInt(x.substring( x.indexOf('-') + 1 ));
	if ( term[Start-1] && term[Stop+1] ) {
		wrong('s',n,l); wrong('j',n,'');
		alertX("The cited subderivation is not accessible.")
		}
	else if ( rule[Start] != 'Assumption' ) {
		wrong('s',n,l); wrong('j',n,'');
		alertX("Line " + Start + " is not an assumption.")
		}
	else {
	if (  subT[Start] != Stop && subs[level[n]+1] < n ) {
		termQ(Start,Stop+1,n)
		document.der.elements['j'+(n+1)].focus()
		}
	if ( (th.charAt(0) != '/' && mainConn(th) != '>' )|| x.indexOf('-')<0 || isNaN(Start) || isNaN(Stop) || j2[n] != null ){
		wrong('s',n,l) ;wrong('j',n,'')
		}
	else if ( subT[Start] != Stop ) {
		wrong('s',n,l) ;wrong('j',n,'');
		alertX('Check to make sure you have cited a subderivation.<P>You wrote '+ Start + '-' + Stop + '. Is ' + Start + ' the first line of the subderivation? and ' + Stop + ' its last?')
		}
	else if ( th == '/' || th == '//' ) {
	a = (mainConn(thm[Start]) != null && mainConn(thm[Start]) != '~') ? '(' + thm[Start] + ')' : thm[Start]
	c = (mainConn(thm[Stop]) != null && mainConn(thm[Stop]) != '~') ? '(' + thm[Stop] + ')' : thm[Stop]
	ans = a + '>' + c;
	th = ans; thm[n]= ans; document.der.elements['s' + n + l].value = ans }
else {
	var a = th.substring(0,p); var c = th.substring(p+1);
	var a1 = dropParen(a); var c1 = dropParen(c)
	  if ( thm[Start] != a1 || thm[Stop] != c1 ) {
   	wrong('s',n,l);
   	alertX("For >I, the subderivation must assume the antecedent of  " + th + " and end with its consequent.")
		}
	  else {
	   if ( ( mainConn(a1) != null && mainConn(a1) != '~' && !out(a) ) || ( mainConn(c1) != null && mainConn(c1) != '~' && !out(c) ) ) {
   	 wrong('s',n,l);
   	 alertX("Check parentheses in " + th + ".")
}}}}}

else if ( (rl == '>E' || rl == 'MP')&& j2[n] != null && j3[n] == null ) {
   var h = (thm[j1[n]].length > thm[j2[n]].length) ? thm[j1[n]] : thm[j2[n]];
   var a = (thm[j1[n]].length > thm[j2[n]].length) ? thm[j2[n]] : thm[j1[n]];
   if ( mainConn(h) != '>'  ) {
   	wrong('j',n,'');wrong('s',n,l);	}
	else {
	ans = dropParen(h.substring(p+1) )
	if ( th == '/' || th == '//' ) {th = ans; thm[n]= ans; document.der.elements['s' + n + l].value = ans }
	if ( th != ans || dropParen(h.substring(0,p)) != a ) {
		wrong('s',n,l)
	}	
	}
}
else if ( rl == 'vI' ) {
   if ( j2[n] != null || (mainConn(th) != 'v' && th.charAt(0) != '/')) {
   	wrong("s",n,l); wrong('j',n,'');
		}
	else {
	th1 = thm[j1[n]]
		if ( th.charAt(0) == '/' ) {
  		 	thP = ( biC.indexOf(mainConn(th1))>-1 ) ?  '(' + th1 + ')' : th1
			if ( th == '/' )  {document.der.elements['s' + n + l].value = thP + 'v?_?'; document.der.elements['s' + n + l].focus()}
   		else if ( th == '//' ) { document.der.elements['s' + n + l].value =  '?_?v' + thP; document.der.elements['s' + n + l].focus()}
   		else {wrong('s',n,l)}
		}
		else {
			var p1 = th.substring(0,p); var p2 = th.substring(p+1)
			var c1 = dropParen(p1); var c2 = dropParen(p2)
			if ( !( c1 == th1 && isSL(c2) ) && !( c2 == th1 ) && isSL(c1) ) {wrong('s',n,l); 	}
			else if ( ( mainConn(c1) != null && mainConn(c1) != '~' && !out(p1) ) || ( mainConn(c2) != null && mainConn(c2) != '~' && !out(p2) )) {wrong('s',n,l);}
}}}
else if ( rl == 'vE' && j3[n] != null ) {
   for ( var i=0; i<3; i++ ) {
   	cite = new Array (thm[j1[n]],thm[j2[n]],thm[j3[n]])
   	if ( mainConn(cite[i]) == 'v' ) {
   	var d = cite[i]; var d1 = dropParen(cite[i].substring(0,p)); var d2 = dropParen(cite[i].substring(p+1))
   	var h1 = (mainConn(cite[(i+1)%3]) == ">" && dropParen(cite[(i+1)%3].substring(0,p)) == d1) ? cite[(i+1)%3] : cite[(i+2)%3];
   	var h2 = (h1 == cite[(i+1)%3]) ? cite[(i+2)%3] : cite[(i+1)%3]
   	stop = false; break;
			}
		else {
   		stop = true
		}		

		}
	if ( stop ) {
   	  wrong('s',n,l);alertX("One cited sentence should be a disjunction, i.e.,  its main connective should be \'v\'.");
		}
	else {
   	if ( mainConn(h1) != ">" || mainConn(h2) != ">" ) {
   		wrong('s',n,l);alertX(c + " should be a conditional, i.e., main connective should be \'>\'.");
		}
		else {
   		var a1; mainConn(h1); a1 = dropParen(h1.substring(0,p)); c1 = dropParen(h1.substring(p+1))
   		var a2; mainConn(h2); a2 = dropParen(h2.substring(0,p)); c2 = dropParen(h2.substring(p+1))
   		if ( th == '/' || th == '//' ) {th = c1; thm[n]= c1; document.der.elements['s' + n + l].value = c1 }
   		if ( a1 != d1 || a2 != d2 || c1 != c2 || c1 != th) {
   			wrong('s',n,l);alertX("The form seems to be incorrect for \'vE\'.");
			}
		}
		}
	
}
else if ( rl == '~E' ) {
   var x = j1[n]; var Start = parseInt(x.substring(0,x.indexOf('-'))); var Stop = parseInt(x.substring( x.indexOf('-') + 1 ));
	if ( term[Start-1] && term[Stop+1] ) {
		wrong('s',n,l); wrong('j',n,'');
		alertX("The cited subderivation is not accessible.")
		}
	else if (  subT[Start] != Stop && subs[level[n]+1] < n ) {
		termQ(Start,Stop+1,n)
		document.der.elements['j'+(n+1)].focus()
		}
	else if ( x.indexOf('-')<0 || isNaN(Start) || isNaN(Stop) || j2[n] != null || subT[Start] != Stop ){
		wrong('s',n,l); wrong('j',n,''); }
	else {
	if ( th == '/' || th == '//' ) {th = dropParen(thm[Start].substring(1)); thm[n]= th; document.der.elements['s' + n + l].value = th }
	if ( mainConn(thm[Start]) != '~' || th != dropParen( thm[Start].substring(1)  ) ) {
   	wrong('s',n,l);
   	alertX("For Negation Elimination, ~E, on line " + Start + " you need to assume the negation of your goal, line " + n + ".");
	}
	 else {
	 	var stop = true; var thmE = thm[Stop]; var c = mainConn(thmE)
	 	negEP = ( !out(thmE) && c != null && c != '~' ) ? '~(' + thmE + ')' : '~' + thmE ;
	 	negEB = ( !out(thmE) && c != null && c != '~' ) ? '~[' + thmE + ']' : '~' + thmE ;
	 	for ( var i=Stop-1; i>=Start; i-- ) {
			if (level[i]!=level[Start]) continue
	 	 if ( thm[i] == negEP || thm[i] == negEB ) {
   	  stop = false; break;}
		 else {
	 	  var t = thm[i]; c = mainConn(t);
	 	  var tNP = ( !out(t) && c != null && c != '~' )? '~(' + t + ')' : '~' + t;
	 	  var tNB = ( !out(t) && c != null && c != '~' )? '~[' + t + ']' : '~' + t;
	 	  if ( thmE == tNP || thmE == tNB ) {
	 	   stop = false; break; }
		}	
	 }
	 	if ( stop ) {
   		wrong('s',n,l)
	 		alertX('I can\'t find the opposite of line ' + Stop + ' anywhere in the cited subderivation.')
		}
 	 
 }

}
}
else if ( rl == '~I' || rl == 'RD') {
   var x = j1[n]; var Start = parseInt(x.substring(0,x.indexOf('-'))); var Stop = parseInt(x.substring( x.indexOf('-') + 1 ));
	if ( term[Start-1] && term[Stop] ) {
		wrong('s',n,l); wrong('j',n,'');
		alertX("The cited subderivation is not accessible.")
		}
	else if (  subT[Start] != Stop && subs[level[n]+1] < n ) {
		termQ(Start,Stop+1,n)
		document.der.elements['j'+(n+1)].focus()
		}
	else if ( x.indexOf('-')<0 || isNaN(Start) || isNaN(Stop) || j2[n] != null || subT[Start] != Stop ){
		wrong('j',n,''); wrong('s',n,l);}
	else {	
	ans = ( biC.indexOf(mainConn(thm[Start])) >-1 ) ? '~(' + thm[Start] + ')' : '~' + thm[Start]
	if ( th == '/' || th == '//' ) {th = ans; thm[n]= th; document.der.elements['s' + n + l].value = th }
	if ( mainConn(th) != '~' || thm[Start] != dropParen( th.substring(1) )   ) {
   wrong('s',n,l);
   alertX("For RD, the sentence on line " + n + " needs to be the negation of the assumption of line " + Start + ".");
	}
	 else {
	 	var stop = true; var thmE = thm[Stop]; var c = mainConn(thmE)
	 	negEP = ( !out(thmE) && c != null && c != '~' ) ? '~(' + thmE + ')' : '~' + thmE ;
	 	negEB = ( !out(thmE) && c != null && c != '~' ) ? '~[' + thmE + ']' : '~' + thmE ;
	 	for ( var i=Stop-1; i>=Start; i-- ) {
			if (level[i]!=level[Start]) continue
	 	 if ( thm[i] == negEP || thm[i] == negEB ) {
   	  stop = false; break;}
		 else {
	 	  var t = thm[i]; c = mainConn(t);
	 	  var tNP = ( !out(t) && c != null && c != '~' )? '~(' + t + ')' : '~' + t;
	 	  var tNB = ( !out(t) && c != null && c != '~' )? '~[' + t + ']' : '~' + t;
	 	  if ( thmE == tNP || thmE == tNB ) {
	 	   stop = false; break; }
		}	
	 }
	 	if ( stop ) {
   		wrong('s',n,l)
	 		alertX('I can\'t find the opposite of line ' + Stop + ' anywhere in the cited subderivation.')
		}
 	 
 }
}}
else if ( rl == '=I' ) {
   if (j3[n] != null || j2[n] == null ) {
		wrong('j',n,''); wrong('s',n,l);
		}
		else {
		var cite = new Array; cite[0] = thm[j1[n]]; cite[1] = thm[j2[n]];
   if ( mainConn(cite[0]) != '>' ) {	
   	wrong('j',n,''); wrong('s',n,l);
	}
	else {
     var a1 = dropParen(cite[0].substring(0,p)); var c1 = dropParen(cite[0].substring(p+1));
		if ( mainConn(cite[1]) != '>' ) {wrong('j',n,''); wrong('s',n,l);}
		else {
   	   var a2 = dropParen(cite[1].substring(0,p)); var c2 = dropParen(cite[1].substring(p+1));
   	   if ( th == '/' )  {
   	   	a1P = (biC.indexOf(mainConn(a1))>-1) ? '(' + a1 + ')' : a1; a2P = (biC.indexOf(mainConn(a2))>-1) ? '(' + a2 + ')' : a2
   	   	th = a1P + '=' + a2P; thm[n]= th; document.der.elements['s' + n + l].value = th 
   	   }
   	   if (  th == '//' )  {
   	   	a1P = (biC.indexOf(mainConn(a1))>-1) ? '(' + a1 + ')' : a1; a2P = (biC.indexOf(mainConn(a2))>-1) ? '(' + a2 + ')' : a2
   	   	th = a2P + '=' + a1P; thm[n]= th; document.der.elements['s' + n + l].value = th 
   	   }
			if ( mainConn(th) == '=' && a1 == c2 && a2 == c1) {
   			var comp1 = dropParen(th.substring(0,p)); var comp2 = dropParen(th.substring(p+1));
   			if ( ((a1 == comp1 && a2 == comp2) || (a1 == comp2 && a2 == comp1)) && isSL(th) ) {
   			}
				else {
   			wrong('s',n,l);
				}
			}	
	else {
   	wrong('s',n,l);
	}
 }
}	}}
else if ( rl == '=E' && j2[n] != null && j3[n] == null ) {
	var b = (thm[j1[n]].length > thm[j2[n]].length) ? thm[j1[n]] : thm[j2[n]];
   var c = (thm[j1[n]].length > thm[j2[n]].length) ? thm[j2[n]] : thm[j1[n]];
   if ( mainConn(b) != '=') {
   	wrong('j',n,'');wrong('s',n,l);
	}
	else {
	var b1 = dropParen(b.substring(0,p)); var b2 = dropParen(b.substring(p+1));
		if ( th == '/' || th == '//') {
   		th = (b1==c) ? b2 : b1; thm[n]= th; document.der.elements['s' + n + l].value = th 
		}
   	if ( !(b1 == c && b2 == th) && !( b1 == th && b2 == c ) ) {
   		wrong('s',n,l);
		}
  	}
}

else if ( rl == 'R' ) {
	if (j1[n] == null || j2[n] != null ) {
   	wrong('j',n,'');wrong('s',n,l);
	}
	else if ( th == '/' || th == '//' )  {th = thm[j1[n]]; thm[n]= th; document.der.elements['s' + n + l].value = th }
   else if ( th != thm[j1[n]] ) {
   	wrong('s',n,l)
	}
}
//for SD+
else if ( plus == true ) {
   checkPlus(th,n,l,rl)
}
else { wrong('s',n,l);wrong('j',n, "");}
}}
// Now final judgments are made. replace == true means to leave the replace message ???
if (th.charAt(th.length-1) != '?' && thm[n]!=null) {
	if (!replace && th != '' && (th != '/' || rl == 'DS' || rl == 'HS' || rl == 'MT') ) top.window.status= (wrongLine) ? 'Problem: line ' + n + ' is NOT correct.' : 'Line ' + n + ' is correct.'
	if ( typeof getCookie == 'function' && !wrongLine && typeof goal == 'string') { // if all's gone ok with the step we get to this point and check to see if there's a goal that's been met...
		if ( l == 1 && goal == '*') checkContra(n,th,goal + goalLine) // looking for a contradiction
		if ( l == 1 && goal.charAt(0) == '!') checkEquiv(n,th)// looking to see that there are two derivations
		else if ( l == 1 && isSame(thm[n],goal) ) keepTrack(goal + goalLine) 
		}
	}
}