// checkPlusFill.js

function checkPlus(th,n,l,rl)  {
 if (rl == 'MT' && typeof(thm[j2[n]])!= "undefined")	{
	var h = (thm[j1[n]].length > thm[j2[n]].length) ? thm[j1[n]] : thm[j2[n]];
   var neg = (thm[j1[n]].length > thm[j2[n]].length) ? thm[j2[n]] : thm[j1[n]];
   	if ( j2[n] == null || j3[n] != null  || mainConn(neg) != '~'|| mainConn(h) != '>') {
   		wrong('j',n,'');wrong('s',n,l); alertX('You need to cite one conditional and one negation for MT.')
		}
	else {
	var a = h.substring(0,p); var c = h.substring(p+1);  ans = '~' + a;
		if ( typeof MTDSHSreplace == 'boolean' && MTDSHSreplace == true && (th == '/' || th == '//') ) {
			th = ans; thm[n]= ans; document.der.elements['s' + n + l].value = ans }
		if ( neg != '~' + c || th != ans) {
			wrong('s',n,l);
			alertX('Your answer does not fit the form for MT:<TABLE border="1" align="center"><TR><TH colspan="2">MT</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><BR><IMG src="pix/down.gif" width="14" height="21"> <BR>~<SPAN class="variable">P</SPAN></SPAN></TD></TR></TABLE>')
	}		}
}

else if ( rl == 'DS' && typeof(thm[j2[n]])!= "undefined" )  {
	var d = (thm[j1[n]].length > thm[j2[n]].length) ? thm[j1[n]] : thm[j2[n]];
   var neg = (thm[j1[n]].length > thm[j2[n]].length) ? thm[j2[n]] : thm[j1[n]];
   	if ( j2[n] == null || j3[n] != null || mainConn(neg) != '~' || mainConn(d) != 'v') {
   		wrong('j',n,'');wrong('s',n,l); alertX('You need to cite a disjunction and the negation of one of the disjuncts.')
		return
		}
	var d1 = d.substring(0,p); var d2 = d.substring(p+1);
		if (mainConn(neg) != '~') {wrong('s',n,l); alertX('You need to cite a disjunction and the negation of one of the disjuncts.')}
		else {
		neg = neg.substring(1);
		var ans = ( neg == d1 ) ? d2 : d1
		ans = dropParen(ans);	
			if ( typeof MTDSHSreplace == 'boolean' && MTDSHSreplace == true && (th == '/' || th == '//' )) {th = ans; thm[n]= ans; document.der.elements['s' + n + l].value = ans }
			if ( (ans == d1  && neg != d2) || th != ans) {wrong('s',n,l);
		alertX('Your answer does not fit the form for DS:<TABLE border="1" align="center"><TR><TH colspan="5">DS</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>v<SPAN class="variable">Q</span><BR>~<SPAN class="variable">Q</SPAN><BR><IMG src="pix/down.gif" width="14" height="21"> <BR><SPAN class="variable">P</SPAN></TD><td>or</td><TD>input 1:<BR>input 2:<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">Q</SPAN><BR><IMG src="pix/down.gif" width="14" height="21"> <BR><SPAN class="variable">P</SPAN> </SPAN></TD></TR></TABLE>')
	}
		}
}

else if ( rl == 'HS' && j2[n] != null && j3[n] == null )  {
	var h1 = thm[j1[n]]; var h2 = thm[j2[n]]; 
		if (mainConn(h1) != '>') {wrong('j',n,'');wrong('s',n,l);alertX('You need to site two conditionals for HS.')}
	else {
			var a1 = h1.substring(0,p); var c1 = h1.substring(p+1);
				if (mainConn(h2) != '>') {wrong('j',n,'');wrong('s',n,l);alertX('You need to site two conditionals for HS.')}
		else {
			var a2 = h2.substring(0,p); var c2 = h2.substring(p+1);
			var a1a=a1, a2a=a2
			if (biC.indexOf(mainConn(a1))>-1) a1a = (a1.charAt(0)=='(') ? '['+a1.substring(1,a1.length-1)+']' : '('+a1.substring(1,a1.length-1)+')'
			if (biC.indexOf(mainConn(a2))>-1) a2a = (a2.charAt(0)=='(') ? '['+a2.substring(1,a1.length-1)+']' : '('+a2.substring(1,a2.length-1)+')'
			var ans1 = ''; 
			if ( c1 == a2 || c1 == a2a ) ans1 = a1 + '>' + c2
			else if (a1 == c2 || a1a == c2) ans1 = a2 + '>' + c1
			if ( typeof MTDSHSreplace == 'boolean' && MTDSHSreplace == true && (th == '/' || th == '//' ) ) {
				if (ans1 != '') {
					th = ans1; thm[n]= ans1; document.der.elements['s' + n + l].value = ans1 
				}
			}
			if ( th != ans1 ) {
				wrong('s',n,l);
				alertX('Your answer does not fit the form for HS:<TABLE border="1" align="center"><TR><TH colspan="2">HS</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">R</span><BR><IMG src="pix/down.gif" width="14" height="21"> <BR><SPAN class="variable">P</SPAN><FONT face="Logic">&gt;</FONT><SPAN class="variable">R</span></TD></TR></TABLE>')
			}
		}	
	}
}

else {
	if ( j2[n] != null || rl == null || rl == 'DS' || rl == 'HS' || rl == 'MT' ) {
		wrong('j',n,'');wrong('s',n,l);}
	else if ( th == '/' || th == '//' ) {
		thm[n]= null; th = thm[j1[n]] + '???'
		document.der.elements['s' + n + l].value = th
		document.der.elements['s' + n + l].focus()
	}
	else  if ( rl == 'DN' ) {
	var lng = (th.length > thm[j1[n]].length) ? th : thm[j1[n]]; var sht = (th.length > thm[j1[n]].length) ? thm[j1[n]]  : th
	var found = false
	for ( var i=0; i<sht.length; i++ ) {
		if ( sht.charAt(i) != lng.charAt(i) ) {
		found = true
		if ( i==0 && biC.indexOf(mainConn(sht))>-1 ) var sht2 = '(' + sht + ')'
		break
		}	
	}
	if ( !found || lng.charAt(i) != '~' || lng.charAt(i+1) != '~' || ( (lng.substring(0,i) + lng.substring(i+2) != sht && lng.substring(0,i) + lng.substring(i+2) != sht2 )) || !isSL(lng) ) wrong('s',n,l);
}
	else {
CS = null; CS = new Array; 
comp = null; comp1 = null; comp2 = null; compOrder = null; compOrder1 = null; compOrder2 = null; cmp1 = null; cmp2 = null;
comp = new Array;  compOrder = new Array;comp1 = new Array;  compOrder1 = new Array;comp2 = new Array;  compOrder2= new Array;
absMcPos = null; absMcPos1 = null; absMcPos2 = null; absMcPos = new Array; absMcPos1 = new Array; absMcPos2 = new Array; var neg; var oth; var negMc; var othMc;
compare(th,thm[j1[n]])
	if ( rl == 'DM' && (mc1 == '~' && mc2 == '&'|| mc2 == '~' && mc1 == '&' || mc1 == '~' && mc2 == 'v'|| mc2 == '~' && mc1 == 'v') ) {
		if ( mc1 == '~' ) {
   		neg = cmp1; oth = cmp2
   		negMc = mc1; othMc = mc2
   		oth1 = sub21; oth2 = sub22
		}
		else {
   		neg = cmp2; oth = cmp1
   		negMc = mc2; othMc = mc1
   		oth1 = sub1; oth2 = sub2
		}
		neg1 = neg.substring(1); neg1mc = mainConn(dropParen(neg1)); neg11 = neg1.substring(1,++p); neg12 = neg1.substring(++p, neg1.length-1);
		if ( (neg1mc != '&' && neg1mc != 'v') || neg1mc == othMc || oth1 != '~' + neg11 || oth2 !=  '~' + neg12 ) wrong('s',n,l);
	}
	else if ( rl == 'IM' && ((mc1 == '>' && mc2 == 'v') || (mc2 == '>' && mc1 == 'v') ) ){
   	if ( mc1 == '>' ) {
   		ant = sub1;  cons = sub2;   d1= sub21;   d2= sub22
		}
		else {
   		d1 = sub1;  d2 = sub2;  ant = sub21;  cons = sub22
		}
		if ( d1 != '~' + ant || d2 != cons ) wrong('s',n,l);
	}
	else if ( rl == 'AS' &&  mc1 == mc2 && (mc1 == '&' || mc1 == 'v') )  {
		if ( sub1.length > sub21.length ) {
   		mainConn(dropParen(sub1))
   		c11 = sub1.substring(1,++p); c12 = sub1.substring(++p,sub1.length-1); c2 = sub2
   		mainConn(dropParen(sub22))
   		b1 = sub21; b21 = sub22.substring(1,++p); b22 = sub22.substring(++p,sub22.length-1)
		}
		else {
   		mainConn(dropParen(sub21))
   		c11 = sub21.substring(1,++p); c12 = sub21.substring(++p,sub21.length-1); c2 = sub22
   		mainConn(dropParen(sub2))
   		b1 = sub1; b21 = sub2.substring(1,++p); b22 = sub2.substring(++p,sub2.length-1)
		}
		if ( b1 != c11 || b21 != c12 || b22 != c2 ) wrong('s',n,l);
	}
	else if ( rl == 'TR' && mc1=='>' && mc2=='>' ) {
   		if (cmp1.length<cmp2.length) {
			var sht1 = sub1, sht2 = sub2
			var lng1 = sub21, lng2 = sub22
			}
		else {
			var lng1 = sub1, lng2 = sub2
			var sht1 = sub21, sht2 = sub22
			}
		if ( (lng1.charAt(0)!='~' || mainConn(lng1)!='~' ) || (lng2.charAt(0)!='~' || mainConn(lng2)!='~' ) || ( lng1.substring(1)!=sht2 || lng2.substring(1)!=sht1 ) ) wrong('s',n,l)
		}
else if ( rl == 'EX'  && mc1 == '>'  && mc2 == '>' ) {
   if ( sub1.length > sub21.length ) {
   	mc1 = mainConn(dropParen(sub1))
   	x1 = sub1.substring(1,++p); y1 = sub1.substring(++p,sub1.length-1); z1 = sub2;
   	mc2 =mainConn(dropParen(sub22))
   	x2 = sub21; y2 = sub22.substring(1,++p); z2 =sub22.substring(++p,sub22.length-1); 
	}
	else {
   	mc1 =mainConn(dropParen(sub21))
   	x1 = sub21.substring(1,++p); y1 = sub21.substring(++p,sub21.length-1); z1 = sub22;
   	mc2 = mainConn(dropParen(sub2)); 
   	x2 = sub1; y2 = sub2.substring(1,++p); z2 =sub2.substring(++p,sub2.length-1); 
	}
	if ( mc1 != '&' || mc2 != '>' || x1 != x2 || y1 != y2 || z1 != z2 ) wrong('s',n,l);

}
else if ( rl == 'DI' && ( mc1 == 'v' && mc2 == '&' || mc1 == '&' && mc2 == 'v' ) ) {
   if ( cmp1.length < cmp2.length ) {	
   var mcS = mc1; var mcL = mc2
   var mcC1 = mainConn(dropParen(sub2));
   var x1 = sub1; var y1 = sub2.substring(1,++p); var z1 = sub2.substring(++p,sub2.length-1)
   var mcC2 = mainConn(dropParen(sub21))
   var x21 = sub21.substring(1,++p); var y2 = sub21.substring(++p,sub21.length-1)
   var mcC3 = mainConn(dropParen(sub22))
   var x22 = sub22.substring(1,++p); var z2 = sub22.substring(++p,sub22.length-1)
	}
	else  {
   var mcS = mc2; var mcL = mc1
   var mcC1 = mainConn(dropParen(sub22));
   var x1 = sub21; var y1 = sub22.substring(1,++p); var z1 = sub22.substring(++p,sub22.length-1)
   var mcC2 = mainConn(dropParen(sub1))
   var x21 = sub1.substring(1,++p); var y2 = sub1.substring(++p,sub1.length-1)
   var mcC3 = mainConn(dropParen(sub2))
   var x22 = sub2.substring(1,++p); var z2 = sub2.substring(++p,sub2.length-1)
	}
	if ( mcS != mcC2 || mcS != mcC3 || mcL != mcC1 || x1 != x21 || x21 != x22 || y1 != y2 || z1 != z2 ) wrong('s',n,l);
}
else if ( rl == 'EQ' ) {
	if ( cmp1.length < cmp2.length ) {
   	var x1 = sub1; var y1 = sub2; var mcS = mc1; var mcL = mc2
   	var mcC2 = mainConn(dropParen(sub21))
   	var x2 = sub21.substring(1,++p); var y2 = sub21.substring(++p,sub21.length-1)
   	var mcC3 = mainConn(dropParen(sub22))
   	var y3 = sub22.substring(1,++p); var x3 = sub22.substring(++p,sub22.length-1)
	}
	else {
   	var x1 = sub21; var y1 = sub22; var mcS = mc2; var mcL = mc1
   	var mcC2 = mainConn(dropParen(sub1))
   	var x2 = sub1.substring(1,++p); var y2 = sub1.substring(++p,sub1.length-1)
   	var mcC3 = mainConn(dropParen(sub2))
   	var y3 = sub2.substring(1,++p); var x3 = sub2.substring(++p,sub2.length-1)
	}
	if ( mcL == '&' && mcS == '=' &&  mcC2 == '>' && mcC2 == '>' && x1 == x2 && x2 == x3 && y1 == y2 && y2 == y3 ) {}
	else if ( mcL == 'v' && mcS == '=' && mcC2 == '&' && mcC2 == '&' && x1 == x2 && '~' + x2 == y3 && y1 == y2 && '~' + y2 == x3) {	}
	else {
   	wrong('s',n,l)
	}
}
	else if ( rl == 'ID' ) { 
   	var shrt = (cmp1.length > cmp2.length) ? cmp2 : cmp1
  		var lng =  (cmp1.length > cmp2.length) ? cmp1 : cmp2
		var dropL = dropParen(lng); 
  			if ( dropL != shrt + '&' + shrt && dropL != shrt + 'v' + shrt ) {
			if ( (shrt == cmp1 && biC.indexOf(mc1)>-1) || (shrt == cmp2 && biC.indexOf(mc2)>-1) ) {
				var dropS = '(' + dropParen(shrt) + ')';
				if ( dropL != dropS + '&' + dropS && dropL != dropS + 'v' + dropS ) wrong('s',n,l);
				}
				else { wrong('s',n,l); }
			}
		}
else if ( rl == 'CM' ) { 				//CM for '=' !!!
	var c1 = sub1; var d1 = sub2; var c2 = sub21; var d2 = sub22;
	if (mc1!=mc2 || (mc1 != '&' && mc1 != 'v' && mc1 != '=') || c1 != d2 || d1 != c2) wrong('s',n,l);
}

else { wrong('s',n,l);wrong('j',n, "");}
	
}

  
}


}