/*      
_______________________________________________________________
derivationPLI.js

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

// 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) {
	var rl
     value =  deSpace(value); 
     var ll = value.length
     var valL = value.charAt(ll -1); var valSL = value.charAt(ll -2)
     if ( valSL == '7' && (valL.toUpperCase() == 'I' || valL.toUpperCase() == 'E') ){
     value = value.substring(0,ll-2) + '&' + valL
     }
     if ( (valSL == '6' || valSL == 'V') && (valL.toUpperCase() == 'I' || valL.toUpperCase() == 'E') ){
     value = value.substring(0,ll-2) + '^' + valL
     }
     if ( (valSL == '5' || valSL == '3') && (valL.toUpperCase() == 'I' || valL.toUpperCase() == 'E') ){
     value = value.substring(0,ll-2) + '%' + valL
     }
	var valN = (value.charAt(ll-2) == 'v') ? 'v' : value.charAt(ll-2).toUpperCase()
	value = value.substring(0,ll-2).toUpperCase() + valN + valL.toUpperCase() // don't need the toUpperCase in first part???
for ( var i=0; i<ll; i++ ) {
     var valu = value.charAt(i)
     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 = (document.cookie.indexOf('fontSTARTno')>-1) ? rewriteNoLogicFont(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 (value == 'I1') {rl = value; rule[n]=value}
 else if (  a == 'A' ) {
     rule[n] = 'Assumption'; level[n] = level[n-1] + 1;
     document.der.elements['s' + n + level[n-1] ].value = "....what if?..............................................."
   document.der.elements['j' + n].value = "Assumption";
     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 + '-,'; 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 >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'; rl = 'R'
          value = value.substring(0,value.length-1) + ' R' 
}
          else {
     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 == 'I2' || rl == '&E' || rl  == 'vI' || rl == '^E' || rl == '^I' || rl == '%I') && (j2[n] != null || isIn('-',j1[n]))) {
               wrong('j',n,'')
               alertX("You need to cite one individual line for " + rl)
   }
   else if (  rl == '^E' && (j2[n] != null || isNaN(j1[n]) || mainLO(thm[j1[n]]) != '^' )) {
               wrong('j',n,'')
               alertX("You need to cite a universally quanified sentence for " + rl )
   }
   else if ( rl == '%E' && ( j2[n]==null || j3[n]!=null || ( !( isIn('-',j2[n]) && mainLO( thm[j1[n]] ) == '%' ) && !( isIn('-',j1[n])  && mainLO( thm[j2[n]] ) == '%') )))  {
     wrong('j',n,'')
     alertX("You need to cite one indiviual line - an existentially quantified sentence - and one subderivation for backward-E elimination.")
}
          else if ( (rl == 'I3' || rl == 'I4' || rl == '>E' || rl == '=E' || rl == '&I' || rl == '=I' || rl == 'DS' || rl == 'MT' || rl == 'HS') && (j2[n] == null || j3[n] != null || isIn('-',j1[n]) || isIn('-',j2[n])) ) {
               wrong('j',n,'')
               alertX("You need to cite two individual 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 = (document.cookie.indexOf('fontSTARTno')>-1) ? rewriteNoLogicFont(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 if (  rl == '%E') {
     a = ( isIn('-',j2[n]) ) ? j2[n] : j1[n]
          var ls = level[a.substring(0,a.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 = dropParen(rewritePLder(deSpace(value)))
     document.der.elements['s'+n+l].value = displaySpace(value);
if ( value.charAt(value.length-1) == '?' ) {}
else {
     thm[n] = value; var th = value
     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 = mainLO(goal), asm // main connective of goal and appropriate assumption
		if (mcon == '>') asm = goal.substring(0,p)
		else if (mcon == '~') asm = goal.substring(1)
		else if (mcon == '%' || mcon == '^' ) asm = '~' + goal
		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 (th == '') {}
else if ( rl == 'Premise' ) {
   if ( l != 1 || !isPL(th) || !noFreeVar(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 ( !isPL(th) || !noFreeVar(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 (rl == 'I1' && th.length==3) {
var con1 = th.charAt(1), con2 =  th.charAt(2)
if (th.charAt(0)!='I' || !isIn(con1,constant) || con1!=con2) wrong('s',n,l)
}

else if (rl == 'I2' && j1[n] != null && j2[n] == null && th.length == 3 && thm[j1[n]].length==3 && th.charAt(0)=='I' && thm[j1[n]].charAt(0)=='I') {
var con1 = th.charAt(1), con2 =  th.charAt(2)
if ( !isIn(con1,constant) || !isIn(con2,constant) ||con1!=thm[j1[n]].charAt(2) ||con2!=thm[j1[n]].charAt(1)) wrong('s',n,l)
}

else if (rl == 'I3' && j2[n] != null && j3[n] == null && th.length == 3 && th.charAt(0)=='I' ) {
var inp1 = thm[j1[n]], inp2 = thm[j2[n]], con1 = th.charAt(1), con2 =  th.charAt(2)
if (inp1.length!=3 || inp2.length!=3 || inp1.charAt(0)!='I' || inp2.charAt(0)!='I') wrong('s',n,l)
else if (inp1.charAt(1)!=con1 ) {
	if (inp2.charAt(1) == con1) {
		if (inp2.charAt(2)!=inp1.charAt(1) || con2 != inp1.charAt(2) ) wrong('s',n,l)
		}
	else wrong('s',n,l)
	}
	else {
		if (inp2.charAt(2)!=con2 || inp1.charAt(2)!=inp2.charAt(1) ) wrong('s',n,l)
		}
}

else if (rl == 'I4') {
	var inp1 = thm[j1[n]], inp2 = thm[j2[n]]
	if (inp2.charAt(0)=='I' && inp2.length==3) {
		var con1 = inp2.charAt(1), con2 = inp2.charAt(2)
		if (th != substitute(con2,con1,inp1)) wrong('s',n,l)
	}
	else if (inp1.charAt(0)=='I' && inp1.length==3) {
		var con1 = inp1.charAt(1), con2 = inp1.charAt(2)
		if (th != substitute(con2,con1,inp2)) wrong('s',n,l)
	}
	// else if ( both inputs are identities... FIX THIS!!!!!
	else wrong('s',n,l)
}

else if ( rl == '&E' ) {
   if ( j2[n] != null || mainLO(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]] 
     if ( biC.indexOf(mainLO(th1)) >-1 ) { th1 = '(' + th1 + ')';}
     if ( biC.indexOf(mainLO(th2)) >-1 ) { th2 = '(' + th2 + ')';}
     ans = th1 + '&' + th2; ans2 = th2 + '&' + th1
     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  ( mainLO(th) != '&' ) {
          wrong('s',n,l)
     alertX("The sentence entered does not have main connective \'&\'.")
     }    
     else if ( th != ans && th != ans2  ) {
     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) != '/' && mainLO(th) != '>' )|| x.indexOf('-')<0 || isNaN(Start) || isNaN(Stop) || j2[n] != null || subT[Start] != Stop ){
          wrong('s',n,l) ;wrong('j',n,'');
}
     else if ( th == '/' || th == '//' ) {
     a = ( biC.indexOf(mainLO(thm[Start]))>-1 ) ? '(' + thm[Start] + ')' : thm[Start]
     c = ( biC.indexOf(mainLO(thm[Stop]))>-1 ) ? '(' + 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 ( ( mainLO(a1) != null &&!isIn(mainLO(a1),unary) && !out(a) ) || ( mainLO(c1) != null && !isIn(mainLO(c1),unary) && !out(c) ) ) {
      wrong('s',n,l);
      alertX("Check parentheses in " + th + ".")
          }}
}}}

else if ( rl == '>E' && 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 ( mainLO(h) != '>'  ) {
     wrong('j',n,'')
     }
     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 || (mainLO(th) != 'v' && th.charAt(0) != '/')) {
     wrong("s",n,l); wrong('j',n,'');
          }
     else {
     th1 = thm[j1[n]]
          if ( th.charAt(0) == '/' ) {
               thP = ( biC.indexOf(mainLO(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 && isPL(c2) && noFreeVar(c2)) || ( c2 == th1  && isPL(c1) && noFreeVar(c1)) ) {
	wrong('s',n,l);
	alertX('Make sure that you\'ve added a sentence -- not just a formula -- to <blockquote>' + th1 + '.</blockquote>') 
               }
               else if ( ( mainLO(c1) != null && !isIn(mainLO(c1),unary) && !out(p1) ) || ( mainLO(c2) != null &&!isIn(mainLO(c2),unary) && !out(p2) ))  {
     wrong('s',n,l);}
}}}
else if ( rl == 'vE' && j3[n] != null ) {
     cite = new Array (thm[j1[n]],thm[j2[n]],thm[j3[n]])
   for ( var i=0; i<3; i++ ) {
     if (mainLO(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 = (mainLO(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(d + " should be a disjunction, i.e.,  its main connective should be \'v\'.");
          }
     else {
     if ( mainLO(h1) != ">" || mainLO(h2) != ">" ) {
          wrong('s',n,l);alertX(c + " should be a conditional, i.e., main connective should be \'>\'.");
          }
          else {
          var a1; mainLO(h1); a1 = dropParen(h1.substring(0,p)); c1 = dropParen(h1.substring(p+1))
          var a2; mainLO(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()
          }
     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 ( mainLO(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 = mainLO(thmE)
          negEP = ( !out(thmE) && c != null && c != '~'  && c!='^' && c!='%') ? '~(' + thmE + ')' : '~' + thmE ;
          negEB = ( !out(thmE) && c != null && c != '~'  && c!='^' && 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 = mainLO(t);
            var tNP = ( !out(t) && c != null && !isIn(c,unary)  )? '~(' + t + ')' : '~' + t;
            var tNB = ( !out(t) && c != null && !isIn(c,unary) )? '~[' + 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' ) {
   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()
          }
     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(mainLO(thm[Start])) >-1 ) ? '~(' + thm[Start] + ')' : '~' + thm[Start]
     if ( th == '/' || th == '//' ) {th = ans; thm[n]= th; document.der.elements['s' + n + l].value = th }
     if ( mainLO(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 stop = true; var thmE = thm[Stop]; var c = mainLO(thmE)
          negEP = ( !out(thmE) && c != null && !isIn(c,unary)) ? '~(' + thmE + ')' : '~' + thmE ;
          negEB = ( !out(thmE) && c != null && !isIn(c,unary)) ? '~[' + 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 = mainLO(t);
            var tNP = ( !out(t) && c != null && !isIn(c,unary))? '~(' + t + ')' : '~' + t;
            var tNB = ( !out(t) && c != null && !isIn(c,unary) )? '~[' + 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,''); 
          }
          else {
          var cite = new Array; cite[0] = thm[j1[n]]; cite[1] = thm[j2[n]];
   if ( mainLO(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 ( mainLO(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(mainLO(a1))>-1) ? '(' + a1 + ')' : a1; a2P = (biC.indexOf(mainLO(a2))>-1) ? '(' + a2 + ')' : a2
          th = a1P + '=' + a2P; thm[n]= th; document.der.elements['s' + n + l].value = th 
        }
        if (  th == '//' )  {
          a1P = (biC.indexOf(mainLO(a1))>-1) ? '(' + a1 + ')' : a1; a2P = (biC.indexOf(mainLO(a2))>-1) ? '(' + a2 + ')' : a2
          th = a2P + '=' + a1P; thm[n]= th; document.der.elements['s' + n + l].value = th 
        }
               if ( mainLO(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) ) && isPL(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 ( mainLO(b) != '=') {
     wrong('j',n,'');
     }
     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,'')
     }
     else if ( th == '/' || th == '//' )  {th = thm[j1[n]]; thm[n]= th; document.der.elements['s' + n + l].value = displaySpace(th) }
   else    if ( th != thm[j1[n]] ) {
     wrong('s',n,l)
     }
}
else if ( rl == '^E'  && thm[j1[n]].substring(0,2) == '(^' && thm[j1[n]].charAt(3) == ')' ) {
   if ( !subInst(th,thm[j1[n]] ) )wrong('s',n,l)
}
else if ( rl == '^I' ) {
     if ( mainLO(th) != '^' ) {
   wrong('s',n,l)
   alertX("For ^I, your sentence on line " + n + " must have main logical operator \'^\'.")
     }
     else if ( !subInst(thm[j1[n]],th ) )  {
     wrong('s',n,l)
     alertX("Your cited line " + j1[n] + ", which is \'" + thm[j1[n]] + "\', needs to be a substitution instance of  line " + n + ": \'" + th + "\'.")
   }
   else if ( isIn(cnst, th) ) {
     wrong('s',n,l)
     alertX("The substituting constant, " + cnst + ", is not allowed to occur in \'" + th + "\' of line " + n + ".")
     }
   else {
     for ( var i=1; i<n; i++ ) {
          if ( (rule[i] == 'Premise' || (rule[i] == 'Assumption' && !term[i])) && isIn(cnst,thm[i]) ) {
               wrong('s',n,l)
               alertX("Your choice of constant, " + cnst + ", in line " + n + " occurs above in " + i + ".  But  line " + i + " is a premise or undischarged assumption. The constant \'" + cnst + "\' needs to be ARBITRARY.")
                    break
               }
          }
   }
}

else if ( rl == '%E'  ) {
	if (!isIn('-',j2[n])) { // so that j1[n] is the single line
		var swtch = j2[n]
		j2[n] = j1[n]
		j1[n] = swtch
	}
   Start = j2[n].substring(0,j2[n].indexOf('-')); Stop = j2[n].substring(j2[n].indexOf('-')+1)
   e = thm[j1[n]]; a = thm[Start]; d = thm[Stop]
     if (  subT[Start] != Stop && subs[level[n]+1] < n ) {
          termQ(Start,parseInt(Stop)+1,n)
          document.der.elements['j'+(n+1)].focus()
          }
   if ( th != d ) {
     wrong('s',n,l)
     }
     else if ( !subInst(a,e) ) wrong('s',n,l)
     else if ( isIn(cnst,th) ) {
          wrong('s',n,l) 
          alertX("Your choice of constant, \'" + cnst + "\' in the assumption \'" + a + "\' is not allowed to occur in \'" + th + "\' at line " + n + ".")
     }
     else if ( isIn(cnst,thm[j1[n]]) ) {
     alertX("Your choice of constant, \'" + cnst + "\' in the assumption \'" + a + "\' is not allowed because it already  occurs in \'" + e + "\' at line " + j1[n] + ".")
     }
     else {
     for ( var i=1; i<n; i++ ) {
          if ( (rule[i] == 'Premise' || (rule[i] == 'Assumption' && !term[i])) && isIn(cnst,thm[i]) ) {
               alertX("Your choice of constant, " + cnst + ", in line " + n + " occurs above in " + i + ".  But  line " + i + " is a premise or undischarged assumption.  Choose a new constant; it needs to be ARBITRARY.")
               wrong('s',n,l)
                    break
               }
          }
   }
}
else if ( rl == '%I' ) {
     c = mainLO(th)
     if ( c != '%' ) {
   wrong('s',n,l)
   alertX("For %I, your sentence on line " + n + " must have main logical operator \'%\'. Note that the main logical operator of your line " + n + " is \'" + c + "\'. You may need to add parentheses.")
     }
     if ( !subInst(thm[j1[n]],th ) )wrong('s',n,l)
}

//for PD+
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 (!replace &&  th.charAt(th.length-1) != '?' && 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 (typeof move == 'function' && th == goal && l==1 ) move() // to avoid keeping track
	else if ( l == 1 && goal == '*') checkContra(n,th,goal + goalLine) // looking for a contradiction
	else if ( l == 1 && goal.charAt(0) == '!') checkEquiv(n,th)// looking to see that there are two derivations 
	else if ( l == 1 && th == goal ) keepTrack(goal + goalLine) 
	}
}
     //s1 is a substitution instance of s0?  boolean function.  assumes dropParen, isIn(), mainLO()
function subInst(s1,s7) {
var s0 = s7.substring(4)
     var vari = s7.charAt(2); 
     var s0 = (isIn(mainLO(s0),biC) ) ? dropParen(s0) : s0
     var len = s1.length
     if ( s0.length != len || isIn(vari,s1) || !isIn(vari,variable) ) return false
else {
   cnst = null;
     for ( var i=0; i<len; i++ ) {
     chr1 = s1.charAt(i); chr2 = s0.charAt(i)
     if ( chr1 != chr2 ) {
          if ( !isIn(chr1,constant) ) {return false; break}
               else if ( cnst == null  )  {
                    if ( chr2 == vari  )  cnst = chr1
                    else { return false; break}
               }
               else if ( chr1 != cnst || chr2 != vari ) {return false; break}        
          
               }
          }
          return true
     }
}

// a simple substitution: c2 in place of c1...
function substitute(c2,c1,strng) {
for (var i=0;i<strng.length;i++) {
	if (strng.charAt(i)==c1) strng = strng.substring(0,i) + c2 + strng.substring(i+1)
	}
return strng
}