/* ======================================================================
DESC: 	This is the collection of functions for use in derivations.

PLATFORMS:

USAGE NOTES:
====================================================================== */

/* ======================================================================
FUNCTION:

INPUT:

RETURNS:

DESC:
====================================================================== */

// This is the test of a justification.
function checkJ(value,n) {
	v1=value; n1=n; elmtFocus=''
	setTimeout("checkJ1(v1,n1)",1)
	if (window.status.indexOf("the justification")>-1) window.status=''
}

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.  Something like \'1,2 >E\' or \'1 &E\' or \'3-4 ~I\'.  But NOT: \'1,2, >E\'; in this latter, the second comma will not be understood.")

 }
  else {
   numplus = num + '-,'; stopX = false
   for ( var i=0; i<value.length-2; i++ ) {
   	if ( numplus.indexOf(value.charAt(i)) < 0 ) {
   	stopX = true
   	break;
		}
	}
   if ( stopX ) {
   	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 >E\' or \'1 &E\' or \'3-4 ~I\'. But NOT: \'3&5 >E\' 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 ) {
	alertX('Check your rule name. ' + rl + ' is not in our set of rules.')
	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 == '=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') && (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' ) {
		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, ""); alertX('You need to cite from a subderivation.')
	}
   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 window.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){
// additions for tracking and records...
wrongLine = false; replace = false // to reset these values
//end of additions
	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 == '' || th.substring(th.length-3,th.length) == '...' ) {}
else {
	document.der.elements['j'+(n+1)].focus()
 if ( level[j1[n]] > l || level[j2[n]] > l || level[j3[n]] > l  ) {
   wrong('j',n,"");
   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)
   		alertX("The premise must be a grammatically correct sentence.<p>And it must be entered in the first sentence column.");
	}

}
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' ) { // What is this???????????????
		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 = ''
				}
			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)
   alertX("The assumption must be a grammatically correct sentence.")
	}
	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,'')
   			alertX("You must cite a terminated subderivation.")
			}
		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 ( !isSL(th) ) {
   wrong('s',n,l)
   alertX("Your entry must be a grammatically correct sentence of SL.")
	}
	
else if ( rl == '&E' ) {
   if ( j2[n] != null || mainConn(thm[j1[n]]) != '&') {
    wrong('s',n,l); wrong('j',n,'');
    alertX('For &E, you need to cite a single sentence with main connective \'&\'.')
	}
	else if ( th != dropParen(thm[j1[n]].substring(0,p)) && th != dropParen(thm[j1[n]].substring(p+1)) ) {
   wrong('s',n,l); alertX('You need to write one of the two <i>immediate</i> components of the cited sentence,<blockquote>' + thm[j1[n]] + '</blockquote>at line ' + j1[n] + '.')
	}}
	
else if ( rl == '&I' && j2[n] != null && j3[n] == null ) {
   if ( mainConn(th) != '&' ) {
   wrong('s',n,l)
   alertX('The entered expression<blockquote>' + th + '</blockquote>does not have main connective \'&\'.<p>It must for &I.')
}
  else {
   var c1 = th.substring(0,p); var c2 = th.substring(p+1);
   var d1 = dropParen(c1); var d2 = dropParen(c2);
   if ( ( mainConn(d1) != null && mainConn(d1) != '~' && !out(c1) ) || ( mainConn(d2) != null && mainConn(d2) != '~' && !out(c2) ) ) {
   		wrong('s',n,l);
   		alertX("The entered expression, \'" + th + "\' is missing parentheses")
}
	else {
   if ( !( d1 == thm[j1[n]] && d2 == thm[j2[n]] ) && !( d2 == thm[j1[n]] && d1 == thm[j2[n]] ) ) {
   wrong('s',n,l); alertX('Given your justification,<blockquote>' + j1[n] + ',' + j2[n] + ' &I</blockquote>you need to conjoin \'' + thm[j1[n]] + '\' with \''+ thm[j2[n]] + '\'.')
		}
	}
 }
}

