/*
FUNCTIONS: 	termQ() and terminate()
 */
function termQ(b,e,n) {
var lev = level[b]
if ( b != null && subs[lev] == b) {
  	var x = prompt("Would you like to terminate the subdervation?  If ok, the subderivation will be:", b + " - " + (e-1));
	if ( x == null ) {
   return false
	}
	else {
	x = deSpace(x); Start = parseInt(x.substring(0,x.indexOf('-'))); Stop = parseInt(x.substring( x.indexOf('-') + 1 ));
		if ( x.indexOf('-')<0 || isNaN(Start) || isNaN(Stop) ) {
   		alert("You need to enter a subderivation, something like \'" + b + " - " + e + "\'.");
			termQ(b,e);
			return null;
		}	
		else if ( Start > Stop ||  Stop >=n || rule[Start] != 'Assumption' || lev != level[Stop]) {
   		alert("I dont\'t understand. The subderivation you cite seems to be inappropriate. Please try again.");
   		var y = termQ(b,e,n);
			return null;
		}
		else {
			var stop = false
			for (i=Start+1; i<=Stop; i++)  { // this checks to make sure there is no sub-subD at the same level 
				if ( rule[i] == 'Assumption' && level[i] == lev ) {
					stop = true; break
				}
			}
			if (stop) {
				alert("The subderivation you cite seems to be inappropriate.")
				return false
			}
			else {
   			terminate(Start,Stop);
				return true;
			}
		}
	}
}
}

function terminate(b,e) { var wrong = false
 for ( var i=e+1; i<j.length; i++ ) {
   if ( (j1[i]>=b && j1[i]<=e && j[i]!='') || (j2[i]>=b && j2[i]<=e && j[i]!='') || (j3[i]>=b && j3[i]<=e && j[i]!='') ) {
   alert("If you terminate this subderivation at " + e + ", then line " + i + " will no longer be justified");
   wrong = true; break;
}

}
if ( !wrong ) {

 subT[b] = e;
	for ( var i=b; i<=e; i++ ) {
   term[i] = true;}
   subs[level[b]] = null;
   var ls = level[b]-1;
   document.der.elements['s' + b + ls].value = "....what if?.........."
   if ( ls > 0 ) {
   	for ( var i=b+1; i<=e; i++ ) {
		   document.der.elements['s' + i + ls].value = '....then...............'
		}
   }
	else {
   	alert('The cited range does not correspond to a subderivation');
	}
	

}
}