/* ======================================================================
DESC: 		Checks for membership in PL, the set of formulas

PLATFORMS: 

USAGE NOTES:  isPL() removes spaces and adds parens if needed, then returns PL().

	The functions here require simp.js, def.js and mainLO.js to work!!!
====================================================================== */

/* ======================================================================
FUNCTIONS: 	isPL , PL, noFreeVar

INPUT:		text string
				
RETURNS:		boolean

DESC:							
====================================================================== */
function isPL(text)  {
	text = deSpace(text)
	if (!out(text) && biC.indexOf(mainLO(text))>-1)  {
		text = '(' + text + ')';
		}
	return PL(text);
}

function PL(text)  {
	if ( isAtomic(text) ) return true
	else {
	mainLO(dropParen(text))
	if ( c == '~' && text.charAt(0) == '~')  {
		gamma = text.substring(1);
		return PL(gamma);
	}
	else if ( ((c == '%' && text.substring(0,2) == '(%')||(c == '^' && text.substring(0,2) == '(^')) &&  isIn( text.charAt(2), variable ) && text.charAt(3) == ')' ) {
		gamma = text.substring(4); var t = text.charAt(2)
		if ( isIn('%' + t , gamma) || isIn('^' + t , gamma) ) {
   		return false
		}
		else {
   		return PL(gamma);
		}
	}
	else if ( biC.indexOf(mainLO(dropParen(text))) > -1 && out(text) )  {
	beta = text.substring(p+2,text.length - 1);
	if ( !PL(beta) )  {
		return false;}
	else { mainLO(dropParen(text));
	alpha = text.substring(1,p+1); 
	if ( !PL(alpha) ) {
		return false;}
	else {return true}
}}
	else { return false }
}
}

stop = true
function noFreeVar(string) {
var jj
if (structurePL(string)) {
stop = false
y=newtext; jj = 0
if ( isIn(mainLO(string),biC) && !out(string) ) jj = -1
for ( var i=0; i<y.length; i++ ) {
   if ( isIn(y.charAt(i),variable) && !bound[i] ) {
	jj += i + 1
   stop = true 
   break;
}
}
if ( !stop ) {
	return true
}}
else {
   return false
}
}