else if ( rl == '>I' ) {
   x = j1[n]; Start = parseInt(x.substring(0,x.indexOf('-'))); stopX = parseInt(x.substring( x.indexOf('-') + 1 ));
	if ( term[Start-1] && term[stopX+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] != stopX && subs[level[n]+1] < n ) {
		termQ(Start,stopX+1,n)
		document.der.elements['j'+(n+1)].focus()
		}
	if ( (th.charAt(0) != '/' && mainConn(th) != '>' ) ) {
		wrong('s',n,l)
		alertX('Does your sentence you just entered on line ' + n + ' have horseshoe as its main connective?')
		}
	else if (x.indexOf('-')<0 || isNaN(Start) || isNaN(stopX) || j2[n] != null || subT[Start] != stopX ){
		wrong('s',n,l) ;wrong('j',n,''); alertX('There is someting wrong here.<p>Have you correctly cited an appropriate subderivation?')
		}
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[stopX] != c1 ) {
   	wrong('s',n,l);
   	alertX('For >I of \'' + th + '\', the subderivation must assume its antecedent and end with its consequent.<TABLE align="center" border="1"><tr><td><TABLE border="0"><TR><TD><IMG src="pix/subd.jpg" width="9" height="60" align="top"></TD><TD>'+a1+'<BR><BR><BR>'+c1+'</TD></TR><TR align="center"><TD colspan="2"><IMG src="pix/down.gif" width="14" height="21"  border="0"></TD></TR><TR><TD colspan="2">'+a+'<FONT face="Logic">&gt;</FONT>'+c+'</TD></TR></TABLE></TD></TR></TABLE>')
		}
	  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); alertX('Your sentence \'' + h + '\' does not have horseshoe as its main connective.<p>Did you really mean for this to be <font family="Logic">></font>E?')
	}
	else if ( th != dropParen(h.substring(p+1) )  && th == dropParen(h.substring(0,p)) ){
			wrong('s',n,l)
			alertX('You are using <font family="Logic">></font>E in the wrong "direction"!<p>\'' + th +'\' needs to be an input rather than output.')
		}
			else if ( th != dropParen(h.substring(p+1) ) || dropParen(h.substring(0,p)) != a ) {
		wrong('s',n,l)
		alertX('Your answer does not fit the form for <font family="Logic">></font>E.<TABLE border="1" align="center"><TR><TH colspan="2"><FONT face="Logic">&gt;</FONT>E</TH></TR><TR align="center"><TD>input 1:<BR>input 2:<BR><IMG src="empty.gif" width="1" height="21" border="0"><BR>output: </TD><TD><SPAN class="variable">P</SPAN> <FONT face="Logic">&gt;</FONT><SPAN class="variable">Q</SPAN><BR><SPAN class="variable">P</SPAN><BR><IMG src="pix/down.gif" width="14" height="21" border="0"> <BR><SPAN class="variable">Q</SPAN></TD></TR></TABLE>')
	}
}
else if ( rl == 'vI' ) {
   if ( j2[n] != null ) {
	   wrong('j',n,'');wrong('s',n,l)
	   alertX("Cite only one line for vI.")
   }
   else if (!isSL(th)) { wrong('s',n,l);alertX('You need to enter a grammatically correct sentence of SL.')}
   else if ( mainConn(th) != 'v' ) {
   	wrong('s',n,l);alertX('You need to enter a sentence with wedge as main connective.')
		}
	else {
	var p1 = th.substring(0,p); var p2 = th.substring(p+1)
	var c1 = dropParen(p1); var c2 = dropParen(p2)
	if ( !( c1 == thm[j1[n]] && isSL(c2) ) && !( c2 == thm[j1[n]] ) && isSL(c1) ) {
   	wrong('s',n,l); alertX('The entered sentence must have \'' + thm[j1[n]] + '\' as one disjunct. Make sure that you are following this form:<TABLE align="center" border="1" class="display"><TR><TH colspan="4">vI</TH></TR><TR align="center"><TD rowspan="3">input:<BR><BR>output:</TD><TD align="center" rowspan="3"><SPAN class="variable">P</SPAN><BR><IMG src="pix/down.gif" width="14" height="21"><BR><SPAN class="variable">P</SPAN>v<SPAN class="variable">Q</SPAN></TD><TD align="center" rowspan="3"> or</TD><TD align="center" rowspan="3"><SPAN class="variable">Q<BR></SPAN> <IMG src="pix/down.gif" width="14" height="21"><BR><SPAN class="variable">P</SPAN>v<SPAN class="variable">Q</SPAN></TD></TR><TR align="center"></TR><TR align="center"></TR></TABLE>')
			}
		else if ( ( mainConn(c1) != null && mainConn(c1) != '~' && !out(p1) ) || ( mainConn(c2) != null && mainConn(c2) != '~' && !out(p2) ))  {
   	wrong('s',n,l); alertX('You need some parentheses to make this a sentence.')
}}}
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]
   	stopX = false; break;
			}
		else {
   		stopX = true
			}
		}
	if ( stopX ) {
   	  wrong('s',n,l);alertX(d + " should be a disjunction, i.e., 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 ( a1 != d1 || a2 != d2 || c1 != c2 || c1 != th) {
   		wrong('s',n,l);alertX('The form seems to be incorrect for \'vE\'. Try:<TABLE border="1" align="center" class="display"><TR><TH colspan="2">vE</TH></TR><TR align="center"><TD>input 1:<BR>input 2:<BR>input 3: <BR><IMG src="empty.gif" width="1" height="21"><BR>output: </TD><TD><SPAN class="variable">P</SPAN>v<SPAN class="variable">Q</span><BR><SPAN class="variable">P</SPAN><FONT face="Logic">&gt;</FONT><SPAN class="variable">R</SPAN><BR><SPAN class="variable">Q</SPAN><FONT face="Logic">&gt;</FONT><SPAN class="variable">R</SPAN><BR><IMG src="pix/down.gif" width="14" height="21"><BR><SPAN class="variable">R</SPAN></TD></TR></TABLE>');
		}
		}
		}

}
else if ( rl == '~E' ) {
   var x = j1[n]; var Start = parseInt(x.substring(0,x.indexOf('-'))); var Stopp = parseInt(x.substring( x.indexOf('-') + 1 ));
	if ( term[Start-1] && term[Stopp+1] ) {
		wrong('s',n,l); wrong('j',n,'');
		alertX("The cited subderivation is not accessible.")
		}
	else if (  subT[Start] != Stopp && subs[level[n]+1] < n ) {
		termQ(Start,Stopp+1,n)
		document.der.elements['j'+(n+1)].focus()
		}
	else if ( x.indexOf('-')<0 || isNaN(Start) || isNaN(Stopp) || j2[n] != null || subT[Start] != Stopp ){
		wrong('s',n,l); wrong('j',n,''); }
	else 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 stopX = true; var thmE = thm[Stopp]; var c = mainConn(thmE)
	 	negEP = ( !out(thmE) && c != null && c != '~' ) ? '~(' + thmE + ')' : '~' + thmE ;
	 	negEB = ( !out(thmE) && c != null && c != '~' ) ? '~[' + thmE + ']' : '~' + thmE ;
	 	for ( var i=Stopp-1; i>=Start; i-- ) {
			if (level[i]!=level[Start]) continue
	 	 if ( thm[i] == negEP || thm[i] == negEB ) {
   	  stopX = 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 ) {
	 	   stopX = false; break; }
		}
	 }
	 	if ( stopX ) {
   		wrong('s',n,l)
	 		alertX('I can\'t find the opposite of line ' + Stopp + ' anywhere in the cited subderivation.')
		}
 }
}

