/* PCP: Point and Click Proofs, Peter Jipsen, March 2001 www.math.vanderbilt.edu/~pjipsen/PCP/PCPproofs.js Requires: www.math.vanderbilt.edu/~pjipsen/PCP/math2html.js Examples: www.math.vanderbilt.edu/~pjipsen/PCP/PCPmain.html */ function obj2str(obj, obj_name) { var result = "" for (var i in obj) result += i + " = " + obj[i] + "; " return result } function equalExpr(p,q) { if (p==null || q==null || p.symbol==null || q.symbol==null) { document.write(obj2str(p),obj2str(q),"*******equalExpr*******"); return false; } if (p.symbol.name!=q.symbol.name) return false; if (p.arg.length!=q.arg.length) return false; if (p.arg.length==0) return true; for (var i=0; iparseInt(ind2[i]) || parseInt(ind1[i])=10) s=""; if (less((ns+i).split("."),currentFocus) && (pr[i].expr.symbol.pred || pr[i].expr.symbol.conn) || pr[i].gap && (pr[i-1].expr.symbol.pred || pr[i-1].expr.symbol.conn)) st=st+""; else st=st+" "+s+ns+i+s; st=st+space(indent); if (pr[i].apply) { var r=pr[i]; //document.write(obj2str(r),"**
"); var q=getElement(p,r.rule); if (pr[0].consider) st=st+q.expr.symbol.output; st=st+e2s(r.expr); st=st+sp+"(by "+(q.name==null?r.rule.join("."):q.name); if (r.premises!=null) for (var j=0; j......"+ ""; else st=st+"......"+ ""; } else if (pr[i].gap) st=st+"......"; if (pr[i].name!=null) if (pr[i].name[0]=="(") st=st+"   "+pr[i].name; else st=st+"   "+pr[i].name+""; st=st+"
\n"; } } else if (showFlag || i==currentFocus[indent-1]) st=st+proof2html(p,pr[i],indent+1,ns+i+"."); } return st; } function hideshow() { showFlag=!showFlag; proof.location.href="PCPproof.html" } function undoAbove() {//modify currentProof and redisplay var fo=getElement(currentProof,currentFocus); var subpr=getSubproof(currentProof,currentFocus); if (subprFocus>0 && !subpr[subprFocus].axiom && subpr[subprFocus].name==null) { for (var i=subprFocus; i1) { subpr=getSubproof(currentProof,currentFocus.slice(0,currentFocus.length-1)); subpr[currentFocus[currentFocus.length-2]]= subpr[currentFocus[currentFocus.length-2]][1]; } if (list.length!=0) { list=[]; choose.location.href="PCPchoose.html"; } proof.location.href="PCPproof.html"; } function undoBelow() {//modify currentProof and redisplay var fo=getElement(currentProof,currentFocus); var subpr=getSubproof(currentProof,currentFocus); if (subprFocus1) { subpr=getSubproof(currentProof,currentFocus.slice(0,currentFocus.length-1)); subpr[currentFocus[currentFocus.length-2]]= subpr[currentFocus[currentFocus.length-2]][1]; } if (list.length!=0) { list=[]; choose.location.href="PCPchoose.html"; } proof.location.href="PCPproof.html"; } function focusAbove(st) {//modify currentProof and redisplay var ind=st.split("."); getElement(currentProof,currentFocus).focusAbove=null; getElement(currentProof,ind).focusAbove=true; if (list.length!=0) { list=[]; choose.location.href="PCPchoose.html"; } proof.location.href="PCPproof.html"; } function focusBelow(st) {//modify currentProof and redisplay var ind=st.split("."); getElement(currentProof,currentFocus).focusAbove=null; getElement(currentProof,ind).focusAbove=false; if (list.length!=0) { list=[]; choose.location.href="PCPchoose.html"; } proof.location.href="PCPproof.html"; } function displayExprList(li) { document.writeln("=================
"); for (var i=0; i"); } substList=[]; premsList=[]; function match(q,t,sub) { // Find substitution such that q==sub(t); return true if found. //displayExprList(sub); if (t.symbol.vari) if (sub[t.symbol.index]==null) { if (q.symbol.conn || q.symbol.pred || q.symbol.formulavari) return false; sub[t.symbol.index]=q; if (substList.lengthsl) { for (var j=sl; jsl) { for (var j=sl; jind; i--) subpr[i]=subpr[i-1]; subpr[ind]=list[nextStepChoice]; } } else {//fo.focusBelow nex=list[nextStepChoice].expr; if ((nex.symbol==eq || nex.symbol==iffSymbol) && equalExpr(nex.arg[0],nex.arg[1])) { var ind=subprFocus; subpr[ind-1]={expr:nex, name:"(by equality)"}; list[nextStepChoice].expr=subpr[ind].expr; if (subpr[ind].name!=null) list[nextStepChoice].name=subpr[ind].name; subpr[ind]=list[nextStepChoice]; } else { if (subpr[0].consider) { var cli=[list[nextStepChoice].expr]; var eqli=[{expr:subpr[subprFocus-2].expr, index:currentFocus.slice(0,currentFocus.length-1).concat([subprFocus-2])}]; } else { var cli=conj2list(list[nextStepChoice].expr,[]); //list of premises var eqli=findTrueExpr(); } var newli=[]; var prems=[]; for (var i=0; iind+2*newli.length-2; i--) subpr[i]=subpr[i-2*newli.length+1]; for (var i=0; i