else if ( rl == '~I' ) {
   var x = j1[n]; var Start = parseInt(x.substring(0,x.indexOf('-'))); var Stopp = parseInt(x.substring( x.indexOf('-') + 1 ));
	if ( term[Start-1] && term[Stopp+1] ) {
		wrong('s',n,l); wrong('j',n,'');
		alertX("The cited subderivation is not accessible.")
		}
	else if (  subT[Start] != Stopp && subs[level[n]+1] < n ) {
		termQ(Start,Stopp+1,n)
		document.der.elements['j'+(n+1)].focus()
		}
	else if ( x.indexOf('-')<0 || isNaN(Start) || isNaN(Stopp) || j2[n] != null || subT[Start] != Stopp ){
		wrong('j',n,''); wrong('s',n,l);}
	else if ( mainConn(th) != '~' || thm[Start] != dropParen( th.substring(1) )   ) {
   wrong('s',n,l);
   alertX("For Negation Introduction, the sentence on line " + n + " needs to be the negation of the assumption of line " + Start + ".");
}
	 else {
	 	var stopX = true; var thmE = thm[Stopp]; var c = mainConn(thmE)
	 	negEP = ( !out(thmE) && c != null && c != '~' ) ? '~(' + thmE + ')' : '~' + thmE ;
	 	negEB = ( !out(thmE) && c != null && c != '~' ) ? '~[' + thmE + ']' : '~' + thmE ;
	 	for ( var i=Stopp-1; i>=Start; i-- ) {
			if (level[i]!=level[Start]) continue
	 	 if ( thm[i] == negEP || thm[i] == negEB ) {
   	  stopX = 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 ) {
	 	   stopX = false; break; }
			}
	 	}
	 	if ( stopX ) {
   		wrong('s',n,l)
	 		alertX('I can\'t find the opposite of line ' + Stopp + ' anywhere in the cited subderivation.')
		}
 	}
}
else if ( rl == '=I' ) {
   if (j3[n] != null || j2[n] == null ) {
		wrong('j',n,''); wrong('s',n,l); alertX('You need to cite two line numbers for <font family="Logic">=</font>I.')
		}
		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); alertX('Your entry on line number ' + j1[n] + ' needs to have main connective horseshoe to fit the pattern:<TABLE border="1" align="center" class="display"><TR><TH colspan="2"><FONT face="Logic">=</FONT>I</TH></TR><TR align="center"><TD>input 1:<BR>input 2:<BR><IMG src="empty.gif" width="1" height="21"><BR>output: </TD><TD><SPAN class="variable">P</SPAN><FONT face="Logic">&gt;</FONT><SPAN class="variable">Q</span><BR><SPAN class="variable">Q</SPAN><FONT face="Logic">&gt;</FONT><SPAN class="variable">P</SPAN><FONT face="Logic"></FONT><BR><IMG src="pix/down.gif" width="14" height="21"> <BR><SPAN class="variable">P</SPAN><FONT face="Logic">=</FONT><SPAN class="variable">Q</SPAN></TD></TR></TABLE>')
	}
	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); alertX('The sentence on line number ' + j2[n] + ' needs to have main connective horseshoe to fit the pattern:<TABLE border="1" align="center" class="display"><TR><TH colspan="2"><FONT face="Logic">=</FONT>I</TH></TR><TR align="center"><TD>input 1:<BR>input 2:<BR><IMG src="empty.gif" width="1" height="21"><BR>output: </TD><TD><SPAN class="variable">P</SPAN><FONT face="Logic">&gt;</FONT><SPAN class="variable">Q</span><BR><SPAN class="variable">Q</SPAN><FONT face="Logic">&gt;</FONT><SPAN class="variable">P</SPAN><FONT face="Logic"></FONT><BR><IMG src="pix/down.gif" width="14" height="21"> <BR><SPAN class="variable">P</SPAN><FONT face="Logic">=</FONT><SPAN class="variable">Q</SPAN></TD></TR></TABLE>')}
		else {
   	   var a2 = dropParen(cite[1].substring(0,p)); var c2 = dropParen(cite[1].substring(p+1));
			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);
					if (!isSL(th)) alertX(th + ' is not a sentence of SL.')
   				else  alertX('The bicomponents of the sentence you entered need to correspond to the antecedents and consequents of your two inputs.<p>Try to fit the pattern<TABLE border="1" align="center" class="display"><TR><TH colspan="2"><FONT face="Logic">=</FONT>I</TH></TR><TR align="center"><TD>input 1:<BR>input 2:<BR><IMG src="empty.gif" width="1" height="21"><BR>output: </TD><TD><SPAN class="variable">P</SPAN><FONT face="Logic">&gt;</FONT><SPAN class="variable">Q</span><BR><SPAN class="variable">Q</SPAN><FONT face="Logic">&gt;</FONT><SPAN class="variable">P</SPAN><FONT face="Logic"></FONT><BR><IMG src="pix/down.gif" width="14" height="21"> <BR><SPAN class="variable">P</SPAN><FONT face="Logic">=</FONT><SPAN class="variable">Q</SPAN></TD></TR></TABLE>')
				}
			}
	else {
		wrong('s',n,l)
		if (!isSL(th)) alertX(th + ' is not a sentence of SL.')
   	else alertX('To derive \''+th+'\', the two conditionals you cite need to be of the forms<p>&nbsp;&nbsp;<SPAN class="variable">P</SPAN><FONT face="Logic">&gt;</FONT><SPAN class="variable">Q</span><p>and<p>&nbsp;&nbsp;<SPAN class="variable">Q</SPAN><FONT face="Logic">&gt;</FONT><SPAN class="variable">P</span>.')
	}
 }
}	}}
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);alertX('For <font family="Logic">=</font>E, one of your input sentences (on line '+j1[n]+' or line '+j2[n]+ ') needs to have main connective <font family="Logic">=</font>.')
	}
	else {
   	var b1 = dropParen(b.substring(0,p)); var b2 = dropParen(b.substring(p+1));
   	if ( !(b1 == c && b2 == th) && !( b1 == th && b2 == c ) ) {
   		wrong('s',n,l); alertX('Careful, you need to precisely follow this form:<p><TABLE align="center" border="1" class="display"><TR><TH colspan="4"><FONT face="Logic">=</FONT>E</TH></TR><TR align="center"> <TD rowspan="3">input 1:<BR>input 2:<BR><IMG src="empty.gif" width="1" height="21"><BR>output: </TD><TD align="center" rowspan="3"><SPAN class="variable">P</SPAN><FONT face="Logic">=</FONT><SPAN class="variable">Q<BR>P<BR><IMG src="pix/down.gif" width="14" height="21"> <BR>Q</SPAN></TD><TD align="center" rowspan="3"> or</TD><TD align="center" rowspan="3"><SPAN class="variable">P</SPAN><FONT face="Logic">=</FONT><SPAN class="variable">Q<BR>P<BR><IMG src="pix/down.gif" width="14" height="21"> <BR>Q</SPAN></TD></TR><TR align="center"> </TR><TR align="center"> </TR></TABLE>')
		}
  	}
}

else if ( rl == 'R' ) {
	if ( j2[n] != null ) {
   	wrong('s',n,l);wrong('j',n,''); alertX('You need to cite exactly one line number for reiteration.')
	}
   if ( th != thm[j1[n]] ) {
   	wrong('s',n,l); alertX('Careful, this is not a precise reiteration.')
	}
}
//for SD+
else if ( plus == true ) {
   checkPlus(th,n,l,rl)
}
else { wrong('s',n,l);wrong('j',n, "");}
}}
	// additions for window.status, tracking and records...
// Now final judgments are made. replace == true means to leave the replace message ???
if (!replace &&  th.charAt(th.length-1) != '?' && th != '') 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)
	}
//end of additions
}