/* l2.pl This CatLog3 - CatLog version l2.pl of 29th August 2018. Copyright (C) Glyn V. Morrill This work may be distributed and/or modified under the conditions of the LaTeX Project Public License, either version 1.3 of this license or (at your option) any later version. The latest version of this license is in http://www.latex-project.org/lppl.txt and version 1.3 or later is part of all distributions of LaTeX version 2005/12/01 or later. This work has the LPPL maintenance status `maintained'. The Current Maintainer of this work is Glyn V. Morrill. This work consists of the files l2.pl, examples.pl, lexicon.pl, out.tex and the derived files der.tex, lex.tex and out.pdf. This is CatLog version l2.pl (CatLog3) by Glyn Morrill, Departament of Computer Science, Polytechnic University of Catalonia (UPC). It is a version of the author's parser/theorem-prover and is made available for non-comercial research purposes. It runs as is on swi-prolog. This file should be consulted together with examples.pl and lexicon.pl. Once consulted, pplex pretty prints the lexicon within Prolog and pplexlatex pretty prints the lexicon in latex to file lex.tex. tt(N) tests examples with identifier unifying with N and writes analyses within Prolog and an analysis for each reading in latex to file der.tex. LaTeXing file out.tex formats all of the lexicon and analyses; prooftree.sty is required. 29th August 2018 */ % atfoc(inp) or atfoc(out) atfoc(inp). :- op(450, xfy, :). :- op(500, xfx, '=>'). :- op(400, xfx, /). % 1 over :- op(400, xfx, bs). % 2 under :- op(400, xfx, *). % 3 continuous product % i % 4 continuous unit :- op(400, xfx, ci). % 5+ circumfix (leftmost) :- op(400, xfx, cin). % 5- circumfix (rightmost) :- op(400, xfx, in). % 6+ infix (leftmost) :- op(400, xfx, inn). % 6- infix (rightmost) :- op(400, xfx, dp). % 7+ discontinuous product (leftmost) :- op(400, xfx, dpn). % 7- discontinuous product (rightmost) % j % 8 discontinuous unit :- op(400, xfx, &). % 9 additive conjunction :- op(400, xfy, +). % 10 additive disjunction :- op(300, xfy, u). % 11 1st order univ. qu. :- op(300, xfy, e). % 12 1st order exist. qu. :- op(300, fy, nL). % 13 sem. active universal modality :- op(300, fy, nM). % 14 sem. active existential modality :- op(300, fy, ab). % 15 univ. bracket modality :- op(300, fy, br). % 16 exist. bracket modality :- op(300, fy, ue). % 17 universal exponential :- op(300, fy, ee). % 18 existential exponential :- op(400, xfx, een). % bounded existential exponential :- op(400, xfx, lca). % 19 limited contr. for anaphora % w(w) % 20 limited weak. for words as types :- op(400, xfx, lio). % 21 left sem. inactive over :- op(400, xfx, liu). % 22 left sem. inactive under :- op(400, xfx, rio). % 23 right sem. inactive over :- op(400, xfx, riu). % 24 right sem. inactive under :- op(400, xfx, lip). % 25 left sem. inactive cont. product :- op(400, xfx, rip). % 26 right sem. inactive cont. product :- op(400, xfx, uic). % 27+ upper sem. inactive circumfix (leftmost) :- op(400, xfx, uicn). % 27- upper sem. inactive circumfix (rightmost) :- op(400, xfx, uii). % 28+ upper sem. inactive infix (leftmost) :- op(400, xfx, uiin). % 28- upper sem. inactive infix (rightmost) :- op(400, xfx, lic). % 29+ lower sem. inactive circumfix (leftmost) :- op(400, xfx, licn). % 29- lower sem. inactive circumfix (rightmost) :- op(400, xfx, lii). % 30+ lower sem. inactive infix (leftmost) :- op(400, xfx, liin). % 30- lower sem. inactive infix (rightmost) :- op(400, xfx, uidp). % 31+ upper sem. inactive disc. product (leftmost) :- op(400, xfx, uidpn).% 31- upper sem. inactive disc. product (rightmost) :- op(400, xfx, lidp). % 32+ lower sem. inactive disc. product (leftmost) :- op(400, xfx, lidpn).% 32- lower sem. inactive disc. product (rightmost) :- op(400, xfx, iac). % 33 sem. inactive additive conjunction :- op(400, xfx, iad). % 34 sem. inactive additive disjunction :- op(300, xfy, iu). % 35 sem. inactive 1st order univ. qu. :- op(300, xfy, ie). % 36 sem. inactive 1st order exist. qu. :- op(300, fy, iL). % 37 sem. inactive universal modality :- op(300, fy, iM). % 38 sem. inactive existential modality :- op(300, fy, lp). % 39 left projection :- op(300, fy, rp). % 40 right projection :- op(300, fy, li). % 41 left injection :- op(300, fy, ri). % 42 right projection :- op(300, fy, sp). % 43+ split (leftmost) :- op(300, fy, spn). % 43- split (rightmost) :- op(300, fy, bg). % 44+ bridge (leftmost) :- op(300, fy, bgn). % 44- bridge (rightmost) :- op(400, xfx, nd). % 45 nondet. division :- op(400, xfx, np). % 46 nondet. continuous product :- op(400, xfx, nci). % 47 nondet. circumfix :- op(400, xfx, nin). % 48 nondet. infix :- op(400, xfx, ndp). % 49 nondet. discontinuous product :- op(400, xfx, -). % 50 difference doout(Gamma, A, S) :- nl, nl, ppseq(user, yes, []: Gamma, l(A)), nl, nl(S), nl(S), write(S, '\\vspace{0.15in}'), nl(S), write(S, '$'), ppseq(latex(S), yes, []: Gamma, l(A)), write(S, '$'), nl(S), (!). prs(N, S) :- fetch(N, Str, A, S), lookuptop(Str, Gamma, A), doout(Gamma, A, S), export(S), clean, p([]: Gamma, l(A, Phi), Prf), nl, nl, ppprf(user, no, 0, Prf), eval(Phi, NF), nl, nl, ppsem(user, NF), nl, assert(found(Prf, NF)), fail. prs(_, S) :- close(S). tt(N) :- time(t(N)). t(N) :- open('der.tex', write, S), prs(N, S). t(_). clean :- retract(copy(_)), (!), clean. clean :- retract(copy(_,_)), (!), clean. clean :- retract(found(_, _)), (!), clean. clean :- retract(symb(_)), (!), clean. clean :- assert(symb(0)). gensymb(S1) :- retract(symb(S)), S1 is S+1, assert(symb(S1)). allumodszone([]: Gamma) :- allumodsconfig(Gamma). allumodsconfig([H|T]) :- var(H), (!), allumodsconfig(T). allumodsconfig([1|T]) :- allumodsconfig(T). allumodsconfig([]). allumodsconfig([l(nL _, _, Ls)|Gamma]) :- allumodsconfiglst(Ls), allumodsconfig(Gamma). allumodsconfig([l(iL _, _, Ls)|Gamma]) :- allumodsconfiglst(Ls), allumodsconfig(Gamma). allumodsconfig([b(OMEGA)|Gamma]) :- allumodszone(OMEGA), allumodsconfig(Gamma). allumodsconfiglst([]). allumodsconfiglst([H|T]) :- allumodsconfig(H), allumodsconfiglst(T). fetch(N, Str, A, S) :- str(N, Str, A), nl, nl, write('('), write(N), write(') '), nl(S), nl(S), write(S, '\\vspace{0.15in}'), nl(S), write(S, '('), write(S, N), write(S, ') '), pppros(user, Str), write(' '), pptype(user, A), nl, write(S, '$'), pppros(latex(S), Str), write(S, ': '), pptype(latex(S), A), write(S, '$'), nl(S). exportone(S) :- collectall([], Derivs), exportall(Derivs, S). exportone(S) :- close(S). export(_). export(S) :- collectall([], Derivs), exportall(Derivs, S). collectall(InDerivs, OutDerivs) :- retract(found(Prf, NF)), (!), numbervars(NF, 0, _), addifnew(Prf, NF, InDerivs, Derivs), collectall(Derivs, OutDerivs). collectall(Derivs, Derivs). addifnew(_, NF, Derivs, Derivs) :- member(f(_, NF), Derivs), (!). addifnew(Prf, NF, Derivs, [f(Prf, NF)|Derivs]). % exportall([], _). exportall([f(Prf, Phi)|Derivs], S) :- nl(S), nl(S), write(S, '\\vspace{0.15in}'), nl(S), nl(S), ppprf(latex(S), no, _, Prf), nl(S), nl(S), write(S, '\\vspace{0.15in}'), nl(S), nl(S), write(S, '$'), ppsem(latex(S), Phi), write(S, '$'), exportall(Derivs, S). p(OMEGA, l(A, Phi), Prf) :- %% countcheck(OMEGA, A), p1(OMEGA, l(A, Phi), Prf). primitive(n(_), []). primitive(s(_), []). primitive(pp(_), []). primitive(cp(_), []). primitive(cn(_), []). primitive(si, [1]). primitive(q, []). primitive(w(_), []). % countcheck(+Xi, +A) checks that the sequent Xi => A % is not unprovable by reason of the count invariant. countcheck(Xi, A) :- typecount(min, out, A, V3), zonecount(max, Xi, V4), listminus(V3, V4, VV), allmlezero(VV), typecount(max, out, A, V1), zonecount(min, Xi, V2), listminus(V1, V2, V), allmgezero(V). zonecount(M, Stoup: Gamma, V) :- stoupcount(M, Stoup, V1), configcount(M, Gamma, V2), listplus(V1, V2, V). stoupcount(_, [], [0, 0, 0, 0, 0, 0, 0, 0]). stoupcount(M, [l(A, _, [])|Stoup], V) :- typecount(M, inp, ue A, V1), stoupcount(M, Stoup, V2), listplus(V1, V2, V). stoupcount(M, [f(A, _, [])|Stoup], V) :- typecount(M, inp, ue A, V1), stoupcount(M, Stoup, V2), listplus(V1, V2, V). allmlezero([]). allmlezero([C|V]) :- mlezero(C), allmlezero(V). mlezero(bot). mlezero(C) :- integer(C), C =< 0. mlzero(bot). mlzero(C) :- integer(C), C < 0. allmgezero([]). allmgezero([C|V]) :- mgezero(C), allmgezero(V). mgezero(top). mgezero(C) :- integer(C), C >= 0. mgzero(top). mgzero(C) :- integer(C), C > 0. comp(inp, out). comp(out, inp). comp(min, max). comp(max, min). typecount(_, _, n(_), [0, 1, 0, 0, 0, 0, 0, 0]). typecount(_, _, s(_), [0, 0, 1, 0, 0, 0, 0, 0]). typecount(_, _, pp(_),[0, 0, 0, 1, 0, 0, 0, 0]). typecount(_, _, cp(_),[0, 0, 0, 0, 1, 0, 0, 0]). typecount(_, _, cn(_),[0, 0, 0, 0, 0, 1, 0, 0]). typecount(_, _, si, [0, 0, 0, 0, 0, 0, 1, 0]). typecount(_, _, q, [0, 0, 0, 0, 0, 0, 0, 1]). typecount(M, Pol, C/B, V) :- % 1 typecount(M, Pol, C, V1), comp(Pol, Pol1), comp(M, M1), typecount(M1, Pol1, B, V2), listminus(V1, V2, V). typecount(M, Pol, A bs C, V) :- % 2 typecount(M, Pol, C, V1), comp(Pol, Pol1), comp(M, M1), typecount(M1, Pol1, A, V2), listminus(V1, V2, V). typecount(M, Pol, A*B, V) :- % 3 typecount(M, Pol, A, V1), typecount(M, Pol, B, V2), listplus(V1, V2, V). typecount(_, _, i, [0, 0, 0, 0, 0, 0, 0, 0]). % 4 typecount(M, Pol, C ci B, V) :- % 5+ typecount(M, Pol, C, V1), comp(Pol, Pol1), comp(M, M1), typecount(M1, Pol1, B, V2), listminus(V1, V2, V). typecount(M, Pol, C cin B, V) :- % 5- typecount(M, Pol, C, V1), comp(Pol, Pol1), comp(M, M1), typecount(M1, Pol1, B, V2), listminus(V1, V2, V). typecount(M, Pol, A in C, V) :- % 6+ typecount(M, Pol, C, V1), comp(Pol, Pol1), comp(M, M1), typecount(M1, Pol1, A, V2), listminus(V1, V2, V). typecount(M, Pol, A inn C, V) :- % 6- typecount(M, Pol, C, V1), comp(Pol, Pol1), comp(M, M1), typecount(M1, Pol1, A, V2), listminus(V1, V2, V). typecount(M, Pol, A dp B, V) :- % 7+ typecount(M, Pol, A, V1), typecount(M, Pol, B, V2), listplus(V1, V2, V). typecount(M, Pol, A dpn B, V) :- % 7- typecount(M, Pol, A, V1), typecount(M, Pol, B, V2), listplus(V1, V2, V). typecount(_, _, j, [0, 0, 0, 0, 0, 0, 0, 0]). % 8 typecount(M, out, A&B, V) :- % 9 typecount(M, out, A, V1), typecount(M, out, B, V2), comp(M, M1), listm(M1, V1, V2, V). typecount(M, inp, A&B, V) :- typecount(M, inp, A, V1), typecount(M, inp, B, V2), listm(M, V1, V2, V). typecount(M, out, A+B, V) :- % 10 typecount(M, out, A, V1), typecount(M, out, B, V2), listm(M, V1, V2, V). typecount(M, inp, A+B, V) :- typecount(M, inp, A, V1), typecount(M, inp, B, V2), comp(M, M1), listm(M1, V1, V2, V). typecount(M, Pol, _ u A, V) :- % 11 typecount(M, Pol, A, V). typecount(M, Pol, _ e A, V) :- % 12 typecount(M, Pol, A, V). typecount(M, Pol, nL A, V) :- % 13 typecount(M, Pol, A, V). typecount(M, Pol, nM A, V) :- % 14 typecount(M, Pol, A, V). typecount(M, Pol, ab A, [C1|V]) :- % 15 typecount(M, Pol, A, [C|V]), minus(C, 1, C1). typecount(M, Pol, br A, [C1|V]) :- % 16 typecount(M, Pol, A, [C|V]), plus(C, 1, C1). typecount(max, inp, ue A, [top|V]) :- % 17 typecount(max, inp, A, [_|U]), xmap(U, V). typecount(min, inp, ue A, V) :- typecount(min, inp, A, U), ymap(U, V). typecount(M, out, ue A, V) :- typecount(M, out, A, V). typecount(max, out, ee A, V) :- % 18 typecount(max, out, A, U), xmap(U, V). typecount(min, out, ee A, V) :- typecount(min, out, A, U), ymap(U, V). typecount(M, inp, ee A, V) :- typecount(M, inp, A, V). typecount(max, out, _ een A, V) :- typecount(max, out, A, U), xmap(U, V). typecount(min, out, _ een A, V) :- typecount(min, out, A, U), ymap(U, V). typecount(M, inp, _ een A, V) :- typecount(M, inp, A, V). typecount(M, P, B lca _, V) :- % 19 typecount(M, P, B, V). typecount(_, _, w(_), [0, 0, 0, 0, 0, 0, 0, 0]). % 20 typecount(M, Pol, C lio B, V) :- % 21 typecount(M, Pol, C, V1), comp(Pol, Pol1), comp(M, M1), typecount(M1, Pol1, B, V2), listminus(V1, V2, V). typecount(M, Pol, A liu C, V) :- % 22 typecount(M, Pol, C, V1), comp(Pol, Pol1), comp(M, M1), typecount(M1, Pol1, A, V2), listminus(V1, V2, V). typecount(M, Pol, C rio B, V) :- % 23 typecount(M, Pol, C, V1), comp(Pol, Pol1), comp(M, M1), typecount(M1, Pol1, B, V2), listminus(V1, V2, V). typecount(M, Pol, A riu C, V) :- % 24 typecount(M, Pol, C, V1), comp(Pol, Pol1), comp(M, M1), typecount(M1, Pol1, A, V2), listminus(V1, V2, V). typecount(M, Pol, A lip B, V) :- % 25 typecount(M, Pol, A, V1), typecount(M, Pol, B, V2), listplus(V1, V2, V). typecount(M, Pol, A rip B, V) :- % 26 typecount(M, Pol, A, V1), typecount(M, Pol, B, V2), listplus(V1, V2, V). typecount(M, Pol, C uic B, V) :- % 27+ typecount(M, Pol, C, V1), comp(Pol, Pol1), comp(M, M1), typecount(M1, Pol1, B, V2), listminus(V1, V2, V). typecount(M, Pol, C uicn B, V) :- % 27- typecount(M, Pol, C, V1), comp(Pol, Pol1), comp(M, M1), typecount(M1, Pol1, B, V2), listminus(V1, V2, V). typecount(M, Pol, A uii C, V) :- % 28+ typecount(M, Pol, C, V1), comp(Pol, Pol1), comp(M, M1), typecount(M1, Pol1, A, V2), listminus(V1, V2, V). typecount(M, Pol, A uiin C, V) :- % 28- typecount(M, Pol, C, V1), comp(Pol, Pol1), comp(M, M1), typecount(M1, Pol1, A, V2), listminus(V1, V2, V). typecount(M, Pol, C lic B, V) :- % 29+ typecount(M, Pol, C, V1), comp(Pol, Pol1), comp(M, M1), typecount(M1, Pol1, B, V2), listminus(V1, V2, V). typecount(M, Pol, C licn B, V) :- % 29- typecount(M, Pol, C, V1), comp(Pol, Pol1), comp(M, M1), typecount(M1, Pol1, B, V2), listminus(V1, V2, V). typecount(M, Pol, A lii C, V) :- % 30+ typecount(M, Pol, C, V1), comp(Pol, Pol1), comp(M, M1), typecount(M1, Pol1, A, V2), listminus(V1, V2, V). typecount(M, Pol, A liin C, V) :- % 30- typecount(M, Pol, C, V1), comp(Pol, Pol1), comp(M, M1), typecount(M1, Pol1, A, V2), listminus(V1, V2, V). typecount(M, Pol, A uidp B, V) :- % 31+ typecount(M, Pol, A, V1), typecount(M, Pol, B, V2), listplus(V1, V2, V). typecount(M, Pol, A uidpn B, V) :- % 31- typecount(M, Pol, A, V1), typecount(M, Pol, B, V2), listplus(V1, V2, V). typecount(M, Pol, A lidp B, V) :- % 32+ typecount(M, Pol, A, V1), typecount(M, Pol, B, V2), listplus(V1, V2, V). typecount(M, Pol, A lidpn B, V) :- % 32- typecount(M, Pol, A, V1), typecount(M, Pol, B, V2), listplus(V1, V2, V). typecount(M, out, A iac B, V) :- % 33 typecount(M, out, A, V1), typecount(M, out, B, V2), comp(M, M1), listm(M1, V1, V2, V). typecount(M, inp, A iac B, V) :- typecount(M, inp, A, V1), typecount(M, inp, B, V2), listm(M, V1, V2, V). typecount(M, out, A iad B, V) :- % 34 typecount(M, out, A, V1), typecount(M, out, B, V2), listm(M, V1, V2, V). typecount(M, inp, A iad B, V) :- typecount(M, inp, A, V1), typecount(M, inp, B, V2), comp(M, M1), listm(M1, V1, V2, V). typecount(M, Pol, _ iu A, V) :- % 35 typecount(M, Pol, A, V). typecount(M, Pol, _ ie A, V) :- % 36 typecount(M, Pol, A, V). typecount(M, Pol, iL A, V) :- % 37 typecount(M, Pol, A, V). typecount(M, Pol, iM A, V) :- % 38 typecount(M, Pol, A, V). typecount(M, Pol, lp A, V) :- % 39 typecount(M, Pol, A, V). typecount(M, Pol, rp A, V) :- % 40 typecount(M, Pol, A, V). typecount(M, Pol, li A, V) :- % 41 typecount(M, Pol, A, V). typecount(M, Pol, ri A, V) :- % 42 typecount(M, Pol, A, V). typecount(M, Pol, sp A, V) :- % 43+ typecount(M, Pol, A, V). typecount(M, Pol, spn A, V) :- % 43- typecount(M, Pol, A, V). typecount(M, Pol, bg A, V) :- % 44+ typecount(M, Pol, A, V). typecount(M, Pol, bgn A, V) :- % 44- typecount(M, Pol, A, V). typecount(M, Pol, C nd B, V) :- % 45 typecount(M, Pol, C, V1), comp(Pol, Pol1), comp(M, M1), typecount(M1, Pol1, B, V2), listminus(V1, V2, V). typecount(M, Pol, A np B, V) :- % 46 typecount(M, Pol, A, V1), typecount(M, Pol, B, V2), listplus(V1, V2, V). typecount(M, Pol, C nci B, V) :- % 47 typecount(M, Pol, C, V1), comp(Pol, Pol1), comp(M, M1), typecount(M1, Pol1, B, V2), listminus(V1, V2, V). typecount(M, Pol, A nin C, V) :- % 48 typecount(M, Pol, C, V1), comp(Pol, Pol1), comp(M, M1), typecount(M1, Pol1, A, V2), listminus(V1, V2, V). typecount(M, Pol, A ndp B, V) :- % 49 typecount(M, Pol, A, V1), typecount(M, Pol, B, V2), listplus(V1, V2, V). typecount(M, P, B - _, V) :- % 50 typecount(M, P, B, V). xmap([], []). xmap([C|V], [top|V1]) :- mgzero(C), xmap(V, V1). xmap([C|V], [C|V1]) :- mlezero(C), xmap(V, V1). ymap([], []). ymap([C|V], [C|V1]) :- mgezero(C), ymap(V, V1). ymap([C|V], [bot|V1]) :- mlzero(C), ymap(V, V1). listm(_, [], [], []). listm(M, [C1|V1], [C2|V2], [C|V]) :- m(M, C1, C2, C), listm(M, V1, V2, V). m(min, topbot, _, bot) :- (!). m(min, _, topbot, bot) :- (!). m(min, bot, _, bot) :- (!). m(min, _, bot, bot) :- (!). m(min, top, C, C) :- (!). m(min, C, top, C) :- (!). m(min, C1, C2, C1) :- integer(C1), integer(C2), C1 =< C2, (!). m(min, C1, C2, C2) :- integer(C1), integer(C2), C2 < C1. m(max, topbot, _, top) :- (!). m(max, _, topbot, top) :- (!). m(max, top, _, top) :- (!). m(max, _, top, top) :- (!). m(max, bot, C, C) :- (!). m(max, C, bot, C) :- (!). m(max, C1, C2, C1) :- integer(C1), integer(C2), C1 >= C2. m(max, C1, C2, C2) :- integer(C1), integer(C2), C2 > C1. lposex([C|V], [C1|V1]) :- posex(C, C1), lposex(V, V1). lposex([], []) :- (!). posex(N, top) :- integer(N), N > 0, (!). posex(C, C). lnegex([C|V], [C1|V1]) :- negex(C, C1), lnegex(V, V1). lnegex([], []) :- (!). negex(N, bot) :- integer(N), N < 0, (!). negex(C, C). configcount(_, [], [0, 0, 0, 0, 0, 0, 0, 0]). configcount(M, [1|Gamma], V) :- configcount(M, Gamma, V). configcount(M, [l(A, _, Ls)|Gamma], V) :- ltypecount(M, A, Ls, V1), configcount(M, Gamma, V2), listplus(V1, V2, V). configcount(M, [f(A, _, Ls)|Gamma], V) :- ltypecount(M, A, Ls, V1), configcount(M, Gamma, V2), listplus(V1, V2, V). configcount(M, [b(Zeta: Gamma)|Gamma1], [C1|V]) :- stoupcount(M, Zeta, V1), configcount(M, Gamma, V2), listplus(V1, V2, V3), configcount(M, Gamma1, V4), listplus(V3, V4, [C|V]), plus(C, 1, C1). ltypecount(M, A, Ls, V) :- typecount(M, inp, A, V1), configlstcount(M, Ls, V2), listplus(V1, V2, V). configlstcount(_, [], [0, 0, 0, 0, 0, 0, 0, 0]). configlstcount(M, [L|Ls], V) :- configcount(M, L, V1), configlstcount(M, Ls, V2), listplus(V1, V2, V). listminus([], [], []). listminus([X|N], [Y|M], [Z|P]) :- minus(X, Y, Z), listminus(N, M, P). minus(I, J, K) :- integer(I), integer(J), K is I-J. minus(I, bot, top) :- integer(I). minus(I, top, bot) :- integer(I). minus(I, topbot, topbot) :- integer(I). minus(bot, J, bot) :- integer(J). minus(bot, bot, topbot). minus(bot, top, bot). minus(bot, topbot, topbot). minus(top, J, top) :- integer(J). minus(top, bot, top). minus(top, top, topbot). minus(top, topbot, topbot). minus(topbot, J, topbot) :- integer(J). minus(topbot, bot, topbot). minus(topbot, top, topbot). minus(topbot, topbot, topbot). listplus([], [], []). listplus([X|N], [Y|M], [Z|P]) :- plus(X, Y, Z), listplus(N, M, P). plus(I, J, K) :- integer(I), integer(J), K is I+J. plus(I, bot, bot) :- integer(I). plus(I, top, top) :- integer(I). plus(I, topbot, topbot) :- integer(I). plus(bot, J, bot) :- integer(J). plus(bot, bot, bot). plus(bot, top, topbot). plus(bot, topbot, topbot). plus(top, J, top) :- integer(J). plus(top, bot, topbot). plus(top, top, top). plus(top, topbot, topbot). plus(topbot, J, topbot) :- integer(J). plus(topbot, bot, topbot). plus(topbot, top, topbot). plus(topbot, topbot, topbot). % pone(+Zone, ?SuccPhi, -Premises, -Prf) means that Zone => Succ is proved with semantics % Phi with a reversible rule last if Premises can be proved, and the proof is Prf. pone([]: [l(A, Phi, [])], l(A, Phi), [], prf(id, []: [l(A, Phi, [])], l(A), [])) :- primitive(A, []). pone([]: [l(A, Phi, [[1]])], l(A, Phi), [], prf(id, []: [l(A, Phi, [[1]])], l(A), [])) :- primitive(A, [1]). % 1 pone(Zeta: Gamma, l(C/B, [lmd, Y, Chi]), [Zeta: GammaB => l(C, Chi): SubPrf], prf(right(over), Zeta: Gamma, l(C/B), [SubPrf])) :- vector(B, Y, Bvec), append(Gamma, [Bvec], GammaB). % 2 pone(Zeta: Gamma, l(A bs C, [lmd, X, Chi]), [Zeta: [Avec|Gamma] => l(C, Chi): SubPrf], prf(right(under), Zeta: Gamma, l(A bs C), [SubPrf])) :- vector(A, X, Avec). % 3 pone(OMEGA, l(D, Omega), [OMEGAPr => l(D, Omega): SubPrf], prf(left(product), OMEGA, l(D), [SubPrf])) :- subconfigofzoneandapp(OMEGA, OMEGAPr, H, Deltal, [l(A*B, Chi, Ls)], Deltar), ssort(A, S), kappend(S, Ls1, Ls2, Ls), append(Deltal, [l(A, [fst, Chi], Ls1), l(B, [snd, Chi], Ls2)|Deltar], H). % 4 pone(OMEGA, l(A, Phi), [OMEGAPr => l(A, Phi): SubPrf], prf(left(productunit), OMEGA, l(A), [SubPrf])) :- subconfigofzoneandapp(OMEGA, OMEGAPr, H, Deltal, [l(i, _, [])], Deltar), append(Deltal, Deltar, H). % 5+ pone(Zeta: Gamma, l(C ci B, [lmd, Y, Chi]), [Zeta: GammaPr => l(C, Chi): SubPrf], prf(right(circumfix), Zeta: Gamma, l(C ci B), [SubPrf])) :- vector(B, Y, Bvec), configsort(Gamma, S), do_ones(S, [[1]|Ls]), fold(S, Gamma, [[Bvec]|Ls], GammaPr). % 5- pone(Zeta: Gamma, l(C cin B, [lmd, Y, Chi]), [Zeta: GammaPr => l(C, Chi): SubPrf], prf(right(circumfixn), Zeta: Gamma, l(C cin B), [SubPrf])) :- vector(B, Y, Bvec), configsort(Gamma, S), do_ones(S, [[1]|Ls]), append(Ls, [[Bvec]], LsB), fold(S, Gamma, LsB, GammaPr). % 6+ pone(Zeta: Gamma, l(A in C, [lmd, X, Chi]), [Zeta: GammaPr => l(C, Chi): SubPrf], prf(right(infix), Zeta: Gamma, l(A in C), [SubPrf])) :- vector(A, X, Avec), ssort(A, S), do_ones(S, [[1]|Ls]), fold(S, Avec, [[Gamma]|Ls], GammaPr). % 6- pone(Zeta: Gamma, l(A inn C, [lmd, X, Chi]), [Zeta: GammaPr => l(C, Chi): SubPrf], prf(right(infixn), Zeta: Gamma, l(A in C), [SubPrf])) :- vector(A, X, Avec), ssort(A, S), do_ones(S, [[1]|Ls]), append(Ls, Gamma, LsGamma), fold(S, Avec, LsGamma, GammaPr). % 7+ pone(OMEGA, l(D, Omega), [OMEGAPr => l(D, Omega): SubPrf], prf(left(dprod), OMEGA, l(D), [SubPrf])) :- subconfigofzoneandapp(OMEGA, OMEGAPr, H, Deltal, [l(A dp B, Chi, Ls)], Deltar), ssort(B, S), kappend(S, Ls1, Ls2, Ls), append(Deltal, [l(A, [fst, Chi], [[l(B, [snd, Chi], Ls1)]|Ls2])|Deltar], H). % 7- pone(OMEGA, l(D, Omega), [OMEGAPr => l(D, Omega): SubPrf], prf(left(dprodn), OMEGA, l(D), [SubPrf])) :- subconfigofzoneandapp(OMEGA, OMEGAPr, H, Deltal, [l(A dpn B, Chi, Ls)], Deltar), ssort(B, S), kappend(S, Ls1, Ls2, Ls), append(Ls2, [[l(B, [snd, Chi], Ls1)]], Ls2B), append(Deltal, [l(A, [fst, Chi], Ls2B)|Deltar], H). % 8 pone(OMEGA, l(A, Phi), [OMEGAPr => l(A, Phi): SubPrf], prf(left(dproductunit), OMEGA, l(A), [SubPrf])) :- subconfigofzoneandapp(OMEGA, OMEGAPr, H, Deltal, [l(j, _, [Gamma])], Deltar), nappend([Deltal, Gamma, Deltar], H). % 9 pone(OMEGA, l(A&B, [pair, Phi, Psi]), [OMEGA => l(A, Phi): SubPrf1, OMEGA => l(B, Psi): SubPrf2], prf(right(aconj), OMEGA, l(A&B), [SubPrf1, SubPrf2])). % 10 pone(OMEGA, l(C, [case, Chi, X, Chi1, Y, Chi2]), [OMEGAPr1 => l(C, Chi1): SubPrf1, OMEGAPr2 => l(C, Chi2): SubPrf2], prf(left(adisj), OMEGA, l(C), [SubPrf1, SubPrf2])) :- leafofsubconfigofzone(OMEGA, OMEGAPr, xxx, l(A+B, Chi, Ls)), leafofsubconfigofzone(OMEGAPr, OMEGAPr1, l(A, X, Ls), xxx), leafofsubconfigofzone(OMEGAPr, OMEGAPr2, l(B, Y, Ls), xxx). % 11 pone(OMEGA, l(V u A, [lmd, V, Phi]), [OMEGA => l(A1, Phi): SubPrf], prf(right(univq), OMEGA, l(V u A), [SubPrf])) :- gensymb(S), tsubst(S, V, A, A1). % 12 pone(OMEGA, l(B, Psi), [OMEGAPr => l(B, Psi): SubPrf], prf(left(exstq), OMEGA, l(B), [SubPrf])) :- leafofsubconfigofzone(OMEGA, OMEGAPr, l(A1, X, Ls), l(V e A, [snd, X], Ls)), gensymb(S), tsubst(S, V, A, A1). % 13 pone(OMEGA, l(nL A, [up, Phi]), [OMEGA => l(A, Phi): SubPrf], prf(right(umod), OMEGA, l(nL A), [SubPrf])) :- allumodszone(OMEGA). % 14 pone(OMEGA, l(nM B, Psi), [OMEGAPr => l(nM B, Psi): SubPrf], prf(left(emod), OMEGA, l(nM B), [SubPrf])) :- leafofsubconfigofzone(OMEGA, OMEGAPr, H, l(nM A, Chi, Ls)), allumodszone(OMEGAPr), H = l(A, [cup, Chi], Ls). % 15 pone([]: Gamma, l(ab A, Phi), [[]: [[]: b(Gamma)] => l(A, Phi): SubPrf], prf(right(abrack), []: Gamma, l(ab A), [SubPrf])). % 16 pone(OMEGA, l(B, Psi), [OMEGAPr => l(B, Psi): SubPrf], prf(left(brack), OMEGA, l(B), [SubPrf])) :- leafofsubconfigofzone(OMEGA, OMEGAPr, b([]: [l(A, Phi, Ls)]), l(br A, Phi, Ls)). % 17 pone([B]: [], l(ue A, Phi), [[B]: [] => l(A, Phi): SubPrf], prf(right(uexp), [B]: [], l(ue A), [SubPrf])). pone(Zeta: GammaAGamma, l(B, Psi), [[l(A, Phi, [])|Zeta]: GammaGamma => l(B, Psi): SubPrf], prf(left(uexp), Zeta: GammaAGamma, l(B), [SubPrf])) :- append(Gamma1, [l(ue A, Phi, [])|Gamma2], GammaAGamma), append(Gamma1, Gamma2, GammaGamma). % 20 pone(OMEGA, l(A, Phi), [OMEGAPr => l(A, Phi): SubPrf], prf(left(words), OMEGA, l(A), [SubPrf])) :- subconfigofzoneandapp(OMEGA, OMEGAPr, H, Deltal, [l(w([]), _, [])], Deltar), append(Deltal, Deltar, H). % 21 pone(Zeta: Gamma, l(C lio B, 0), [Zeta: GammaB => _: SubPrf], prf(right(liover), Zeta: Gamma, l(C lio B), [SubPrf])) :- vector(B, _, Bvec), append(Gamma, [Bvec], GammaB). % 22 pone(Zeta: Gamma, l(A liu C, Chi), [Zeta: [Avec|Gamma] => l(C, Chi): SubPrf], prf(right(liunder), Zeta: Gamma, l(A liu C), [SubPrf])) :- vector(A, _, Avec). % 23 pone(Zeta: Gamma, l(C rio B, Chi), [Zeta: GammaB => l(C, Chi): SubPrf], prf(right(riover), Zeta: Gamma, l(C rio B), [SubPrf])) :- vector(B, _, Bvec), append(Gamma, [Bvec], GammaB). % 24 pone(Zeta: Gamma, l(A riu C, 0), [Zeta: [Avec|Gamma] => l(C, _): SubPrf], prf(right(riunder), Zeta: Gamma, l(A riu C), [SubPrf])) :- vector(A, _, Avec). % 25 pone(OMEGA, l(D, Omega), [OMEGAPr => l(D, Omega): SubPrf], prf(left(liproduct), OMEGA, l(D), [SubPrf])) :- subconfigofzoneandapp(OMEGA, OMEGAPr, H, Deltal, [l(A lip B, Chi, Ls)], Deltar), ssort(A, S), kappend(S, Ls1, Ls2, Ls), append(Deltal, [l(A, _, Ls1), l(B, Chi, Ls2)|Deltar], H). % 26 pone(OMEGA, l(D, Omega), [OMEGAPr => l(D, Omega): SubPrf], prf(left(riproduct), OMEGA, l(D), [SubPrf])) :- subconfigofzoneandapp(OMEGA, OMEGAPr, H, Deltal, [l(A rip B, Chi, Ls)], Deltar), ssort(A, S), kappend(S, Ls1, Ls2, Ls), append(Deltal, [l(A, Chi, Ls1), l(B, _, Ls2)|Deltar], H). % 27+ pone(Zeta: Gamma, l(C uic B, Chi), [Zeta: GammaPr => l(C, Chi): SubPrf], prf(right(uicircum), Zeta: Gamma, l(C uic B), [SubPrf])) :- vector(B, _, Bvec), configsort(Gamma, S), do_ones(S, [[1]|Ls]), fold(S, Gamma, [[Bvec]|Ls], GammaPr). % 27- pone(Zeta: Gamma, l(C uicn B, Chi), [Zeta: GammaPr => l(C, Chi): SubPrf], prf(right(uicircumn), Zeta: Gamma, l(C uicn B), [SubPrf])) :- vector(B, _, Bvec), configsort(Gamma, S), do_ones(S, [[1]|Ls]), append(Ls, [[Bvec]], LsB), fold(S, Gamma, LsB, GammaPr). % 28+ pone(Zeta: Gamma, l(A uii C, 0), [Zeta: GammaPr => l(C, _): SubPrf], prf(right(uiinfix), Zeta: Gamma, l(A uii C), [SubPrf])) :- vector(A, _, Avec), ssort(A, S), do_ones(S, [[1]|Ls]), fold(S, Avec, [[Gamma]|Ls], GammaPr). % 28- pone(Zeta: Gamma, l(A uiin C, 0), [Zeta: GammaPr => l(C, _): SubPrf], prf(right(uiinfixn), Zeta: Gamma, l(A uiin C), [SubPrf])) :- vector(A, _, Avec), ssort(A, S), do_ones(S, [[1]|Ls]), append(Ls, Gamma, LsGamma), fold(S, Avec, LsGamma, GammaPr). % 29+ pone(Zeta: Gamma, l(C lic B, Chi), [Zeta: GammaPr => l(C, Chi): SubPrf], prf(right(licircum), Zeta: Gamma, l(C lic B), [SubPrf])) :- vector(B, _, Bvec), configsort(Gamma, S), do_ones(S, [[1]|Ls]), fold(S, Gamma, [[Bvec]|Ls], GammaPr). % 29- pone(Zeta: Gamma, l(C licn B, Chi), [Zeta: GammaPr => l(C, Chi): SubPrf], prf(right(licircumn), Zeta: Gamma, l(C licn B), [SubPrf])) :- vector(B, _, Bvec), configsort(Gamma, S), do_ones(S, [[1]|Ls]), append(Ls, [[Bvec]], LsB), fold(S, Gamma, LsB, GammaPr). % 30+ pone(Zeta: Gamma, l(A lii C, 0), [Zeta: GammaPr => l(C, 0): SubPrf], prf(right(liinfix), Zeta: Gamma, l(A lii C), [SubPrf])) :- vector(A, _, Avec), ssort(A, S), do_ones(S, [[1]|Ls]), fold(S, Avec, [[Gamma]|Ls], GammaPr). % 30- pone(Zeta: Gamma, l(A liin C, 0), [Zeta: GammaPr => l(C, 0): SubPrf], prf(right(liinfixn), Zeta: Gamma, l(A liin C), [SubPrf])) :- vector(A, _, Avec), ssort(A, S), do_ones(S, [[1]|Ls]), append(Ls, Gamma, LsGamma), fold(S, Avec, LsGamma, GammaPr). % 31+ pone(OMEGA, l(D, Omega), [OMEGAPr => l(D, Omega): SubPrf], prf(left(uidprod), OMEGA, l(D), [SubPrf])) :- subconfigofzoneandapp(OMEGA, OMEGAPr, H, Deltal, [l(A uidp B, Chi, Ls)], Deltar), ssort(B, S), kappend(S, Ls1, Ls2, Ls), append(Deltal, [l(A, _, [[l(B, Chi, Ls1)]|Ls2])|Deltar], H). % 31- pone(OMEGA, l(D, Omega), [OMEGAPr => l(D, Omega): SubPrf], prf(left(uidprodn), OMEGA, l(D), [SubPrf])) :- subconfigofzoneandapp(OMEGA, OMEGAPr, H, Deltal, [l(A uidpn B, Chi, Ls)], Deltar), ssort(B, S), kappend(S, Ls1, Ls2, Ls), append(Ls2, [[l(B, Chi, Ls1)]], Ls2B), append(Deltal, [l(A, _, Ls2B)|Deltar], H). % 32+ pone(OMEGA, l(D, Omega), [OMEGAPr => l(D, Omega): SubPrf], prf(left(lidprod), OMEGA, l(D), [SubPrf])) :- subconfigofzoneandapp(OMEGA, OMEGAPr, H, Deltal, [l(A lidp B, Chi, Ls)], Deltar), ssort(B, S), kappend(S, Ls1, Ls2, Ls), append(Deltal, [l(A, Chi, [[l(B, _, Ls1)]|Ls2])|Deltar], H). % 32- pone(OMEGA, l(D, Omega), [OMEGAPr => l(D, Omega): SubPrf], prf(left(lidprodn), OMEGA, l(D), [SubPrf])) :- subconfigofzoneandapp(OMEGA, OMEGAPr, H, Deltal, [l(A dpn B, Chi, Ls)], Deltar), ssort(B, S), kappend(S, Ls1, Ls2, Ls), append(Ls2, [[l(B, _, Ls1)]], Ls2B), append(Deltal, [l(A, Chi, Ls2B)|Deltar], H). % 33 pone(OMEGA, l(A iac B, Chi), [OMEGA => l(A, Chi): SubPrf1, OMEGA => l(B, Chi): SubPrf2], prf(right(iaconj), OMEGA, l(A iac B), [SubPrf1, SubPrf2])). % 34 pone(OMEGA, l(C, Chi), [OMEGAPr1 => l(C, Chi): SubPrf1, OMEGAPr2 => l(C, Chi): SubPrf2], prf(left(iadisj), OMEGA, l(C), [SubPrf1, SubPrf2])) :- leafofsubconfigofzone(OMEGA, OMEGAPr, xxx, l(A iad B, Z, Ls)), leafofsubconfigofzone(OMEGAPr, OMEGAPr1, l(A, Z, Ls), xxx), leafofsubconfigofzone(OMEGAPr, OMEGAPr2, l(B, Z, Ls), xxx). % 35 pone(OMEGA, l(V iu A, Phi), [OMEGA => l(A1, Phi): SubPrf], prf(right(iunivq), OMEGA, l(V iu A), [SubPrf])) :- gensymb(S), tsubst(S, V, A, A1). % 36 pone(OMEGA, l(B, Psi), [OMEGAPr => l(B, Psi): SubPrf], prf(left(iexstq), OMEGA, l(B), [SubPrf])) :- leafofsubconfigofzone(OMEGA, OMEGAPr, l(A1, X, Ls), l(V ie A, X, Ls)), gensymb(S), tsubst(S, V, A, A1). % 37 pone(OMEGA, l(iL A, Phi), [OMEGA => l(A, Phi): SubPrf], prf(right(iumod), OMEGA, l(iL A), [SubPrf])) :- allumodszone(OMEGA). % 38 pone(OMEGA, l(iM B, Psi), [OMEGAPr => l(iM B, Psi): SubPrf], prf(left(uemod), OMEGA, l(iM B), [SubPrf])) :- leafofsubconfigofzone(OMEGA, OMEGAPr, H, l(iM A, Chi, Ls)), allumodszone(OMEGAPr), H = l(A, Chi, Ls). % 39 pone(Zeta: Gamma, l(lp A, Phi), [Zeta: Gamma1 => l(A, Phi): SubPrf], prf(right(lproj), Zeta: Gamma, l(lp A), [SubPrf])) :- append(Gamma, [1], Gamma1). % 40 pone(Zeta: Gamma, l(rp A, Phi), [Zeta: [1|Gamma] => l(A, Phi): SubPrf], prf(right(rproj), Zeta: Gamma, l(rp A), [SubPrf])). % 41 pone(OMEGA, l(B, Psi), [OMEGAPr => l(B, Psi): SubPrf], prf(left(linj), OMEGA, l(B), [SubPrf])) :- subconfigofzoneandapp(OMEGA, OMEGAPr, H, Deltal, [l(li A, Phi, Ls)], Deltar), append(Deltal, [l(A, Phi, Ls), 1|Deltar], H). % 42 pone(OMEGA, l(B, Psi), [OMEGAPr => l(B, Psi): SubPrf], prf(left(rinj), OMEGA, l(B), [SubPrf])) :- subconfigofzoneandapp(OMEGA, OMEGAPr, H, Deltal, [l(ri A, Phi, Ls)], Deltar), append(Deltal, [1, l(A, Phi, Ls)|Deltar], H). % 43+ pone(Zeta: Delta, l(sp B, Psi), [Zeta: DeltaPr => l(B, Psi): SubPrf], prf(right(split), Zeta: Delta, l(sp B), [SubPrf])) :- configsort(Delta, [1|S]), do_ones(S, Ls), fold([1|S], Delta, [[]|Ls], DeltaPr). % 43- pone(Zeta: Delta, l(spn B, Psi), [Zeta: DeltaPr => l(B, Psi): SubPrf], prf(right(splitn), Zeta: Delta, l(spn B), [SubPrf])) :- configsort(Delta, [1|S]), do_ones(S, Ls), append(Ls, [[]], Lss), fold([1|S], Delta, Lss, DeltaPr). % 44+ pone(OMEGA, l(C, Chi), [OMEGAPr => l(C, Chi): SubPrf], prf(left(bridge), OMEGA, l(C), [SubPrf])) :- leafofsubconfigofzone(OMEGA, OMEGAPr, l(B, Psi, [[]|Ls]), l(bg B, Psi, Ls)). % 44- pone(OMEGA, l(C, Chi), [OMEGAPr => l(C, Chi): SubPrf], prf(left(bridgen), OMEGA, l(C), [SubPrf])) :- leafofsubconfigofzone(OMEGA, OMEGAPr, l(B, Psi, Lss), l(bgn B, Psi, Ls)), append(Ls, [[]], Lss). % 45 pone(Zeta: Gamma, l(C nd A, [lmd, X, Chi]), [Zeta: [Avec|Gamma] => l(C, Chi): SubPrf1, Zeta: GammaA => l(C, Chi): SubPrf2], prf(right(ndiv), Zeta: Gamma, l(C nd A), [SubPrf1, SubPrf2])) :- vector(A, X, Avec), append(Gamma, [Avec], GammaA). % 46 pone(OMEGA, l(D, Omega), [OMEGAPr => l(D, Omega): SubPrf1, OMEGAPrPr => l(D, Omega): SubPrf2], prf(left(nprod), OMEGA, l(D), [SubPrf1, SubPrf2])) :- subconfigofzoneandapp(OMEGA, OMEGAPr, H, Deltal, [l(A np B, Chi, LsALsB)], Deltar), makecopy((OMEGAPr, H, Deltal, Deltar), (OMEGAPrPr, HPr, DeltalPr, DeltarPr)), ssort(A, SA), kappend(SA, LsA, LsB, LsALsB), append(Deltal, [l(A, [fst, Chi], LsA), l(B, [snd, Chi], LsB)|Deltar], H), append(DeltalPr, [l(B, [snd, Chi], LsB), l(A, [fst, Chi], LsA)|DeltarPr], HPr). % 47 pone(Zeta: Gamma, l(C nci B, [lmd, Y, Chi]), [Zeta: GammaPr => l(C, Chi): SubPrf1, Zeta: GammaPrPr => l(C, Chi): SubPrf2], prf(right(ninfix), Zeta: Gamma, l(C nci B), [SubPrf1, SubPrf2])) :- vector(B, Y, Bvec), configsort(Gamma, [1|S]), do_ones(S, Ls), fold(Gamma, [1|S], [[Bvec]|Ls], GammaPr), append(Ls, [[Bvec]], LsB), fold(Gamma, [1|S], LsB, GammaPrPr). % 48 pone(Zeta: Gamma, l(A nin C, [lmd, X, Chi]), [Zeta: GammaPr => l(C, Chi): SubPrf1, Zeta: GammaPrPr => l(C, Chi): SubPrf2], prf(right(ninfix), Zeta: Gamma, l(A nin C), [SubPrf1, SubPrf2])) :- vector(A, X, Avec), ssort(A, [1|S]), do_ones(S, Ls), fold([Avec], [1|S], [Gamma|Ls], GammaPr), append(Ls, Gamma, LsGamma), fold([Avec], [1|S], LsGamma, GammaPrPr). % 49 pone(OMEGA, l(D, Omega), [OMEGAPr => l(D, Omega): SubPrf1, OMEGAPrPr => l(D, Omega): SubPrf2], prf(left(ndprod), OMEGA, l(D), [SubPrf1, SubPrf2])) :- subconfigofzoneandapp(OMEGA, OMEGAPr, H, Deltal, [l(A ndp B, Chi, Ls)], Deltar), makecopy((OMEGAPr, H, Deltal, Deltar), (OMEGAPrPr, HPr, DeltalPr, DeltarPr)), ssort(B, SB), kappend(SB, Ls1B, Ls1A, Ls), append(Deltal, [l(A, [fst, Chi], [l(B, [snd, Chi], Ls1B)|Ls1A])|Deltar], H), ssort(A, [1|S]), kappend(S, Ls2A, Ls2B, Ls), append(Ls2A, [[l(B, [snd, Chi], Ls2B)]], Lss), append(DeltalPr, [l(A, [fst, Chi], Lss)|DeltarPr], HPr). makecopy(X, Y) :- assert(copy(X)), retract(copy(Y)). % ssort(+A, -SA) means that type A is of sort SA where sort n % is represented as a list of n 1's. ssort(P, SP) :- primitive(P, SP). ssort(C/B, S) :- % 1 ssort(B, S1), ssort(C, S2), append(S, S1, S2). ssort(A bs C, S) :- % 2 ssort(A, S1), ssort(C, S2), append(S1, S, S2). ssort(A*B, S) :- % 3 ssort(A, S1), ssort(B, S2), append(S1, S2, S). ssort(i, []). % 4 ssort(C ci B, [1|S]) :- % 5+ ssort(B, S1), ssort(C, S2), append(S, S1, S2). ssort(C cin B, [1|S]) :- % 5- ssort(B, S1), ssort(C, S2), append(S, S1, S2). ssort(A in C, S) :- % 6+ ssort(A, [1|S1]), ssort(C, S2), append(S1, S, S2). ssort(A inn C, S) :- % 6- ssort(A, [1|S1]), ssort(C, S2), append(S1, S, S2). ssort(A dp B, S) :- % 7+ ssort(A, [1|S1]), ssort(B, S2), append(S1, S2, S). ssort(A dpn B, S) :- % 7- ssort(A, [1|S1]), ssort(B, S2), append(S1, S2, S). ssort(j, [1]). % 8 ssort(A&B, S) :- % 9 ssort(A, S), ssort(B, S). ssort(A+B, S) :- % 10 ssort(A, S), ssort(B, S). ssort(_ u A, S) :- % 11 ssort(A, S). ssort(_ e A, S) :- % 12 ssort(A, S). ssort(nL A, S) :- % 13 ssort(A, S). ssort(nM A, S) :- % 14 ssort(A, S). ssort(ab A, S) :- % 15 ssort(A, S). ssort(br A, S) :- % 16 ssort(A, S). ssort(ue A, []) :- % 17 ssort(A, []). ssort(ee A, []) :- % 18 ssort(A, []). ssort(_ een A, []) :- ssort(A, []). ssort(B lca A, S) :- % 19 ssort(B, S), ssort(A, SPr), append(SPr, _, S). ssort(w(_), []). % 20 ssort(C lio B, S) :- % 21 ssort(B, S1), ssort(C, S2), append(S, S1, S2). ssort(A liu C, S) :- % 22 ssort(A, S1), ssort(C, S2), append(S1, S, S2). ssort(C rio B, S) :- % 23 ssort(B, S1), ssort(C, S2), append(S, S1, S2). ssort(A riu C, S) :- % 24 ssort(A, S1), ssort(C, S2), append(S1, S, S2). ssort(A lip B, S) :- % 25 ssort(A, S1), ssort(B, S2), append(S1, S2, S). ssort(A rip B, S) :- % 26 ssort(A, S1), ssort(B, S2), append(S1, S2, S). ssort(C uic B, [1|S]) :- % 27+ ssort(B, S1), ssort(C, S2), append(S, S1, S2). ssort(C uicn B, [1|S]) :- % 27- ssort(B, S1), ssort(C, S2), append(S, S1, S2). ssort(A uii C, S) :- % 28+ ssort(A, [1|S1]), ssort(C, S2), append(S1, S, S2). ssort(A uiin C, S) :- % 28- ssort(A, [1|S1]), ssort(C, S2), append(S1, S, S2). ssort(C lic B, [1|S]) :- % 29+ ssort(B, S1), ssort(C, S2), append(S, S1, S2). ssort(C licn B, [1|S]) :- % 29- ssort(B, S1), ssort(C, S2), append(S, S1, S2). ssort(A lii C, S) :- % 30+ ssort(A, [1|S1]), ssort(C, S2), append(S1, S, S2). ssort(A liin C, S) :- % 30- ssort(A, [1|S1]), ssort(C, S2), append(S1, S, S2). ssort(A uidp B, S) :- % 31+ ssort(A, [1|S1]), ssort(B, S2), append(S1, S2, S). ssort(A uidpn B, S) :- % 31- ssort(A, [1|S1]), ssort(B, S2), append(S1, S2, S). ssort(A lidp B, S) :- % 32+ ssort(A, [1|S1]), ssort(B, S2), append(S1, S2, S). ssort(A lidpn B, S) :- % 32- ssort(A, [1|S1]), ssort(B, S2), append(S1, S2, S). ssort(A iac B, S) :- % 33 ssort(A, S), ssort(B, S). ssort(A iad B, S) :- % 34 ssort(A, S), ssort(B, S). ssort(_ iu A, S) :- % 35 ssort(A, S). ssort(_ ie A, S) :- % 36 ssort(A, S). ssort(iL A, S) :- % 37 ssort(A, S). ssort(iM A, S) :- % 38 ssort(A, S). ssort(lp A, S) :- % 39 ssort(A, [1|S]). ssort(rp A, S) :- % 40 ssort(A, [1|S]). ssort(li A, [1|S]) :- % 41 ssort(A, S). ssort(ri A, [1|S]) :- % 42 ssort(A, S). ssort(sp A, [1|S]) :- % 43+ ssort(A, S). ssort(spn A, [1|S]) :- % 43- ssort(A, S). ssort(bg A, S) :- % 44+ ssort(A, [1|S]). ssort(bgn A, S) :- % 44- ssort(A, [1|S]). ssort(B nd A, S) :- % 45 ssort(A, S1), ssort(B, S2), append(S1, S, S2). ssort(A np B, S) :- % 46 ssort(A, S1), ssort(B, S2), append(S1, S2, S). ssort(C nci B, [1|S]) :- % 47 ssort(B, S1), ssort(C, S2), append(S, S1, S2). ssort(A nin C, S) :- % 48 ssort(A, [1|S1]), ssort(C, S2), append(S1, S, S2). ssort(A ndp B, S) :- % 49 ssort(A, [1|S1]), ssort(B, S2), append(S1, S2, S). ssort(A-B, S) :- % 50 ssort(A, S), ssort(B, S). % subconfigandapp(+Delta, -DeltaPr, -H, -Deltal, -Ls, -Deltar) means that configuration Delta % can be analysed into DeltaPr(Deltal, Ls, Deltar) where variable H is a leaf in % DeltaPr marking the position of maximal subconfiguration Deltal, Ls, Deltar in Delta subconfigandapp(Delta, DeltaPr, H, Deltal, Ls, Deltar) :- subconfig(Delta, DeltaPr, H, Gamma), nappend([Deltal, Ls, Deltar], Gamma). % subconfigofzoneandapp(+Zeta, -ZetaPr, -H, -Deltal, -Ls, -Deltar) means that zone Zeta % can be analysed into ZetaPr(Deltal, Ls, Deltar) where variable H is a leaf in % ZetaPr marking the position of maximal subconfiguration Deltal, Ls, Deltar in Zeta subconfigofzoneandapp(Zeta, ZetaPr, H, Deltal, Ls, Deltar) :- subconfigofzone(Zeta, ZetaPr, H, Delta), nappend([Deltal, Ls, Deltar], Delta). % subconfig(+Delta, -DeltaPr, -H, -Gamma) means that % configuration Delta can be analysed into DeltaPr(Gamma) % where H is a leaf variable in DeltaPr marking the % position of subconfiguration Gamma in Zeta. subconfig(Delta, H, H, Delta). subconfig(Delta, Delta1, H, Delta2) :- append(Deltaleft, [l(X, Phi, Lss)|Deltaright], Delta), append(L1, [Ls|L2], Lss), subconfig(Ls, LsPr, H, Delta2), append(L1, [LsPr|L2], LssPr), append(Deltaleft, [l(X, Phi, LssPr)|Deltaright], Delta1). subconfig(Delta, Delta1, H, Delta2) :- append(Deltaleft, [b(Zeta)|Deltaright], Delta), subconfigofzone(Zeta, ZetaPr, H, Delta2), append(Deltaleft, [b(ZetaPr)|Deltaright], Delta1). % leafofsubconfig(+Delta, -DeltaPr, -H, ?L) means that configuration Delta can be % analysed into DeltaPr(L) where H is a leaf variable in DeltaPr marking the % position of leaf L in Delta leafofsubconfig(Delta, DeltaPr, H, L) :- subconfigandapp(Delta, DeltaPr, H1, Deltal, [L], Deltar), append(Deltal, [H|Deltar], H1). % leafofsubconfigofzone(+Zeta, -ZetaPr, -H, ?L) means that zone Zeta can be % analysed into ZetaPr(L) where H is a leaf variable in ZetaPr marking the % position of leaf L in Delta leafofsubconfigofzone(Omega: Delta, Omega: DeltaPr, H, L) :- subconfigandapp(Delta, DeltaPr, H1, Deltal, [L], Deltar), append(Deltal, [H|Deltar], H1). % subconfigofzoneP(+Zeta, -ZetaPr, H, Delta) means that Zeta can be analysed into % ZetaPr(Delta) where variable H is a leaf in ZetaPr marking the position of % maximal subconfiguration Delta in Zeta subconfigofzone(Omega: Delta, Omega: DeltaPr, H, Gamma) :- subconfig(Delta, DeltaPr, H, Gamma). % subzoneandapp(+Zeta, -ZetaPr, -H, -Stoup, L1, L2, L3) means that zone Zeta can be % analyzed into ZetaPr(Stoup: L1, L2, L3) where variable H in ZetaPr marks the % position of subzone Stoup: L1, L2, L3 subzoneandapp(Zeta, ZetaPr, H, Stoup, L1, L2, L3) :- subzone(Zeta, ZetaPr, H, Stoup: Lss), nappend([L1, L2, L3], Lss). % subzone(+Zeta, -ZetaPr, -H, -ZetaPrPr) means that zone Zeta can be analysed % into ZetaPr(ZetaPrPr) where H is a variable in ZetaPr marking the position of % subzone ZetaPrPr in Zeta subzone(Zeta, H, H, Zeta). subzone(Omega: Delta, Omega: DeltaPr, H, Zeta) :- subzoneofconfig(Delta, DeltaPr, H, Zeta). % subzoneofconfig(+Delta, -DeltaPr, -H, -Zeta) means that configuration Delta % can be analysed into DeltaPr(Zeta) where variable H is a leaf in DeltaPr % marking the position of subzone Zeta in Delta subzoneofconfig(Delta, DeltaPr, H, Zeta) :- append(Deltal, [l(A, Phi, Lss)|Deltar], Delta), append(Ls1, [Ls|Ls2], Lss), subzoneofconfig(Ls, LsPr, H, Zeta), append(Ls1, [LsPr|Ls2], LssPr), append(Deltal, [l(A, Phi, LssPr)|Deltar], DeltaPr). subzoneofconfig(Delta, DeltaPr, H, Zeta) :- append(Deltal, [b(ZetaPr)|Deltar], Delta), subzone(ZetaPr, ZetaPrPr, H, Zeta), append(Deltal, [b(ZetaPrPr)|Deltar], DeltaPr). % vector(+A, +Phi, -Avec) means that Avec is the vector of type A with semantics Phi vector(A, Phi, l(A, Phi, Ls)) :- ssort(A, S), do_ones(S, Ls). % do_ones(+S, -Ls) means that where S is a sort in unary notation, % Ls is the list of singleton lists of separators of the same length. do_ones([],[]). do_ones([1|L], [[1]|L1]) :- do_ones(L, L1). % nappend(?Ls, ?L) means that L is the concatenation of the % list of lists Ls. nappend([], []). nappend([[]|Ls], L) :- nappend(Ls, L). nappend([[H|L1]|Ls], [H|L]) :- nappend([L1|Ls], L). % partition(+L, -L1, -L2) means that L1 and L2 are a partition of L partition([], [], []). partition([H|T], [H|T1], T2) :- partition(T, T1, T2). partition([H|T], T1, [H|T2]) :- partition(T, T1, T2). % p1(+OMEGA, +APhi, -Prf) means that OMEGA => APhi is provable with proof Prf p1(OMEGA, l(A, Phi), Prf) :- countcheck(OMEGA, A), p1lst([OMEGA => l(A, Phi): Prf], L), p2lst(L). % p1lst(+L1, -L2) means that the list of sequents L1 unfolds don't care % nondeterministically to the list of sequents L2 by reversible/"phase 1" % rules p1lst([], []). p1lst([OMEGA => APhiPrf|L], LPrPr) :- leafofsubconfigofzone(OMEGA, _, _, l(w(W), _, _)), var(W), (!), (W = []; W = [_|_]), p1lst([OMEGA => APhiPrf|L], LPrPr). p1lst([OMEGA => APhi: Prf|L], LPrPr) :- pone(OMEGA, APhi, Ls, Prf), (!), append(Ls, L, LPr), p1lst(LPr, LPrPr). p1lst([H|T], [H|L]) :- p1lst(T, L). % p2lst(+L) means that the sequents of list L are provable starting with % irreversible/“phase 2" rules p2lst([]). p2lst([OMEGA => APhi: Prf|L]) :- p2(OMEGA, APhi, Prf), p2lst(L). % p2(+OMEGA, +DOmega, -Prf) means that sequent OMEGA => DOmega is derivable with % proof Prf p2(OMEGA, l(D, Omega), Prf) :- countcheck(OMEGA, D), p2aux(OMEGA, l(D, Omega), Prf). p2aux(OMEGA, l(A, Phi), Prf) :- p2r(OMEGA, f(A, Phi), Prf). p2aux(OMEGA, DOmega, Prf) :- subzone(OMEGA, OMEGAPr, StoupPr: Delta, [H|T]: Delta), append(Stoup1, [l(A, Phi, [])|Stoup2], [H|T]), append(Stoup1, [f(A, Phi, [])|Stoup2], StoupPr), p2s(OMEGAPr, DOmega, Prf). p2aux(OMEGA, DOmega, Prf) :- leafofsubconfigofzone(OMEGA, OMEGAPr, f(A, Phi, Ls), l(A, Phi, Ls)), p2l(A, OMEGAPr, DOmega, Prf). % p2l(+A, +OMEGA, -DOmega -Prf) means that sequent OMEGA => DOmega, in which type A is % focused in its configuration, is provable with proof Prf p2l(A, []: [f(A, Phi, [])], l(A, Phi), prf(id, []: [f(A, Phi, [])], l(A), [])) :- atfoc(inp), primitive(A, []), (!). p2l(A, []: [f(A, Phi, [[1]])], l(A, Phi), prf(id, []: [f(A, Phi, [[1]])], l(A), [])) :- atfoc(inp), primitive(A, [1]), (!). % 1 p2l(P/Q, OMEGA, l(D, Omega), prf(left(over), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, inp), pos(Q, out), ssort(Q, SQ), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(P/Q, Psi, Ls2)|Ls], Deltar), partition(Stoup, Stoup1, Stoup2), fold(SQ, Gamma, Ls1, Ls), p2r(Stoup1: Gamma, f(Q, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(P, [app, Psi, Phi], Lss)|Deltar], Delta), p2l(P, OMEGAPr, l(D, Omega), SubPrf2). p2l(P/N, OMEGA, l(D, Omega), prf(left(over), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, inp), neg(N, out), ssort(N, SN), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(P/N, Psi, Ls2)|Ls], Deltar), partition(Stoup, Stoup1, Stoup2), fold(SN, Gamma, Ls1, Ls), p1(Stoup1: Gamma, l(N, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(P, [app, Psi, Phi], Lss)|Deltar], Delta), p2l(P, OMEGAPr, l(D, Omega), SubPrf2). p2l(N/P, OMEGA, l(D, Omega), prf(left(over), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(N, inp), pos(P, out), ssort(P, SP), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(N/P, Psi, Ls2)|Ls], Deltar), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma, Ls1, Ls), p2r(Stoup1: Gamma, f(P, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(N, [app, Psi, Phi], Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(N/M, OMEGA, l(D, Omega), prf(left(over), OMEGA, l(D), [SubPrf1, SubPrf2])) :- (!), neg(N, inp), neg(M, out), ssort(M, SM), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(N/M, Psi, Ls2)|Ls], Deltar), partition(Stoup, Stoup1, Stoup2), fold(SM, Gamma, Ls1, Ls), p1(Stoup1: Gamma, l(M, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(N, [app, Psi, Phi], Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). % 2 p2l(P bs Q, OMEGA, l(D, Omega), prf(left(under), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, out), pos(Q, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, LsB, Deltar), append(Ls, [f(P bs Q, Psi, Ls2)], LsB), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma, Ls1, Ls), p2r(Stoup1: Gamma, f(P, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(Q, [app, Psi, Phi], Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(P bs N, OMEGA, l(D, Omega), prf(left(under), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, out), neg(N, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, LsB, Deltar), append(Ls, [f(P bs N, Psi, Ls2)], LsB), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma, Ls1, Ls), p2r(Stoup1: Gamma, f(P, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(N, [app, Psi, Phi], Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(N bs P, OMEGA, l(D, Omega), prf(left(under), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(N, out), pos(P, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, LsB, Deltar), append(Ls, [f(N bs P, Psi, Ls2)], LsB), ssort(N, SN), partition(Stoup, Stoup1, Stoup2), fold(SN, Gamma, Ls1, Ls), p1(Stoup1: Gamma, l(N, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(P, [app, Psi, Phi], Lss)|Deltar], Delta), p2l(P, OMEGAPr, l(D, Omega), SubPrf2). p2l(N bs M, OMEGA, l(D, Omega), prf(left(under), OMEGA, l(D), [SubPrf1, SubPrf2])) :- (!), neg(N, out), neg(N, inp), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, LsB, Deltar), append(Ls, [f(N bs M, Psi, Ls2)], LsB), ssort(N, SN), partition(Stoup, Stoup1, Stoup2), fold(SN, Gamma, Ls1, Ls), p1(Stoup1: Gamma, l(N, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(M, [app, Psi, Phi], Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). % 5+ p2l(Q ci P, OMEGA, l(D, Omega), prf(left(circumfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), pos(P, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(Q ci P, Phi, [Gamma|Gammas])], Deltar), (!), partition(Stoup, Stoup1, Stoup2), p2r(Stoup1: Gamma, f(P, Psi), SubPrf1), ssort(P, SP), do_ones(SP, Ls), append(Ls, Gammas, LsGammas), append(Deltal, [f(Q, [app, Phi, Psi], LsGammas)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(Q ci N, OMEGA, l(D, Omega), prf(left(circumfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), neg(N, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(Q ci N, Phi, [Gamma|Gammas])], Deltar), (!), partition(Stoup, Stoup1, Stoup2), p1(Stoup1: Gamma, l(N, Psi), SubPrf1), ssort(N, SN), do_ones(SN, Ls), append(Ls, Gammas, LsGammas), append(Deltal, [f(Q, [app, Phi, Psi], LsGammas)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(M ci P, OMEGA, l(D, Omega), prf(left(circumfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(M, inp), pos(P, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(M ci P, Phi, [Gamma|Gammas])], Deltar), (!), partition(Stoup, Stoup1, Stoup2), p2r(Stoup1: Gamma, f(P, Psi), SubPrf1), ssort(P, SP), do_ones(SP, Ls), append(Ls, Gammas, LsGammas), append(Deltal, [l(M, [app, Phi, Psi], LsGammas)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(M ci N, OMEGA, l(D, Omega), prf(left(circumfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(M, inp), neg(N, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(M ci N, Phi, [Gamma|Gammas])], Deltar), (!), partition(Stoup, Stoup1, Stoup2), p1(Stoup1: Gamma, l(N, Psi), SubPrf1), ssort(N, SN), do_ones(SN, Ls), append(Ls, Gammas, LsGammas), append(Deltal, [l(M, [app, Phi, Psi], LsGammas)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). % 5- p2l(Q cin P, OMEGA, l(D, Omega), prf(left(circumfixn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), pos(P, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(Q cin P, Phi, GammasGamma)], Deltar), append(Gammas, [Gamma], GammasGamma), (!), partition(Stoup, Stoup1, Stoup2), p2r(Stoup1: Gamma, f(P, Psi), SubPrf1), ssort(P, SP), do_ones(SP, Ls), append(Gammas, Ls, GammasLs), append(Deltal, [f(Q, [app, Phi, Psi], GammasLs)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(Q cin N, OMEGA, l(D, Omega), prf(left(circumfixn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), neg(N, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(Q cin N, Phi, GammasGamma)], Deltar), append(Gammas, [Gamma], GammasGamma), (!), partition(Stoup, Stoup1, Stoup2), p1(Stoup1: Gamma, l(N, Psi), SubPrf1), ssort(N, SN), do_ones(SN, Ls), append(Gammas, Ls, GammasLs), append(Deltal, [f(Q, [app, Phi, Psi], GammasLs)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(M cin P, OMEGA, l(D, Omega), prf(left(circumfixn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(M, inp), pos(P, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(M cin P, Phi, GammasGamma)], Deltar), append(Gammas, [Gamma], GammasGamma), (!), partition(Stoup, Stoup1, Stoup2), p2r(Stoup1: Gamma, f(P, Psi), SubPrf1), ssort(P, SP), do_ones(SP, Ls), append(Gammas, Ls, GammasLs), append(Deltal, [l(M, [app, Phi, Psi], GammasLs)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(M cin N, OMEGA, l(D, Omega), prf(left(circumfixn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(M, inp), neg(N, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(M cin N, Phi, GammasGamma)], Deltar), append(Gammas, [Gamma], GammasGamma), (!), partition(Stoup, Stoup1, Stoup2), p1(Stoup1: Gamma, l(N, Psi), SubPrf1), ssort(N, SN), do_ones(SN, Ls), append(Gammas, Ls, GammasLs), append(Deltal, [l(M, [app, Phi, Psi], GammasLs)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). % 6+ p2l(P in Q, OMEGA, l(D, Omega), prf(left(infix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, out), pos(Q, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, [f(P in Q, Psi, Ls1)|_], [], L), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma2, [[1]|Ls2], Gamma1), p2r(Stoup1: Gamma2, f(P, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(Q, [app, Psi, Phi], Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(P in M, OMEGA, l(D, Omega), prf(left(infix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, out), neg(M, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, [f(P in M, Psi, Ls1)|_], [], L), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma2, [[1]|Ls2], Gamma1), p2r(Stoup1: Gamma2, f(P, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(M, [app, Psi, Phi], Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(N in Q, OMEGA, l(D, Omega), prf(left(infix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(N, out), pos(Q, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, [f(N in Q, Psi, Ls1)|_], [], L), ssort(N, SN), partition(Stoup, Stoup1, Stoup2), fold(SN, Gamma2, [[1]|Ls2], Gamma1), p1(Stoup1: Gamma2, l(N, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(Q, [app, Psi, Phi], Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(N in M, OMEGA, l(D, Omega), prf(left(infix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- (!), neg(N, out), neg(M, inp), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, [f(N in M, Psi, Ls1)|_], [], L), ssort(N, SN), partition(Stoup, Stoup1, Stoup2), fold(SN, Gamma2, [[1]|Ls2], Gamma1), p1(Stoup1: Gamma2, l(N, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(M, [app, Psi, Phi], Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). % 6- p2l(P inn Q, OMEGA, l(D, Omega), prf(left(infixn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, out), pos(Q, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, Ls, [], L), append(_, [f(P inn Q, Psi, Ls1)], Ls), ssort(P, [1|N]), kappend(N, Ls2, [[1]], Ls3), partition(Stoup, Stoup1, Stoup2), fold([1|N], Gamma2, Ls3, Gamma1), p2r(Stoup1: Gamma2, f(P, Phi), SubPrf1), append(Ls2, Ls1, Lss), append(Deltal, [f(Q, [app, Psi, Phi], Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(P inn M, OMEGA, l(D, Omega), prf(left(infixn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, out), neg(M, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, Ls, [], L), append(_, [f(P inn M, Psi, Ls1)], Ls), ssort(P, [1|N]), partition(Stoup, Stoup1, Stoup2), kappend(N, Ls2, [[1]], Ls3), fold([1|N], Gamma2, Ls3, Gamma1), p2r(Stoup1: Gamma2, f(P, Phi), SubPrf1), append(Ls2, Ls1, Lss), append(Deltal, [l(M, [app, Psi, Phi], Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(N inn Q, OMEGA, l(D, Omega), prf(left(infixn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(N, out), pos(Q, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, Ls, [], L), append(_, [f(N inn Q, Psi, Ls1)], Ls), ssort(N, [1|NN]), kappend(NN, Ls2, [[1]], Ls3), partition(Stoup, Stoup1, Stoup2), fold([1|NN], Gamma2, Ls3, Gamma1), p1(Stoup1: Gamma2, l(N, Phi), SubPrf1), append(Ls2, Ls1, Lss), append(Deltal, [f(Q, [app, Psi, Phi], Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(N inn M, OMEGA, l(D, Omega), prf(left(infixn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- (!), neg(N, out), neg(M, inp), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, Ls, [], L), append(_, [f(N inn M, Psi, Ls1)], Ls), ssort(N, [1|NN]), kappend(NN, Ls2, [[1]], Ls3), partition(Stoup, Stoup1, Stoup2), fold([1|NN], Gamma2, Ls3, Gamma1), p1(Stoup1: Gamma2, l(N, Phi), SubPrf1), append(Ls2, Ls1, Lss), append(Deltal, [l(M, [app, Psi, Phi], Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). % 9 p2l(Q&_, OMEGA, l(D, Omega), prf(left(aconj), OMEGA, l(D), [SubPrf])) :- pos(Q, inp), leafofsubconfigofzone(OMEGA, OMEGAPr, f(Q, [fst, Chi], Ls), f(Q&_, Chi, Ls)), p2l(Q, OMEGAPr, l(D, Omega), SubPrf). p2l(M&_, OMEGA, l(D, Omega), prf(left(aconj), OMEGA, l(D), [SubPrf])) :- neg(M, inp), leafofsubconfigofzone(OMEGA, OMEGAPr, l(M, [fst, Chi], Ls), f(M&_, Chi, Ls)), p1(OMEGAPr, l(D, Omega), SubPrf). p2l(_&Q, OMEGA, l(D, Omega), prf(left(aconj), OMEGA, l(D), [SubPrf])) :- pos(Q, inp), leafofsubconfigofzone(OMEGA, OMEGAPr, f(Q, [snd, Chi], Ls), f(_&Q, Chi, Ls)), (!), p2l(Q, OMEGAPr, l(D, Omega), SubPrf). p2l(_&M, OMEGA, l(D, Omega), prf(left(aconj), OMEGA, l(D), [SubPrf])) :- neg(M, inp), leafofsubconfigofzone(OMEGA, OMEGAPr, l(M, [snd, Chi], Ls), f(_&M, Chi, Ls)), (!), p1(OMEGAPr, l(D, Omega), SubPrf). % 11 p2l(V u Q, OMEGA, l(D, Omega), prf(left(univq), OMEGA, l(D), [SubPrf])) :- pos(Q, inp), leafofsubconfigofzone(OMEGA, OMEGAPr, f(QQ, [app, Chi, VV], Ls), f(V u Q, Chi, Ls)), tsubst(VV, V, Q, QQ), (!), p2l(QQ, OMEGAPr, l(D, Omega), SubPrf). p2l(V u M, OMEGA, l(D, Omega), prf(left(univq), OMEGA, l(D), [SubPrf])) :- neg(M, inp), leafofsubconfigofzone(OMEGA, OMEGAPr, l(MM, [app, Chi, VV], Ls), f(V u M, Chi, Ls)), tsubst(VV, V, M, MM), (!), p1(OMEGAPr, l(D, Omega), SubPrf). % 13 p2l(nL Q, OMEGA, l(D, Omega), prf(left(umod), OMEGA, l(D), [SubPrf])) :- pos(Q, inp), leafofsubconfigofzone(OMEGA, OMEGAPr, f(Q, [dn, Chi], Ls), f(nL Q, Chi, Ls)), (!), p2l(Q, OMEGAPr, l(D, Omega), SubPrf). p2l(nL M, OMEGA, l(D, Omega), prf(left(umod), OMEGA, l(D), [SubPrf])) :- neg(M, inp), leafofsubconfigofzone(OMEGA, OMEGAPr, l(M, [dn, Chi], Ls), f(nL M, Chi, Ls)), (!), p1(OMEGAPr, l(D, Omega), SubPrf). % 15 p2l(ab Q, OMEGA, l(D, Omega), prf(left(abrack), OMEGA, l(D), [SubPrf])) :- pos(Q, inp), subconfigofzoneandapp(OMEGA, OMEGAPr, H, Deltal, [b([]: [f(ab Q, Phi, Ls)])], Deltar), append(Deltal, [f(Q, Phi, Ls)|Deltar], H), (!), p2l(Q, OMEGAPr, l(D, Omega), SubPrf). p2l(ab M, OMEGA, l(D, Omega), prf(left(abrack), OMEGA, l(D), [SubPrf])) :- neg(M, inp), subconfigofzoneandapp(OMEGA, OMEGAPr, H, Deltal, [b([]: [f(ab M, Phi, Ls)])], Deltar), append(Deltal, [l(M, Phi, Ls)|Deltar], H), (!), p1(OMEGAPr, l(D, Omega), SubPrf). % 19 L p2l(Q lca P, Zeta: Delta, l(D, Omega), prf(left(a), Zeta: Delta, l(D), [MinSubPrf, MajSubPrf])) :- pos(Q, inp), pos(P, out), partition(Zeta, StoupMin, StoupMaj), an(Delta, Gamma, f(Q lca P, Chi, Ls), Theta, l(P, Phi, []), l(Q, [app, Chi, Phi], Ls)), p2r(StoupMin: Gamma, f(P, Phi), MinSubPrf), p1(StoupMaj: Theta, l(D, Omega), MajSubPrf). p2l(Q lca N, Zeta: Delta, l(D, Omega), prf(left(a), Zeta: Delta, l(D), [MinSubPrf, MajSubPrf])) :- pos(Q, inp), neg(N, out), partition(Zeta, StoupMin, StoupMaj), an(Delta, Gamma, f(Q lca N, Chi, Ls), Theta, l(N, Phi, []), l(Q, [app, Chi, Phi], Ls)), p1(StoupMin: Gamma, l(N, Phi), MinSubPrf), p1(StoupMaj: Theta, l(D, Omega), MajSubPrf). p2l(M lca P, Zeta: Delta, l(D, Omega), prf(left(a), Zeta: Delta, l(D), [MinSubPrf, MajSubPrf])) :- neg(M, inp), pos(P, out), partition(Zeta, StoupMin, StoupMaj), an(Delta, Gamma, f(M lca P, Chi, Ls), Theta, l(P, Phi, []), l(M, [app, Chi, Phi], Ls)), p2r(StoupMin: Gamma, f(P, Phi), MinSubPrf), p1(StoupMaj: Theta, l(D, Omega), MajSubPrf). p2l(M lca N, Zeta: Delta, l(D, Omega), prf(left(a), Zeta: Delta, l(D), [MinSubPrf, MajSubPrf])) :- neg(N, out), neg(M, inp), partition(Zeta, StoupMin, StoupMaj), an(Delta, Gamma, f(M lca N, Chi, Ls), Theta, l(N, Phi, []), l(M, [app, Chi, Phi], Ls)), p1(StoupMin: Gamma, f(N, Phi), MinSubPrf), p1(StoupMaj: Theta, l(D, Omega), MajSubPrf). % 19 R p2l(_ lca A, Stoup: Gamma, l(D lca A, [lmd, X, Psi]), prf(right(a), Stoup: Gamma, l(D lca A), [SubPrf])) :- abindoff(Gamma, A, X, Gamma1), p1(Stoup: Gamma1, l(D, Psi), SubPrf). % 21 p2l(Q lio P, OMEGA, l(D, Omega), prf(left(liover), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), pos(P, out), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(Q lio P, _, Ls2)|Ls], Deltar), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma, Ls1, Ls), p2r(Stoup1: Gamma, f(P, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(Q, 0, Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(Q lio N, OMEGA, l(D, Omega), prf(left(liover), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), neg(N, out), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(Q lio N, _, Ls2)|Ls], Deltar), ssort(N, SN), partition(Stoup, Stoup1, Stoup2), fold(SN, Gamma, Ls1, Ls), p1(Stoup1: Gamma, l(N, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(Q, 0, Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(M lio P, OMEGA, l(D, Omega), prf(left(liover), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(N, inp), pos(P, out), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(M lio P, _, Ls2)|Ls], Deltar), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma, Ls1, Ls), p2r(Stoup1: Gamma, f(P, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(N, 0, Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(N lio M, OMEGA, l(D, Omega), prf(left(liover), OMEGA, l(D), [SubPrf1, SubPrf2])) :- (!), neg(N, inp), neg(M, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(N lio M, _, Ls2)|Ls], Deltar), ssort(M, SM), partition(Stoup, Stoup1, Stoup2), fold(SM, Gamma, Ls1, Ls), p1(Stoup1: Gamma, l(M, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(N, 0, Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). % 22 p2l(P liu Q, OMEGA, l(D, Omega), prf(left(liunder), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, out), pos(Q, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, LsB, Deltar), append(Ls, [f(P liu Q, Psi, Ls2)], LsB), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma, Ls1, Ls), p2r(Stoup1: Gamma, f(P, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(Q, Psi, Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(P liu N, OMEGA, l(D, Omega), prf(left(liunder), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, out), neg(N, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, LsB, Deltar), append(Ls, [f(P liu N, Psi, Ls2)], LsB), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma, Ls1, Ls), p2r(Stoup1: Gamma, f(P, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(N, Psi, Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(N liu P, OMEGA, l(D, Omega), prf(left(liunder), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(N, out), pos(P, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, LsB, Deltar), append(Ls, [f(N liu P, Psi, Ls2)], LsB), ssort(N, SN), partition(Stoup, Stoup1, Stoup2), fold(SN, Gamma, Ls1, Ls), p1(Stoup1: Gamma, l(N, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(P, Psi, Lss)|Deltar], Delta), p2l(P, OMEGAPr, l(D, Omega), SubPrf2). p2l(N liu M, OMEGA, l(D, Omega), prf(left(liunder), OMEGA, l(D), [SubPrf1, SubPrf2])) :- (!), neg(N, out), neg(N, inp), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, LsB, Deltar), append(Ls, [f(N liu M, Psi, Ls2)], LsB), ssort(N, SN), partition(Stoup, Stoup1, Stoup2), fold(SN, Gamma, Ls1, Ls), p1(Stoup1: Gamma, l(N, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(M, Psi, Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). % 23 p2l(Q rio P, OMEGA, l(D, Omega), prf(left(riover), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), pos(P, out), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(Q rio P, Psi, Ls2)|Ls], Deltar), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma, Ls1, Ls), p2r(Stoup1: Gamma, f(P, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(Q, Psi, Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(Q rio N, OMEGA, l(D, Omega), prf(left(riover), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), neg(N, out), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(Q rio N, Psi, Ls2)|Ls], Deltar), ssort(N, SN), partition(Stoup, Stoup1, Stoup2), fold(SN, Gamma, Ls1, Ls), p1(Stoup1: Gamma, l(N, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(Q, Psi, Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(M rio P, OMEGA, l(D, Omega), prf(left(riover), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(M, inp), pos(P, out), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(M rio P, Psi, Ls2)|Ls], Deltar), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma, Ls1, Ls), p2r(Stoup1: Gamma, f(P, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(M, Psi, Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(N rio M, OMEGA, l(D, Omega), prf(left(riover), OMEGA, l(D), [SubPrf1, SubPrf2])) :- (!), neg(N, inp), neg(M, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(N rio M, Psi, Ls2)|Ls], Deltar), ssort(M, SM), partition(Stoup, Stoup1, Stoup2), fold(SM, Gamma, Ls1, Ls), p1(Stoup1: Gamma, l(M, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(N, Psi, Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). % 24 p2l(P riu Q, OMEGA, l(D, Omega), prf(left(riunder), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, out), pos(Q, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, LsB, Deltar), append(Ls, [f(P riu Q, _, Ls2)], LsB), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma, Ls1, Ls), p2r(Stoup1: Gamma, f(P, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(Q, 0, Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(P riu N, OMEGA, l(D, Omega), prf(left(riunder), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, out), neg(N, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, LsB, Deltar), append(Ls, [f(P riu N, _, Ls2)], LsB), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma, Ls1, Ls), p2r(Stoup1: Gamma, f(P, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(N, 0, Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(N riu P, OMEGA, l(D, Omega), prf(left(riunder), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(N, out), pos(P, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, LsB, Deltar), append(Ls, [f(N riu P, _, Ls2)], LsB), ssort(N, SN), partition(Stoup, Stoup1, Stoup2), fold(SN, Gamma, Ls1, Ls), p1(Stoup1: Gamma, l(N, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(P, 0, Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(N riu M, OMEGA, l(D, Omega), prf(left(riunder), OMEGA, l(D), [SubPrf1, SubPrf2])) :- (!), neg(N, out), neg(M, inp), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, LsB, Deltar), append(Ls, [f(N riu M, _, Ls2)], LsB), ssort(N, SN), partition(Stoup, Stoup1, Stoup2), fold(SN, Gamma, Ls1, Ls), p1(Stoup1: Gamma, l(N, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(M, 0, Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). % 25+ p2l(Q uic P, OMEGA, l(D, Omega), prf(left(uicircum), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), pos(P, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(Q uic P, Phi, [Gamma|Gammas])], Deltar), (!), partition(Stoup, Stoup1, Stoup2), p2r(Stoup1: Gamma, f(P, _), SubPrf1), ssort(P, SP), do_ones(SP, Ls), append(Ls, Gammas, LsGammas), append(Deltal, [f(Q, Phi, LsGammas)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(Q uic N, OMEGA, l(D, Omega), prf(left(uicircum), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), neg(N, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(Q uic N, Phi, [Gamma|Gammas])], Deltar), (!), partition(Stoup, Stoup1, Stoup2), p1(Stoup1: Gamma, l(N, _), SubPrf1), ssort(N, SN), do_ones(SN, Ls), append(Ls, Gammas, LsGammas), append(Deltal, [f(Q, Phi, LsGammas)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(M uic P, OMEGA, l(D, Omega), prf(left(uicircum), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(M, inp), pos(P, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(M uic P, Phi, [Gamma|Gammas])], Deltar), (!), partition(Stoup, Stoup1, Stoup2), p2r(Stoup1: Gamma, f(P, _), SubPrf1), ssort(P, SP), do_ones(SP, Ls), append(Ls, Gammas, LsGammas), append(Deltal, [l(M, Phi, LsGammas)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(M uic N, OMEGA, l(D, Omega), prf(left(uicircum), OMEGA, l(D), [SubPrf1, SubPrf2])) :- subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(M uic N, Phi, [Gamma|Gammas])], Deltar), (!), partition(Stoup, Stoup1, Stoup2), p1(Stoup1: Gamma, l(N, _), SubPrf1), ssort(N, SN), do_ones(SN, Ls), append(Ls, Gammas, LsGammas), append(Deltal, [l(M, Phi, LsGammas)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). % 25- p2l(Q uicn P, OMEGA, l(D, Omega), prf(left(uicircumn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), pos(P, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(Q uicn P, Phi, GammasGamma)], Deltar), append(Gammas, [Gamma], GammasGamma), (!), partition(Stoup, Stoup1, Stoup2), p2r(Stoup1: Gamma, f(P, _), SubPrf1), ssort(P, SP), do_ones(SP, Ls), append(Gammas, Ls, GammasLs), append(Deltal, [f(Q, Phi, GammasLs)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(Q uicn N, OMEGA, l(D, Omega), prf(left(uicircumn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), neg(N, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(Q uicn N, Phi, GammasGamma)], Deltar), append(Gammas, [Gamma], GammasGamma), (!), partition(Stoup, Stoup1, Stoup2), p1(Stoup1: Gamma, l(N, _), SubPrf1), ssort(N, SN), do_ones(SN, Ls), append(Gammas, Ls, GammasLs), append(Deltal, [f(Q, Phi, GammasLs)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(M uicn P, OMEGA, l(D, Omega), prf(left(uicircumn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(M, inp), pos(P, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(M uicn P, Phi, GammasGamma)], Deltar), append(Gammas, [Gamma], GammasGamma), (!), partition(Stoup, Stoup1, Stoup2), p2r(Stoup1: Gamma, f(P, _), SubPrf1), ssort(P, SP), do_ones(SP, Ls), append(Gammas, Ls, GammasLs), append(Deltal, [l(M, Phi, GammasLs)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(M uicn N, OMEGA, l(D, Omega), prf(left(uicircumn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(M, inp), neg(N, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(M uicn N, Phi, GammasGamma)], Deltar), append(Gammas, [Gamma], GammasGamma), (!), partition(Stoup, Stoup1, Stoup2), p1(Stoup1: Gamma, l(N, _), SubPrf1), ssort(N, SN), do_ones(SN, Ls), append(Gammas, Ls, GammasLs), append(Deltal, [l(M, Phi, GammasLs)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). % 26+ p2l(P uii Q, OMEGA, l(D, Omega), prf(left(uiinfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, out), pos(Q, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, [f(P uii Q, _, Ls1)|_], [], L), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma2, [[1]|Ls2], Gamma1), p2r(Stoup1: Gamma2, f(P, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(Q, 0, Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(P uii M, OMEGA, l(D, Omega), prf(left(uiinfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, out), neg(M, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, [f(P uii M, _, Ls1)|_], [], L), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma2, [[1]|Ls2], Gamma1), p2r(Stoup1: Gamma2, f(P, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(M, 0, Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(N uii Q, OMEGA, l(D, Omega), prf(left(uiinfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(N, out), pos(Q, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, [f(N uii Q, _, Ls1)|_], [], L), ssort(N, SN), partition(Stoup, Stoup1, Stoup2), fold(SN, Gamma2, [[1]|Ls2], Gamma1), p1(Stoup1: Gamma2, l(N, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(Q, 0, Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(N uii M, OMEGA, l(D, Omega), prf(left(uiinfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- (!), neg(N, out), neg(M, inp), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, [f(N uii M, Psi, Ls1)|_], [], L), ssort(N, SN), partition(Stoup, Stoup1, Stoup2), fold(SN, Gamma2, [[1]|Ls2], Gamma1), p1(Stoup1: Gamma2, l(N, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(M, [app, Psi, Phi], Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). % 26- p2l(P uiin Q, OMEGA, l(D, Omega), prf(left(uiinfixn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, out), pos(Q, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, Ls, [], L), append(_, [f(P uiin Q, _, Ls1)], Ls), ssort(P, [1|N]), kappend(N, Ls2, [[1]], Ls3), partition(Stoup, Stoup1, Stoup2), fold([1|N], Gamma2, Ls3, Gamma1), p2r(Stoup1: Gamma2, f(P, _), SubPrf1), append(Ls2, Ls1, Lss), append(Deltal, [f(Q, 0, Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(P uiin M, OMEGA, l(D, Omega), prf(left(uiinfixn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, out), neg(M, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, Ls, [], L), append(_, [f(P uiin M, _, Ls1)], Ls), ssort(P, [1|N]), kappend(N, Ls2, [[1]], Ls3), partition(Stoup, Stoup1, Stoup2), fold([1|N], Gamma2, Ls3, Gamma1), p2r(Stoup1: Gamma2, f(P, _), SubPrf1), append(Ls2, Ls1, Lss), append(Deltal, [l(M, 0, Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(N uiin Q, OMEGA, l(D, Omega), prf(left(uiinfixn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(N, out), pos(Q, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, Ls, [], L), append(_, [f(N uiin Q, _, Ls1)], Ls), ssort(N, [1|NN]), kappend(NN, Ls2, [[1]], Ls3), partition(Stoup, Stoup1, Stoup2), fold([1|NN], Gamma2, Ls3, Gamma1), p1(Stoup1: Gamma2, l(N, _), SubPrf1), append(Ls2, Ls1, Lss), append(Deltal, [f(Q, 0, Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(N uiin M, OMEGA, l(D, Omega), prf(left(uiinfixn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- (!), neg(N, out), neg(M, inp), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, Ls, [], L), append(_, [f(N uiin M, _, Ls1)], Ls), ssort(N, [1|NN]), kappend(NN, Ls2, [[1]], Ls3), partition(Stoup, Stoup1, Stoup2), fold([1|NN], Gamma2, Ls3, Gamma1), p1(Stoup1: Gamma2, l(N, _), SubPrf1), append(Ls2, Ls1, Lss), append(Deltal, [l(M, 0, Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). % 27+ p2l(Q lic P, OMEGA, l(D, Omega), prf(left(licircum), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), pos(P, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(Q lic P, Chi, [Gamma|Gammas])], Deltar), (!), partition(Stoup, Stoup1, Stoup2), p2r(Stoup1: Gamma, f(P, _), SubPrf1), ssort(P, SP), do_ones(SP, Ls), append(Ls, Gammas, LsGammas), append(Deltal, [f(Q, Chi, LsGammas)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(Q lic N, OMEGA, l(D, Omega), prf(left(licircum), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), neg(N, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(Q lic N, Chi, [Gamma|Gammas])], Deltar), (!), partition(Stoup, Stoup1, Stoup2), p1(Stoup1: Gamma, l(N, _), SubPrf1), ssort(N, SN), do_ones(SN, Ls), append(Ls, Gammas, LsGammas), append(Deltal, [f(Q, Chi, LsGammas)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(M lic P, OMEGA, l(D, Omega), prf(left(licircum), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(M, inp), pos(P, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(M lic P, Chi, [Gamma|Gammas])], Deltar), (!), partition(Stoup, Stoup1, Stoup2), p2r(Stoup1: Gamma, f(P, _), SubPrf1), ssort(P, SP), do_ones(SP, Ls), append(Ls, Gammas, LsGammas), append(Deltal, [l(M, Chi, LsGammas)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(N lic M, OMEGA, l(D, Omega), prf(left(licircum), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(N, inp), neg(M, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(N lic M, Chi, [Gamma|Gammas])], Deltar), (!), partition(Stoup, Stoup1, Stoup2), p1(Stoup1: Gamma, l(M, _), SubPrf1), ssort(M, SM), do_ones(SM, Ls), append(Ls, Gammas, LsGammas), append(Deltal, [l(N, Chi, LsGammas)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). % 27- p2l(Q licn P, OMEGA, l(D, Omega), prf(left(licircumn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), pos(P, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(Q licn P, Chi, GammasGamma)], Deltar), append(Gammas, [Gamma], GammasGamma), (!), partition(Stoup, Stoup1, Stoup2), p2r(Stoup1: Gamma, f(P, _), SubPrf1), ssort(P, SP), do_ones(SP, Ls), append(Gammas, Ls, GammasLs), append(Deltal, [f(Q, Chi, GammasLs)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(Q licn N, OMEGA, l(D, Omega), prf(left(licircumn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), neg(N, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(Q licn N, Chi, GammasGamma)], Deltar), append(Gammas, [Gamma], GammasGamma), partition(Stoup, Stoup1, Stoup2), p1(Stoup1: Gamma, l(N, _), SubPrf1), ssort(N, SN), do_ones(SN, Ls), append(Gammas, Ls, GammasLs), append(Deltal, [f(Q, Chi, GammasLs)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(M licn P, OMEGA, l(D, Omega), prf(left(licircumn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(M, inp), pos(P, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(M licn P, Chi, GammasGamma)], Deltar), append(Gammas, [Gamma], GammasGamma), (!), partition(Stoup, Stoup1, Stoup2), p2r(Stoup1: Gamma, f(P, _), SubPrf1), ssort(P, SP), do_ones(SP, Ls), append(Gammas, Ls, GammasLs), append(Deltal, [l(M, Chi, GammasLs)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(N licn M, OMEGA, l(D, Omega), prf(left(licircumn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(N, inp), neg(M, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(N licn M, Chi, GammasGamma)], Deltar), append(Gammas, [Gamma], GammasGamma), partition(Stoup, Stoup1, Stoup2), p1(Stoup1: Gamma, l(M, _), SubPrf1), ssort(M, SM), do_ones(SM, Ls), append(Gammas, Ls, GammasLs), append(Deltal, [l(N, Chi, GammasLs)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). % 28+ p2l(P lii Q, OMEGA, l(D, Omega), prf(left(liinfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, out), pos(Q, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, [f(P lii Q, _, Ls1)|_], [], L), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma2, [[1]|Ls2], Gamma1), p2r(Stoup1: Gamma2, f(P, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(Q, 0, Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(P lii M, OMEGA, l(D, Omega), prf(left(liinfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, out), neg(M, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, [f(P lii M, _, Ls1)|_], [], L), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma2, [[1]|Ls2], Gamma1), p2r(Stoup1: Gamma2, f(P, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(M, 0, Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(N lii Q, OMEGA, l(D, Omega), prf(left(liinfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, [f(N lii Q, _, Ls1)|_], [], L), neg(N, out), pos(Q, inp), ssort(N, SN), partition(Stoup, Stoup1, Stoup2), fold(SN, Gamma2, [[1]|Ls2], Gamma1), p1(Stoup1: Gamma2, l(N, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(Q, 0, Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(N lii M, OMEGA, l(D, Omega), prf(left(liinfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- (!), neg(N, out), neg(M, inp), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, [f(N lii M, _, Ls1)|_], [], L), ssort(N, SN), partition(Stoup, Stoup1, Stoup2), fold(SN, Gamma2, [[1]|Ls2], Gamma1), p1(Stoup1: Gamma2, l(N, _), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(M, 0, Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). % 28- p2l(P liin Q, OMEGA, l(D, Omega), prf(left(liinfixn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, out), pos(Q, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, Ls, [], L), append(_, [f(P liin Q, _, Ls1)], Ls), ssort(P, [1|N]), kappend(N, Ls2, [[1]], Ls3), partition(Stoup, Stoup1, Stoup2), fold([1|N], Gamma2, Ls3, Gamma1), p2r(Stoup1: Gamma2, f(P, _), SubPrf1), append(Ls2, Ls1, Lss), append(Deltal, [f(Q, 0, Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(P liin M, OMEGA, l(D, Omega), prf(left(liinfixn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, out), neg(M, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, Ls, [], L), append(_, [f(P liin M, _, Ls1)], Ls), ssort(P, [1|N]), kappend(N, Ls2, [[1]], Ls3), partition(Stoup, Stoup1, Stoup2), fold([1|N], Gamma2, Ls3, Gamma1), p2r(Stoup1: Gamma2, f(P, _), SubPrf1), append(Ls2, Ls1, Lss), append(Deltal, [l(M, 0, Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(N liin Q, OMEGA, l(D, Omega), prf(left(liinfixn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(N, out), pos(Q, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, Ls, [], L), append(_, [f(N liin Q, _, Ls1)], Ls), ssort(N, [1|NN]), kappend(NN, Ls2, [[1]], Ls3), partition(Stoup, Stoup1, Stoup2), fold([1|NN], Gamma2, Ls3, Gamma1), p1(Stoup1: Gamma2, l(N, _), SubPrf1), append(Ls2, Ls1, Lss), append(Deltal, [f(Q, 0, Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(N liin M, OMEGA, l(D, Omega), prf(left(liinfixn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- (!), neg(N, out), neg(M, inp), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, Ls, [], L), append(_, [f(N liin M, _, Ls1)], Ls), ssort(N, [1|NN]), kappend(NN, Ls2, [[1]], Ls3), partition(Stoup, Stoup1, Stoup2), fold([1|NN], Gamma2, Ls3, Gamma1), p1(Stoup1: Gamma2, l(N, _), SubPrf1), append(Ls2, Ls1, Lss), append(Deltal, [l(M, 0, Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). % 33 p2l(Q iac _, OMEGA, l(D, Omega), prf(left(iaconj), OMEGA, l(D), [SubPrf])) :- pos(Q, inp), leafofsubconfigofzone(OMEGA, OMEGAPr, f(Q, Chi, Ls), f(Q iac _, Chi, Ls)), p2l(Q, OMEGAPr, l(D, Omega), SubPrf). p2l(M iac _, OMEGA, l(D, Omega), prf(left(iaconj), OMEGA, l(D), [SubPrf])) :- neg(M, inp), leafofsubconfigofzone(OMEGA, OMEGAPr, l(M, Chi, Ls), f(M iac _, Chi, Ls)), p1(OMEGAPr, l(D, Omega), SubPrf). p2l(_ iac Q, OMEGA, l(D, Omega), prf(left(iaconj), OMEGA, l(D), [SubPrf])) :- pos(Q, inp), leafofsubconfigofzone(OMEGA, OMEGAPr, f(Q, Chi, Ls), f(_ iac Q, Chi, Ls)), (!), p2l(Q, OMEGAPr, l(D, Omega), SubPrf). p2l(_ iac M, OMEGA, l(D, Omega), prf(left(iaconj), OMEGA, l(D), [SubPrf])) :- neg(M, inp), leafofsubconfigofzone(OMEGA, OMEGAPr, l(M, Chi, Ls), f(_ iac M, Chi, Ls)), (!), p1(OMEGAPr, l(D, Omega), SubPrf). % 35 p2l(V iu Q, OMEGA, l(D, Omega), prf(left(iunivq), OMEGA, l(D), [SubPrf])) :- pos(Q, inp), leafofsubconfigofzone(OMEGA, OMEGAPr, f(QQ, Chi, Ls), f(V iu Q, Chi, Ls)), tsubst(_, V, Q, QQ), (!), p2l(QQ, OMEGAPr, l(D, Omega), SubPrf). p2l(V iu M, OMEGA, l(D, Omega), prf(left(iunivq), OMEGA, l(D), [SubPrf])) :- neg(M, inp), leafofsubconfigofzone(OMEGA, OMEGAPr, l(MM, Chi, Ls), f(V iu M, Chi, Ls)), tsubst(_, V, M, MM), (!), p1(OMEGAPr, l(D, Omega), SubPrf). % 37 p2l(iL Q, OMEGA, l(D, Omega), prf(left(iumod), OMEGA, l(D), [SubPrf])) :- pos(Q, inp), leafofsubconfigofzone(OMEGA, OMEGAPr, f(Q, Chi, Ls), f(iL Q, Chi, Ls)), (!), p2l(Q, OMEGAPr, l(D, Omega), SubPrf). p2l(iL M, OMEGA, l(D, Omega), prf(left(iumod), OMEGA, l(D), [SubPrf])) :- neg(M, inp), leafofsubconfigofzone(OMEGA, OMEGAPr, l(M, Chi, Ls), f(iL M, Chi, Ls)), (!), p1(OMEGAPr, l(D, Omega), SubPrf). % 39 p2l(lp Q, OMEGA, l(B, Psi), prf(left(lproj), OMEGA, l(B), [SubPrf])) :- pos(Q, inp), subconfigofzoneandapp(OMEGA, OMEGAPr, H, Deltal, [f(lp Q, Phi, Ls), 1], Deltar), append(Deltal, [f(Q, Phi, Ls)|Deltar], H), (!), p2l(Q, OMEGAPr, l(B, Psi), SubPrf). p2l(lp M, OMEGA, l(B, Psi), prf(left(lproj), OMEGA, l(B), [SubPrf])) :- neg(M, inp), subconfigofzoneandapp(OMEGA, OMEGAPr, H, Deltal, [f(lp M, Phi, Ls), 1], Deltar), append(Deltal, [l(M, Phi, Ls)|Deltar], H), (!), p1(OMEGAPr, l(B, Psi), SubPrf). % 40 p2l(rp Q, OMEGA, l(B, Psi), prf(left(rproj), OMEGA, l(B), [SubPrf])) :- pos(Q, inp), subconfigofzoneandapp(OMEGA, OMEGAPr, H, Deltal, [1, f(rp Q, Phi, Ls)], Deltar), append(Deltal, [f(Q, Phi, Ls)|Deltar], H), (!), p2l(Q, OMEGAPr, l(B, Psi), SubPrf). p2l(rp M, OMEGA, l(B, Psi), prf(left(rproj), OMEGA, l(B), [SubPrf])) :- neg(M, inp), subconfigofzoneandapp(OMEGA, OMEGAPr, H, Deltal, [1, f(rp M, Phi, Ls)], Deltar), append(Deltal, [l(M, Phi, Ls)|Deltar], H), (!), p1(OMEGAPr, l(B, Psi), SubPrf). % 43+ p2l(sp Q, OMEGA, l(C, Chi), prf(left(split), OMEGA, l(C), [SubPrf])) :- pos(Q, inp), leafofsubconfigofzone(OMEGA, OMEGAPr, f(Q, Psi, Ls), f(sp Q, Psi, [[]|Ls])), (!), p2l(Q, OMEGAPr, l(C, Chi), SubPrf). p2l(sp M, OMEGA, l(C, Chi), prf(left(split), OMEGA, l(C), [SubPrf])) :- neg(M, inp), leafofsubconfigofzone(OMEGA, OMEGAPr, l(M, Psi, Ls), f(sp M, Psi, [[]|Ls])), (!), p1(OMEGAPr, l(C, Chi), SubPrf). % 43- p2l(spn Q, OMEGA, l(C, Chi), prf(left(splitn), OMEGA, l(C), [SubPrf])) :- pos(Q, inp), leafofsubconfigofzone(OMEGA, OMEGAPr, f(Q, Psi, Ls), f(sp Q, Psi, LsLambda)), append(Ls, [[]], LsLambda), (!), p2l(Q, OMEGAPr, l(C, Chi), SubPrf). p2l(spn M, OMEGA, l(C, Chi), prf(left(splitn), OMEGA, l(C), [SubPrf])) :- neg(M, inp), leafofsubconfigofzone(OMEGA, OMEGAPr, l(M, Psi, Ls), f(sp M, Psi, LsLambda)), append(Ls, [[]], LsLambda), (!), p1(OMEGAPr, l(C, Chi), SubPrf). % 45 p2l(Q nd P, OMEGA, l(D, Omega), prf(left(ndiv), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), pos(P, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, LsB, Deltar), append(Ls, [f(Q nd P, Psi, Ls2)], LsB), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma, Ls1, Ls), p2r(Stoup1: Gamma, f(P, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(Q, [app, Psi, Phi], Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(Q nd N, OMEGA, l(D, Omega), prf(left(ndiv), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), neg(N, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, LsB, Deltar), append(Ls, [f(Q nd N, Psi, Ls2)], LsB), ssort(N, SN), partition(Stoup, Stoup1, Stoup2), fold(SN, Gamma, Ls1, Ls), p1(Stoup1: Gamma, l(N, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(Q, [app, Psi, Phi], Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(M nd P, OMEGA, l(D, Omega), prf(left(ndiv), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(M, inp), pos(P, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, LsB, Deltar), append(Ls, [f(M nd P, Psi, Ls2)], LsB), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma, Ls1, Ls), p2r(Stoup1: Gamma, f(P, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(M, [app, Psi, Phi], Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(M nd N, OMEGA, l(D, Omega), prf(left(ndiv), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(M, inp), neg(N, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, LsB, Deltar), append(Ls, [f(M nd N, Psi, Ls2)], LsB), ssort(N, SN), partition(Stoup, Stoup1, Stoup2), fold(SN, Gamma, Ls1, Ls), p1(Stoup1: Gamma, l(N, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(M, [app, Psi, Phi], Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(Q nd P, OMEGA, l(D, Omega), prf(left(ndiv), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), pos(P, out), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(Q nd P, Psi, Ls2)|Ls], Deltar), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma, Ls1, Ls), p2r(Stoup1: Gamma, f(P, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(Q, [app, Psi, Phi], Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(Q nd N, OMEGA, l(D, Omega), prf(left(ndiv), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), neg(N, out), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(Q nd N, Psi, Ls2)|Ls], Deltar), ssort(N, SN), partition(Stoup, Stoup1, Stoup2), fold(SN, Gamma, Ls1, Ls), p1(Stoup1: Gamma, l(N, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(Q, [app, Psi, Phi], Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(M nd P, OMEGA, l(D, Omega), prf(left(ndiv), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(M, inp), pos(P, out), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(M nd P, Psi, Ls2)|Ls], Deltar), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma, Ls1, Ls), p2r(Stoup1: Gamma, f(P, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(M, [app, Psi, Phi], Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(M nd N, OMEGA, l(D, Omega), prf(left(ndiv), OMEGA, l(D), [SubPrf1, SubPrf2])) :- (!), neg(N, inp), neg(M, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(M nd N, Psi, Ls2)|Ls], Deltar), ssort(N, SN), partition(Stoup, Stoup1, Stoup2), fold(SN, Gamma, Ls1, Ls), p1(Stoup1: Gamma, l(N, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(M, [app, Psi, Phi], Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). % 47 p2l(Q nci P, OMEGA, l(D, Omega), prf(left(ncircumfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), pos(P, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(Q nci P, Phi, [Gamma|Gammas])], Deltar), partition(Stoup, Stoup1, Stoup2), p2r(Stoup1: Gamma, f(P, Psi), SubPrf1), ssort(P, SP), do_ones(SP, Ls), append(Ls, Gammas, LsGammas), append(Deltal, [f(Q, [app, Phi, Psi], LsGammas)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(Q nci N, OMEGA, l(D, Omega), prf(left(ncircumfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), neg(N, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(Q nci N, Phi, [Gamma|Gammas])], Deltar), partition(Stoup, Stoup1, Stoup2), p1(Stoup1: Gamma, l(N, Psi), SubPrf1), ssort(N, SN), do_ones(SN, Ls), append(Ls, Gammas, LsGammas), append(Deltal, [f(Q, [app, Phi, Psi], LsGammas)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(M nci P, OMEGA, l(D, Omega), prf(left(ncircumfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(M, inp), pos(P, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(M nci P, Phi, [Gamma|Gammas])], Deltar), partition(Stoup, Stoup1, Stoup2), p2r(Stoup1: Gamma, f(P, Psi), SubPrf1), ssort(P, SP), do_ones(SP, Ls), append(Ls, Gammas, LsGammas), append(Deltal, [l(M, [app, Phi, Psi], LsGammas)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(M nci N, OMEGA, l(D, Omega), prf(left(ncircumfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(M, inp), neg(N, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(M nci N, Phi, [Gamma|Gammas])], Deltar), partition(Stoup, Stoup1, Stoup2), p1(Stoup1: Gamma, l(N, Psi), SubPrf1), ssort(N, SN), do_ones(SN, Ls), append(Ls, Gammas, LsGammas), append(Deltal, [l(M, [app, Phi, Psi], LsGammas)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(Q nci P, OMEGA, l(D, Omega), prf(left(ncircumfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), pos(P, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(Q nci P, Phi, GammasGamma)], Deltar), append(Gammas, [Gamma], GammasGamma), (!), partition(Stoup, Stoup1, Stoup2), p2r(Stoup1: Gamma, f(P, Psi), SubPrf1), ssort(P, SP), do_ones(SP, Ls), append(Gammas, Ls, GammasLs), append(Deltal, [f(Q, [app, Phi, Psi], GammasLs)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(Q nci N, OMEGA, l(D, Omega), prf(left(ncircumfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(Q, inp), neg(N, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(Q nci N, Phi, GammasGamma)], Deltar), append(Gammas, [Gamma], GammasGamma), (!), partition(Stoup, Stoup1, Stoup2), p1(Stoup1: Gamma, l(N, Psi), SubPrf1), ssort(N, SN), do_ones(SN, Ls), append(Gammas, Ls, GammasLs), append(Deltal, [f(Q, [app, Phi, Psi], GammasLs)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(M nci P, OMEGA, l(D, Omega), prf(left(ncircumfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(M, inp), pos(P, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(M nci P, Phi, GammasGamma)], Deltar), append(Gammas, [Gamma], GammasGamma), (!), partition(Stoup, Stoup1, Stoup2), p2r(Stoup1: Gamma, f(P, Psi), SubPrf1), ssort(P, SP), do_ones(SP, Ls), append(Gammas, Ls, GammasLs), append(Deltal, [l(M, [app, Phi, Psi], GammasLs)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(M nci N, OMEGA, l(D, Omega), prf(left(circumfixn), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(M, inp), neg(N, out), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, [f(M nci N, Phi, GammasGamma)], Deltar), append(Gammas, [Gamma], GammasGamma), (!), partition(Stoup, Stoup1, Stoup2), p1(Stoup1: Gamma, l(N, Psi), SubPrf1), ssort(N, SN), do_ones(SN, Ls), append(Gammas, Ls, GammasLs), append(Deltal, [l(M, [app, Phi, Psi], GammasLs)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). % 48 p2l(P nin Q, OMEGA, l(D, Omega), prf(left(ninfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, out), pos(Q, inp), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, [f(P nin Q, Psi, Ls1)|_], [], L), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma2, [[1]|Ls2], Gamma1), p2r(Stoup1: Gamma2, f(P, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(Q, [app, Psi, Phi], Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(P nin M, OMEGA, l(D, Omega), prf(left(ninfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, out), neg(M, inp), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, [f(P nin M, Psi, Ls1)|_], [], L), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), fold(SP, Gamma2, [[1]|Ls2], Gamma1), p2r(Stoup1: Gamma2, f(P, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(M, [app, Psi, Phi], Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(N nin Q, OMEGA, l(D, Omega), prf(left(ninfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(N, out), pos(Q, inp), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, [f(N nin Q, Psi, Ls1)|_], [], L), ssort(N, SN), partition(Stoup, Stoup1, Stoup2), fold(SN, Gamma2, [[1]|Ls2], Gamma1), p1(Stoup1: Gamma2, l(N, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [f(Q, [app, Psi, Phi], Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(N nin M, OMEGA, l(D, Omega), prf(left(ninfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(N, out), neg(M, inp), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, [f(N nin M, Psi, Ls1)|_], [], L), ssort(N, SN), partition(Stoup, Stoup1, Stoup2), fold(SN, Gamma2, [[1]|Ls2], Gamma1), p1(Stoup1: Gamma2, l(N, Phi), SubPrf1), append(Ls1, Ls2, Lss), append(Deltal, [l(M, [app, Psi, Phi], Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(P nin Q, OMEGA, l(D, Omega), prf(left(ninfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, out), pos(Q, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, Ls, [], L), append(_, [f(P nin Q, Psi, Ls1)], Ls), ssort(P, [1|N]), kappend(N, Ls2, [[1]], Ls3), partition(Stoup, Stoup1, Stoup2), fold([1|N], Gamma2, Ls3, Gamma1), p2r(Stoup1: Gamma2, f(P, Phi), SubPrf1), append(Ls2, Ls1, Lss), append(Deltal, [f(Q, [app, Psi, Phi], Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(P nin M, OMEGA, l(D, Omega), prf(left(ninfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- pos(P, out), neg(M, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, Ls, [], L), append(_, [f(P nin M, Psi, Ls1)], Ls), ssort(P, [1|N]), kappend(N, Ls2, [[1]], Ls3), partition(Stoup, Stoup1, Stoup2), fold([1|N], Gamma2, Ls3, Gamma1), p2r(Stoup1: Gamma2, f(P, Phi), SubPrf1), append(Ls2, Ls1, Lss), append(Deltal, [l(M, [app, Psi, Phi], Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). p2l(N nin Q, OMEGA, l(D, Omega), prf(left(ninfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- neg(N, out), pos(Q, inp), (!), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, Ls, [], L), append(_, [f(N nin Q, Psi, Ls1)], Ls), ssort(N, [1|NN]), kappend(NN, Ls2, [[1]], Ls3), partition(Stoup, Stoup1, Stoup2), fold([1|NN], Gamma2, Ls3, Gamma1), p1(Stoup1: Gamma2, l(N, Phi), SubPrf1), append(Ls2, Ls1, Lss), append(Deltal, [f(Q, [app, Psi, Phi], Lss)|Deltar], Delta), p2l(Q, OMEGAPr, l(D, Omega), SubPrf2). p2l(N nin M, OMEGA, l(D, Omega), prf(left(ninfix), OMEGA, l(D), [SubPrf1, SubPrf2])) :- (!), neg(N, out), neg(M, inp), subzoneandapp(OMEGA, OMEGAPr, Stoup2: Delta, Stoup, Deltal, L, Deltar), genins(Gamma1, Ls, [], L), append(_, [f(N nin M, Psi, Ls1)], Ls), ssort(N, [1|NN]), kappend(NN, Ls2, [[1]], Ls3), partition(Stoup, Stoup1, Stoup2), fold([1|NN], Gamma2, Ls3, Gamma1), p1(Stoup1: Gamma2, l(N, Phi), SubPrf1), append(Ls2, Ls1, Lss), append(Deltal, [l(M, [app, Psi, Phi], Lss)|Deltar], Delta), p1(OMEGAPr, l(D, Omega), SubPrf2). % abindoff(+Gamma, +A, +X, -Gamma1) means that Gamma1 is the result % of binding off anaphors A in Gamma with semantics X abindoff([], _, _, []). abindoff([l(B lca A, Chi, Int)|Gamma], A, X, [l(B, [app, Chi, X], Int1)|Gamma1]) :- abindofflist(Int, A, X, Int1), abindoff(Gamma, A, X, Gamma1). abindoff([f(B lca A, Chi, Int)|Gamma], A, X, [l(B, [app, Chi, X], Int1)|Gamma1]) :- abindofflist(Int, A, X, Int1), abindoff(Gamma, A, X, Gamma1). abindoff([l(C, Phi, Int)|Gamma], A, X, [l(C, Phi, Int)|Gamma1]) :- abindoff(Gamma, A, X, Gamma1). abindoff([b(Stoup: Gamma)|Delta], A, X, [b(Stoup: Gamma1)|Delta1]) :- abindoff(Gamma, A, X, Gamma1), abindoff(Delta, A, X, Delta1). abindofflist([], _, _, []). abindofflist([H|T], A, X, [H1|T1]) :- abindoff(H, A, X, H1), abindofflist(T, A, X, T1). % an(+Delta, -Antec, -Anaph, -Theta, -Antec2, -Anaph2) means that configuration Delta % contains the subconfiguration Antec followed later by type Anaph and that % Theta is the result of replacing Antec and Anaph in Delta by variables Antec2 and % Anaph2 respectively. an(Delta, Antec, Anaph, Theta, Antec2, Anaph2) :- an2(Delta, [Antec, Anaph], [], Theta, [Antec2, Anaph2], []). an2([], An, An, [], An2, An2). an2(Gamma, [Gamma1, Anaph], An, [Antec2|Theta], [Antec2, Anaph2], An2) :- append(Gamma1, Gamma2, Gamma), an2(Gamma2, [Anaph], An, Theta, [Anaph2], An2). an2([Anaph|Gamma], [Anaph], [], [Anaph2|Gamma], [Anaph2], []) :- (!). an2([b(Stoup: Gamma)|Gamma2], AnIn, AnOut, [b(Stoup: Theta)|Theta2], AnIn2, AnOut2) :- an2(Gamma, AnIn, AnPr, Theta, AnIn2, AnPr2), an2(Gamma2, AnPr, AnOut, Theta2, AnPr2, AnOut2). an2([l(A, Phi, Int)|Gamma], AnIn, AnOut, [l(A, Phi, Int2)|Gamma2], AnIn2, AnOut2) :- anlst(Int, AnIn, AnPr, Int2, AnIn2, AnPr2), an2(Gamma, AnPr, AnOut, Gamma2, AnPr2, AnOut2). an2([1|Gamma], AnIn, AnOut, [1|Theta], AnIn2, AnOut2) :- an2(Gamma, AnIn, AnOut, Theta, AnIn2, AnOut2). anlst([], An, An, [], An2, An2). anlst([H|T], AnIn, AnOut, [H2|T2], AnIn2, AnOut2) :- an2(H, AnIn, AnPr, H2, AnIn2, AnPr2), anlst(T, AnPr, AnOut, T2, AnPr2, AnOut2). % Irreversible stoup rules 17 p2s(OMEGA, l(D, Omega), prf(perm(uexp), OMEGA, l(D), [SubPrf])) :- subzone(OMEGA, OMEGAPr, StoupPr: DeltaPr, Stoup: Delta), append(Stoup1, [f(A, Phi, [])|Stoup2], Stoup), append(Stoup1, Stoup2, StoupPr), append(Delta1, Delta2, Delta), append(Delta1, [l(A, Phi, [])|Delta2], DeltaPr), p1(OMEGAPr, l(D, Omega), SubPrf). p2s(OMEGA, l(D, Omega), prf(contr(uexp), OMEGA, l(D), [SubPrf])) :- countcheck(OMEGA, ab D), subzone(OMEGA, OMEGAPr, Stoup: Delta, Stoup: Delta1GammaDelta2), append(_, [f(A, Phi, [])|_], Stoup), nappend([Delta1, Gamma, Delta2], Delta1GammaDelta2), append(Delta1, [b([l(A, Phi, [])]: Gamma)|Delta2], Delta), p2s(OMEGAPr, l(D, Omega), SubPrf). neg(_/_, out). % 1 neg(_ bs _, out). % 2 neg(_*_, inp). % 3 neg(i, inp). % 4 neg(_ ci _, out). % 5+ neg(_ cin _, out). % 5- neg(_ in _, out). % 6+ neg(_ inn _, out). % 6- neg(_ dp _, inp). % 7+ neg(_ dpn _, inp). % 7- neg(j, inp). % 8 neg(_ & _, out). % 9 neg(_ + _, inp). % 10 neg(_ u _, out). % 11 neg(_ e _, inp). % 12 neg(nL _, out). % 13 neg(nM _, inp). % 14 neg(ab _, out). % 15 neg(br _, inp). % 16 neg(ue _, inp). % 17 neg(ue _, out). neg(ee _, inp). % 18 neg(_ een _, inp). neg(_ lca _, out). % 19 %neg(w(_), inp). % 20 neg(_ lio _, out). % 21 neg(_ liu _, out). % 22 neg(_ rio _, out). % 23 neg(_ riu _, out). % 24 neg(_ lip _, inp). % 25 neg(_ rip _, inp). % 26 neg(_ uic _, out). % 27+ neg(_ uicn _, out). % 27- neg(_ uii _, out). % 28+ neg(_ uiin _, out). % 28- neg(_ lic _, out). % 29+ neg(_ licn _, out). % 29- neg(_ lii _, out). % 30+ neg(_ liin _, out). % 30- neg(_ uidp _, inp). % 31+ neg(_ uidpn _, inp). % 31- neg(_ lidp _, inp). % 32+ neg(_ lidpn _, inp). % 32- neg(_ iac _, out). % 33 neg(_ iad _, inp). % 34 neg(_ iu _, out). % 35 neg(_ ie _, inp). % 36 neg(iL _, out). % 37 neg(iM _, inp). % 38 neg(lp _, out). % 39 neg(rp _, out). % 40 neg(li _, inp). % 41 neg(ri _, inp). % 42 neg(sp _, out). % 43+ neg(spn _, out). % 43- neg(bg _, inp). % 44+ neg(bgn _, inp). % 44- neg(_ nd _, out). % 45 neg(_ np _, inp). % 46 neg(_ nci _, out). % 47 neg(_ nin _, out). % 48 neg(_ ndp _, inp). % 49 neg(A, out) :- primitive(A, _), atfoc(inp). neg(A, inp) :- primitive(A, _), atfoc(out). pos(_/_, inp). % 1 pos(_ bs _, inp). % 2 pos(_*_, out). % 3 pos(i, out). % 4 pos(_ ci _, inp). % 5+ pos(_ cin _, inp). % 5- pos(_ in _, inp). % 6+ pos(_ inn _, inp). % 6- pos(_ dp _, out). % 7+ pos(_ dpn _, out). % 7- pos(j, out). % 8 pos(_ & _, inp). % 9 pos(_ + _, out). % 10 pos(_ u _, inp). % 11 pos(_ e _, out). % 12 pos(iL _, inp). % 13 pos(iM _, out). % 14 pos(ab _, inp). % 15 pos(br _, out). % 16 %pos(ue _, inp). % 17 pos(ee _, out). % 18 pos(_ een _, out). pos(_ lca _, inp). % 19 %pos(w(_), out). % 32 pos(_ lio _, inp). % 21 pos(_ liu _, inp). % 22 pos(_ rio _, inp). % 23 pos(_ riu _, inp). % 24 pos(_ lip _, out). % 25 pos(_ rip _, out). % 26 pos(_ uic _, inp). % 27+ pos(_ uicn _, inp). % 27- pos(_ uii _, inp). % 28+ pos(_ uiin _, inp). % 28- pos(_ lic _, inp). % 29+ pos(_ licn _, inp). % 29- pos(_ lii _, inp). % 30+ pos(_ liin _, inp). % 30- pos(_ uidp _, out). % 31+ pos(_ uidpn _, out). % 31- pos(_ lidp _, out). % 32+ pos(_ lidpn _, out). % 32- pos(_ iac _, inp). % 33 pos(_ iad _, out). % 34 pos(_ iu _, inp). % 35 pos(_ ie _, out). % 36 pos(iL _, inp). % 37 pos(iM _, out). % 38 pos(lp _, inp). % 39 pos(rp _, inp). % 40 pos(li _, out). % 41 pos(ri _, out). % 42 pos(sp _, inp). % 43+ pos(spn _, inp). % 43- pos(bg _, out). % 44+ pos(bgn _, out). % 44- pos(_ nd _, inp). % 45 pos(_ np _, out). % 46 pos(_ nci _, inp). % 47 pos(_ nin _, inp). % 48 pos(_ ndp _, out). % 49 pos(_-_, out). % 50 pos(A, inp) :- primitive(A, _), atfoc(inp). pos(A, out) :- primitive(A, _), atfoc(out). p2r([]: [l(A, Phi, [])], f(A, Phi), prf(id, []: [l(A, Phi, [])], f(A), [])) :- atfoc(out), primitive(A, []). p2r([]: [l(A, Phi, [[1]])], f(A, Phi), prf(id, []: [l(A, Phi, [[1]])], f(A), [])) :- atfoc(out), primitive(A, [1]). % 3 p2r(Stoup: Delta, f(P1*P2, [pair, Phi, Psi]), prf(right(product), Stoup: Delta, f(P1*P2), [SubPrf1, SubPrf2])) :- pos(P1, out), pos(P2, out), ssort(P1, SP1), (!), partition(Stoup, Stoup1, Stoup2), append(Gamma1, Gamma2, Delta), configsort(Gamma1, SP1), p2r(Stoup1: Gamma1, f(P1, Phi), SubPrf1), p2r(Stoup2: Gamma2, f(P2, Psi), SubPrf2). p2r(Stoup: Delta, f(P*N, [pair, Phi, Psi]), prf(right(product), Stoup: Delta, f(P*N), [SubPrf1, SubPrf2])) :- pos(P, out), neg(N, out), ssort(P, SP), (!), partition(Stoup, Stoup1, Stoup2), append(Gamma1, Gamma2, Delta), configsort(Gamma1, SP), p2r(Stoup1: Gamma1, f(P, Phi), SubPrf1), p1(Stoup2: Gamma2, l(N, Psi), SubPrf2). p2r(Stoup: Delta, f(N*P, [pair, Phi, Psi]), prf(right(product), Stoup: Delta, f(N*P), [SubPrf1, SubPrf2])) :- neg(N, out), pos(P, out), ssort(N, SN), (!), partition(Stoup, Stoup1, Stoup2), append(Gamma1, Gamma2, Delta), configsort(Gamma1, SN), p1(Stoup1: Gamma1, l(N, Phi), SubPrf1), p2r(Stoup2: Gamma2, f(P, Psi), SubPrf2). p2r(Stoup: Delta, f(N1*N2, [pair, Phi, Psi]), prf(right(product), Stoup: Delta, f(N1*N2), [SubPrf1, SubPrf2])) :- neg(N1, out), neg(N2, out), ssort(N1, SN1), (!), partition(Stoup, Stoup1, Stoup2), append(Gamma1, Gamma2, Delta), configsort(Gamma1, SN1), p1(Stoup1: Gamma1, l(N1, Phi), SubPrf1), p1(Stoup2: Gamma2, l(N2, Psi), SubPrf2). % 4 p2r([]: [], f(i, 0), prf(right(productunit), []: [], f(i), [])). % 7+ p2r(Stoup: Delta, f(P1 dp P2, [pair, Phi, Psi]), prf(right(dprod), Stoup: Delta, f(P1 dp P2), [SubPrf1, SubPrf2])) :- pos(P1, out), pos(P2, out), configsort(Delta, S), do_ones(S, Ls), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, [Gamma2|Ls], Delta), p2r(Stoup1: Gamma1, f(P1, Phi), SubPrf1), p2r(Stoup2: Gamma2, f(P2, Psi), SubPrf2). p2r(Stoup: Delta, f(P dp N, [pair, Phi, Psi]), prf(right(dprod), Stoup: Delta, f(P dp N), [SubPrf1, SubPrf2])) :- pos(P, out), neg(N, out), configsort(Delta, S), do_ones(S, Ls), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, [Gamma2|Ls], Delta), p2r(Stoup1: Gamma1, f(P, Phi), SubPrf1), p1(Stoup2: Gamma2, l(N, Psi), SubPrf2). p2r(Stoup: Delta, f(N dp P, [pair, Phi, Psi]), prf(right(dprod), Stoup: Delta, f(N dp P), [SubPrf1, SubPrf2])) :- neg(N, out), pos(P, out), configsort(Delta, S), do_ones(S, Ls), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, [Gamma2|Ls], Delta), p1(Stoup1: Gamma1, l(N, Phi), SubPrf1), p2r(Stoup2: Gamma2, f(P, Psi), SubPrf2). p2r(Stoup: Delta, f(N1 dp N2, [pair, Phi, Psi]), prf(right(dprod), Stoup: Delta, f(N1 dp N2), [SubPrf1, SubPrf2])) :- neg(N1, out), neg(N2, out), configsort(Delta, S), do_ones(S, Ls), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, [Gamma2|Ls], Delta), p1(Stoup1: Gamma1, l(N1, Phi), SubPrf1), p1(Stoup2: Gamma2, l(N2, Psi), SubPrf2). % 7- p2r(Stoup: Delta, f(P1 dpn P2, [pair, Phi, Psi]), prf(right(dprodn), Stoup: Delta, f(P1 dpn P2), [SubPrf1, SubPrf2])) :- pos(P1, out), pos(P2, out), configsort(Delta, S), do_ones(S, Ls), append(Ls, [[Gamma2]], LsGamma2), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, LsGamma2, Delta), p2r(Stoup1: Gamma1, f(P1, Phi), SubPrf1), p2r(Stoup2: Gamma2, f(P2, Psi), SubPrf2). p2r(Stoup: Delta, f(P dpn N, [pair, Phi, Psi]), prf(right(dprodn), Stoup: Delta, f(P dpn N), [SubPrf1, SubPrf2])) :- pos(P, out), neg(N, out), configsort(Delta, S), do_ones(S, Ls), append(Ls, [[Gamma2]], LsGamma2), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, LsGamma2, Delta), p2r(Stoup1: Gamma1, f(P, Phi), SubPrf1), p1(Stoup2: Gamma2, l(N, Psi), SubPrf2). p2r(Stoup: Delta, f(N dpn P, [pair, Phi, Psi]), prf(right(dprodn), Stoup: Delta, f(N dpn P), [SubPrf1, SubPrf2])) :- neg(N, out), pos(P, out), configsort(Delta, S), do_ones(S, Ls), append(Ls, [[Gamma2]], LsGamma2), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, LsGamma2, Delta), p1(Stoup1: Gamma1, l(N, Phi), SubPrf1), p2r(Stoup2: Gamma2, f(P, Psi), SubPrf2). p2r(Stoup: Delta, f(N1 dpn N2, [pair, Phi, Psi]), prf(right(dprodn), Stoup: Delta, f(N1 dpn N2), [SubPrf1, SubPrf2])) :- neg(N1, out), neg(N2, out), configsort(Delta, S), do_ones(S, Ls), append(Ls, [[Gamma2]], LsGamma2), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, LsGamma2, Delta), p1(Stoup1: Gamma1, l(N1, Phi), SubPrf1), p1(Stoup2: Gamma2, l(N2, Psi), SubPrf2). % 8 p2r([]: [1], f(j, 0), prf(right(dproductunit), []: [1], f(j), [])). % 10 p2r(OMEGA, f(P+B, [1, Phi]), prf(right(adisj), OMEGA, f(P+B), [SubPrf])) :- pos(P, out), p2r(OMEGA, f(P, Phi), SubPrf). p2r(OMEGA, f(N+B, [1, Phi]), prf(right(adisj), OMEGA, f(N+B), [SubPrf])) :- neg(N, out), p1(OMEGA, l(N, Phi), SubPrf). p2r(OMEGA, f(A+P, [2, Psi]), prf(right(adisj), OMEGA, f(A+P), [SubPrf])) :- pos(P, out), p2r(OMEGA, f(P, Psi), SubPrf). p2r(OMEGA, f(A+N, [2, Psi]), prf(right(adisj), OMEGA, f(A+N), [SubPrf])) :- (!), neg(N, out), p1(OMEGA, l(N, Psi), SubPrf). % 12 p2r(OMEGA, f(V e P, [pair, T, Phi]), prf(right(exstq), OMEGA, f(V e P), [SubPrf])) :- pos(P, out), tsubst(T, V, P, PP), (!), p2r(OMEGA, f(PP, Phi), SubPrf). p2r(OMEGA, f(V e N, [pair, T, Phi]), prf(right(exstq), OMEGA, f(V e N), [SubPrf])) :- neg(N, out), tsubst(T, V, N, NN), (!), p1(OMEGA, l(NN, Phi), SubPrf). % 14 p2r(OMEGA, f(nM P, [cup, Phi]), prf(right(emod), OMEGA, f(nM P), [SubPrf])) :- pos(P, out), (!), p2r(OMEGA, f(P, Phi), SubPrf). p2r(OMEGA, f(nM N, [cap, Phi]), prf(right(emod), OMEGA, f(nM N), [SubPrf])) :- (!), neg(N, out), p1(OMEGA, l(N, Phi), SubPrf). % 16 p2r([]:[b([]: Gamma)], f(br P, Phi), prf(right(brack), []:[b([]: Gamma)], f(br P), [SubPrf])) :- pos(P, out), (!), p2r([]: Gamma, f(P, Phi), SubPrf). p2r([]:[b([]: Gamma)], f(br N, Phi), prf(right(brack), []:[b([]: Gamma)], f(br N), [SubPrf])) :- (!), neg(N, out), p1([]: Gamma, l(N, Phi), SubPrf). % 18 p2r(OMEGA, f(ee P, [Phi]), prf(right(eexp), OMEGA, f(ee P), [SubPrf])) :- pos(P, out), p2r(OMEGA, f(P, Phi), SubPrf). p2r(OMEGA, f(ee N, [Phi]), prf(right(eexp), OMEGA, f(ee N), [SubPrf])) :- neg(N, out), p1(OMEGA, l(N, Phi), SubPrf). p2r(Stoup: Delta, f(ee P, [Phi|Psi]), prf(expan(eexp), Stoup: Delta, f(ee P), [SubPrf1, SubPrf2])) :- pos(P, out), (!), partition(Stoup, Stoup1, Stoup2), append(Delta1, Delta2, Delta), p2r(Stoup1: Delta1, f(P, Phi), SubPrf1), p2r(Stoup2: Delta2, f(ee P, Psi), SubPrf2). p2r(Stoup: Delta, f(ee N, [Phi|Psi]), prf(expan(eexp), Stoup: Delta, f(ee N), [SubPrf1, SubPrf2])) :- (!), neg(N, out), partition(Stoup, Stoup1, Stoup2), append(Delta1, Delta2, Delta), p1(Stoup1: Delta1, l(N, Phi), SubPrf1), p1(Stoup2: Delta2, l(ee N, Psi), SubPrf2). % 18n p2r(OMEGA, f(1 een P, [Phi]), prf(right(eexp), OMEGA, f(1 een P), [SubPrf])) :- pos(P, out), p2r(OMEGA, f(P, Phi), SubPrf). p2r(OMEGA, f(1 een N, [Phi]), prf(right(eexp), OMEGA, f(1 een N), [SubPrf])) :- neg(N, out), p1(OMEGA, l(N, Phi), SubPrf). % 20 p2r([]: [], f(w([]), 0), prf(right(words), []: [], f(w([])), [])). p2r(Stoup: Delta, f(M1 een P, [Phi|Psi]), prf(expan(eexp), Stoup: Delta, f(M1 een P), [SubPrf1, SubPrf2])) :- pos(P, out), (!), partition(Stoup, Stoup1, Stoup2), append(Delta1, Delta2, Delta), p2r(Stoup1: Delta1, f(P, Phi), SubPrf1), p2r(Stoup2: Delta2, f(M een P, Psi), SubPrf2), M1 is M+1. p2r(Stoup: Delta, f(M1 een N, [Phi|Psi]), prf(expan(eexp), Stoup: Delta, f(M1 een N), [SubPrf1, SubPrf2])) :- (!), neg(N, out), partition(Stoup, Stoup1, Stoup2), append(Delta1, Delta2, Delta), p1(Stoup1: Delta1, l(N, Phi), SubPrf1), p1(Stoup2: Delta2, l(M een N, Psi), SubPrf2), M1 is M+1. % 25 p2r(Stoup: Delta, f(P1 lip P2, Psi), prf(right(liproduct), Stoup: Delta, f(P1 lip P2), [SubPrf1, SubPrf2])) :- pos(P1, out), pos(P2, out), ssort(P1, SP1), (!), partition(Stoup, Stoup1, Stoup2), append(Gamma1, Gamma2, Delta), configsort(Gamma1, SP1), p2r(Stoup1: Gamma1, f(P1, _), SubPrf1), p2r(Stoup2: Gamma2, f(P2, Psi), SubPrf2). p2r(Stoup: Delta, f(P lip N, Psi), prf(right(liproduct), Stoup: Delta, f(P lip N), [SubPrf1, SubPrf2])) :- pos(P, out), neg(N, out), ssort(P, SP), (!), partition(Stoup, Stoup1, Stoup2), append(Gamma1, Gamma2, Delta), configsort(Gamma1, SP), p2r(Stoup1: Gamma1, f(P, _), SubPrf1), p1(Stoup2: Gamma2, l(N, Psi), SubPrf2). p2r(Stoup: Delta, f(N lip P, Psi), prf(right(liproduct), Stoup: Delta, f(N lip P), [SubPrf1, SubPrf2])) :- neg(N, out), pos(P, out), ssort(N, SN), (!), partition(Stoup, Stoup1, Stoup2), append(Gamma1, Gamma2, Delta), configsort(Gamma1, SN), p1(Stoup1: Gamma1, l(N, _), SubPrf1), p2r(Stoup2: Gamma2, f(P, Psi), SubPrf2). p2r(Stoup: Delta, f(N1 lip N2, Psi), prf(right(liproduct), Stoup: Delta, f(N1 lip N2), [SubPrf1, SubPrf2])) :- neg(N1, out), neg(N2, out), ssort(N1, SN1), (!), partition(Stoup, Stoup1, Stoup2), append(Gamma1, Gamma2, Delta), configsort(Gamma1, SN1), p1(Stoup1: Gamma1, l(N1, _), SubPrf1), p1(Stoup2: Gamma2, l(N2, Psi), SubPrf2). % 26 p2r(Stoup: Delta, f(P1 rip P2, Phi), prf(right(riproduct), Stoup: Delta, f(P1 rip P2), [SubPrf1, SubPrf2])) :- pos(P1, out), pos(P2, out), ssort(P1, SP1), (!), partition(Stoup, Stoup1, Stoup2), append(Gamma1, Gamma2, Delta), configsort(Gamma1, SP1), p2r(Stoup1: Gamma1, f(P1, Phi), SubPrf1), p2r(Stoup2: Gamma2, f(P2, _), SubPrf2). p2r(Stoup: Delta, f(P rip N, Phi), prf(right(riproduct), Stoup: Delta, f(P rip N), [SubPrf1, SubPrf2])) :- pos(P, out), neg(N, out), ssort(P, SP), (!), partition(Stoup, Stoup1, Stoup2), append(Gamma1, Gamma2, Delta), configsort(Gamma1, SP), p2r(Stoup1: Gamma1, f(P, Phi), SubPrf1), p1(Stoup2: Gamma2, l(N, _), SubPrf2). p2r(Stoup: Delta, f(N rip P, Phi), prf(right(riproduct), Stoup: Delta, f(N rip P), [SubPrf1, SubPrf2])) :- neg(N, out), pos(P, out), ssort(N, SN), (!), partition(Stoup, Stoup1, Stoup2), append(Gamma1, Gamma2, Delta), configsort(Gamma1, SN), p1(Stoup1: Gamma1, l(N, Phi), SubPrf1), p2r(Stoup2: Gamma2, f(P, _), SubPrf2). p2r(Stoup: Delta, f(N1 rip N2, Phi), prf(right(riproduct), Stoup: Delta, f(N1 rip N2), [SubPrf1, SubPrf2])) :- neg(N1, out), neg(N2, out), ssort(N1, SN1), (!), partition(Stoup, Stoup1, Stoup2), append(Gamma1, Gamma2, Delta), configsort(Gamma1, SN1), p1(Stoup1: Gamma1, l(N1, Phi), SubPrf1), p1(Stoup2: Gamma2, l(N2, _), SubPrf2). % 31+ p2r(Stoup: Delta, f(P1 uidp P2, Psi), prf(right(uidprod), Stoup: Delta, f(P1 uidp P2), [SubPrf1, SubPrf2])) :- pos(P1, out), pos(P2, out), configsort(Delta, S), do_ones(S, Ls), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, [Gamma2|Ls], Delta), p2r(Stoup1: Gamma1, f(P1, _), SubPrf1), p2r(Stoup2: Gamma2, f(P2, Psi), SubPrf2). p2r(Stoup: Delta, f(P uidp N, Psi), prf(right(uidprod), Stoup: Delta, f(P uidp N), [SubPrf1, SubPrf2])) :- pos(P, out), neg(N, out), configsort(Delta, S), do_ones(S, Ls), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, [Gamma2|Ls], Delta), p2r(Stoup1: Gamma1, f(P, _), SubPrf1), p1(Stoup2: Gamma2, l(N, Psi), SubPrf2). p2r(Stoup: Delta, f(N uidp P, Psi), prf(right(uidprod), Stoup: Delta, f(N uidp P), [SubPrf1, SubPrf2])) :- neg(N, out), pos(P, out), configsort(Delta, S), do_ones(S, Ls), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, [Gamma2|Ls], Delta), p1(Stoup1: Gamma1, l(N, _), SubPrf1), p2r(Stoup2: Gamma2, f(P, Psi), SubPrf2). p2r(Stoup: Delta, f(N1 uidp N2, Psi), prf(right(uidprod), Stoup: Delta, f(N1 uidp N2), [SubPrf1, SubPrf2])) :- neg(N1, out), neg(N2, out), configsort(Delta, S), do_ones(S, Ls), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, [Gamma2|Ls], Delta), p1(Stoup1: Gamma1, l(N1, _), SubPrf1), p1(Stoup2: Gamma2, l(N2, Psi), SubPrf2). % 31- p2r(Stoup: Delta, f(P1 uidpn P2, Psi), prf(right(uidprodn), Stoup: Delta, f(P1 uidpn P2), [SubPrf1, SubPrf2])) :- pos(P1, out), pos(P2, out), configsort(Delta, S), do_ones(S, Ls), append(Ls, [[Gamma2]], LsGamma2), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, LsGamma2, Delta), p2r(Stoup1: Gamma1, f(P1, _), SubPrf1), p2r(Stoup2: Gamma2, f(P2, Psi), SubPrf2). p2r(Stoup: Delta, f(P uidpn N, Psi), prf(right(uidprodn), Stoup: Delta, f(P uidpn N), [SubPrf1, SubPrf2])) :- pos(P, out), neg(N, out), configsort(Delta, S), do_ones(S, Ls), append(Ls, [[Gamma2]], LsGamma2), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, LsGamma2, Delta), p2r(Stoup1: Gamma1, f(P, _), SubPrf1), p1(Stoup2: Gamma2, l(N, Psi), SubPrf2). p2r(Stoup: Delta, f(N uidpn P, Psi), prf(right(uidprodn), Stoup: Delta, f(N uidpn P), [SubPrf1, SubPrf2])) :- neg(N, out), pos(P, out), configsort(Delta, S), do_ones(S, Ls), append(Ls, [[Gamma2]], LsGamma2), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, LsGamma2, Delta), p1(Stoup1: Gamma1, l(N, _), SubPrf1), p2r(Stoup2: Gamma2, f(P, Psi), SubPrf2). p2r(Stoup: Delta, f(N1 uidpn N2, Psi), prf(right(uidprodn), Stoup: Delta, f(N1 uidpn N2), [SubPrf1, SubPrf2])) :- neg(N1, out), neg(N2, out), configsort(Delta, S), do_ones(S, Ls), append(Ls, [[Gamma2]], LsGamma2), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, LsGamma2, Delta), p1(Stoup1: Gamma1, l(N1, _), SubPrf1), p1(Stoup2: Gamma2, l(N2, Psi), SubPrf2). % 32+ p2r(Stoup: Delta, f(P1 lidp P2, Phi), prf(right(lidprod), Stoup: Delta, f(P1 lidp P2), [SubPrf1, SubPrf2])) :- pos(P1, out), pos(P2, out), configsort(Delta, S), do_ones(S, Ls), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, [Gamma2|Ls], Delta), p2r(Stoup1: Gamma1, f(P1, Phi), SubPrf1), p2r(Stoup2: Gamma2, f(P2, _), SubPrf2). p2r(Stoup: Delta, f(P lidp N, Phi), prf(right(lidprod), Stoup: Delta, f(P lidp N), [SubPrf1, SubPrf2])) :- pos(P, out), neg(N, out), configsort(Delta, S), do_ones(S, Ls), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, [Gamma2|Ls], Delta), p2r(Stoup1: Gamma1, f(P, Phi), SubPrf1), p1(Stoup2: Gamma2, l(N, _), SubPrf2). p2r(Stoup: Delta, f(N lidp P, Phi), prf(right(lidprod), Stoup: Delta, f(N lidp P), [SubPrf1, SubPrf2])) :- neg(N, out), pos(P, out), configsort(Delta, S), do_ones(S, Ls), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, [Gamma2|Ls], Delta), p1(Stoup1: Gamma1, l(N, Phi), SubPrf1), p2r(Stoup2: Gamma2, f(P, _), SubPrf2). p2r(Stoup: Delta, f(N1 lidp N2, Phi), prf(right(lidprod), Stoup: Delta, f(N1 lidp N2), [SubPrf1, SubPrf2])) :- neg(N1, out), neg(N2, out), configsort(Delta, S), do_ones(S, Ls), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, [Gamma2|Ls], Delta), p1(Stoup1: Gamma1, l(N1, Phi), SubPrf1), p1(Stoup2: Gamma2, l(N2, _), SubPrf2). % 32- p2r(Stoup: Delta, f(P1 lidpn P2, Phi), prf(right(lidprodn), Stoup: Delta, f(P1 lidpn P2), [SubPrf1, SubPrf2])) :- pos(P1, out), pos(P2, out), configsort(Delta, S), do_ones(S, Ls), append(Ls, [[Gamma2]], LsGamma2), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, LsGamma2, Delta), p2r(Stoup1: Gamma1, f(P1, Phi), SubPrf1), p2r(Stoup2: Gamma2, f(P2, _), SubPrf2). p2r(Stoup: Delta, f(P lidpn N, Phi), prf(right(lidprodn), Stoup: Delta, f(P lidpn N), [SubPrf1, SubPrf2])) :- pos(P, out), neg(N, out), configsort(Delta, S), do_ones(S, Ls), append(Ls, [[Gamma2]], LsGamma2), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, LsGamma2, Delta), p2r(Stoup1: Gamma1, f(P, Phi), SubPrf1), p1(Stoup2: Gamma2, l(N, _), SubPrf2). p2r(Stoup: Delta, f(N lidpn P, Phi), prf(right(lidprodn), Stoup: Delta, f(N lidpn P), [SubPrf1, SubPrf2])) :- neg(N, out), pos(P, out), configsort(Delta, S), do_ones(S, Ls), append(Ls, [[Gamma2]], LsGamma2), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, LsGamma2, Delta), p1(Stoup1: Gamma1, l(N, Phi), SubPrf1), p2r(Stoup2: Gamma2, f(P, _), SubPrf2). p2r(Stoup: Delta, f(N1 lidpn N2, Phi), prf(right(lidprodn), Stoup: Delta, f(N1 lidpn N2), [SubPrf1, SubPrf2])) :- neg(N1, out), neg(N2, out), configsort(Delta, S), do_ones(S, Ls), append(Ls, [[Gamma2]], LsGamma2), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, LsGamma2, Delta), p1(Stoup1: Gamma1, l(N1, Phi), SubPrf1), p1(Stoup2: Gamma2, l(N2, _), SubPrf2). % 34 p2r(OMEGA, f(P iad B, Phi), prf(right(iadisj), OMEGA, f(P iad B), [SubPrf])) :- pos(P, out), p2r(OMEGA, f(P, Phi), SubPrf). p2r(OMEGA, f(N iad B, Phi), prf(right(iadisj), OMEGA, f(N iad B), [SubPrf])) :- neg(N, out), p1(OMEGA, l(N, Phi), SubPrf). p2r(OMEGA, f(A iad P, Psi), prf(right(iadisj), OMEGA, f(A iad P), [SubPrf])) :- pos(P, out), p2r(OMEGA, f(P, Psi), SubPrf). p2r(OMEGA, f(A iad N, Psi), prf(right(iadisj), OMEGA, f(A iad N), [SubPrf])) :- neg(N, out), (!), p1(OMEGA, l(N, Psi), SubPrf). % 36 p2r(OMEGA, f(V ie P, Phi), prf(right(iexstq), OMEGA, f(V ie P), [SubPrf])) :- pos(P, out), tsubst(_, V, P, PP), (!), p2r(OMEGA, f(PP, Phi), SubPrf). p2r(OMEGA, f(V ie N, Phi), prf(right(iexstq), OMEGA, f(V ie N), [SubPrf])) :- neg(N, out), tsubst(_, V, N, NN), (!), p1(OMEGA, l(NN, Phi), SubPrf). % 38 p2r(OMEGA, f(iM P, Phi), prf(right(iemod), OMEGA, f(iM P), [SubPrf])) :- pos(P, out), (!), p2r(OMEGA, f(P, Phi), SubPrf). p2r(OMEGA, f(iM N, Phi), prf(right(iemod), OMEGA, f(iM N), [SubPrf])) :- (!), neg(N, out), p1(OMEGA, l(N, Phi), SubPrf). % 39 p2r(Stoup: Gamma1, f(li P, Phi), prf(right(linj), Stoup: Gamma1, f(li P), [SubPrf])) :- pos(P, out), append(Gamma, [1], Gamma1), (!), p2r(Stoup: Gamma, f(P, Phi), SubPrf). p2r(Stoup: Gamma1, f(li N, Phi), prf(right(linj), Stoup: Gamma1, f(li N), [SubPrf])) :- append(Gamma, [1], Gamma1), (!), p2r(Stoup: Gamma, f(N, Phi), SubPrf). % 40 p2r(Stoup: [1|Gamma], f(ri P, Phi), prf(right(rinj), Stoup: [1|Gamma], f(ri P), [SubPrf])) :- pos(P, out), (!), p2r(Stoup: Gamma, f(P, Phi), SubPrf). p2r(Stoup: [1|Gamma], f(ri N, Phi), prf(right(rinj), Stoup: [1|Gamma], f(ri N), [SubPrf])) :- (!), neg(N, out), p2r(Stoup: Gamma, f(N, Phi), SubPrf). % 43+ p2r(Stoup: Delta, f(bg P, Phi), prf(right(bridge), Stoup: Delta, f(bg P), [SubPrf])) :- pos(P, out), configsort(Delta, S), do_ones(S, Ls), (!), fold([1|S], Gamma1, [[]|Ls], Delta), p2r(Stoup: Gamma1, f(P, Phi), SubPrf). p2r(Stoup: Delta, f(bg N, Phi), prf(right(bridge), Stoup: Delta, f(bg N), [SubPrf])) :- neg(N, out), configsort(Delta, S), do_ones(S, Ls), (!), fold([1|S], Gamma1, [[]|Ls], Delta), p1(Stoup: Gamma1, l(N, Phi), SubPrf). % 43- p2r(Stoup: Delta, f(bgn P, Phi), prf(right(bridgen), Stoup: Delta, f(bgn P), [SubPrf])) :- pos(P, out), configsort(Delta, S), do_ones(S, Ls), append(Ls, [[]], Lss), (!), fold([1|S], Gamma1, Lss, Delta), p2r(Stoup: Gamma1, f(P, Phi), SubPrf). p2r(Stoup: Delta, f(bgn N, Phi), prf(right(bridgen), Stoup: Delta, f(bgn N), [SubPrf])) :- neg(N, out), configsort(Delta, S), do_ones(S, Ls), append(Ls, [[]], Lss), (!), fold([1|S], Gamma1, Lss, Delta), p1(Stoup: Gamma1, l(N, Phi), SubPrf). % 46 p2r(Stoup: Delta, f(P1 np P2, [pair, Phi, Psi]), prf(right(nprod), Stoup: Delta, f(P1 np P2), [SubPrf1, SubPrf2])) :- pos(P1, out), pos(P2, out), ssort(P1, SP1), partition(Stoup, Stoup1, Stoup2), append(Gamma1, Gamma2, Delta), configsort(Gamma1, SP1), p2r(Stoup1: Gamma1, f(P1, Phi), SubPrf1), p2r(Stoup2: Gamma2, f(P2, Psi), SubPrf2). p2r(Stoup: Delta, f(P np N, [pair, Phi, Psi]), prf(right(nprod), Stoup: Delta, f(P np N), [SubPrf1, SubPrf2])) :- pos(P, out), neg(N, out), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), append(Gamma1, Gamma2, Delta), configsort(Gamma1, SP), p2r(Stoup1: Gamma1, f(P, Phi), SubPrf1), p1(Stoup2: Gamma2, l(N, Psi), SubPrf2). p2r(Stoup: Delta, f(N np P, [pair, Phi, Psi]), prf(right(nprod), Stoup: Delta, f(N np P), [SubPrf1, SubPrf2])) :- neg(N, out), pos(P, out), ssort(N, SN), partition(Stoup, Stoup1, Stoup2), append(Gamma1, Gamma2, Delta), configsort(Gamma1, SN), p1(Stoup1: Gamma1, l(N, Phi), SubPrf1), p2r(Stoup2: Gamma2, f(P, Psi), SubPrf2). p2r(Stoup: Delta, f(N1 np N2, [pair, Phi, Psi]), prf(right(nprod), Stoup: Delta, f(N1 np N2), [SubPrf1, SubPrf2])) :- neg(N1, out), neg(N2, out), ssort(N1, SN1), partition(Stoup, Stoup1, Stoup2), append(Gamma1, Gamma2, Delta), configsort(Gamma1, SN1), p1(Stoup1: Gamma1, l(N1, Phi), SubPrf1), p1(Stoup2: Gamma2, l(N2, Psi), SubPrf2). p2r(Stoup: Delta, f(P1 np P2, [pair, Phi, Psi]), prf(right(nprod), Stoup: Delta, f(P1 np P2), [SubPrf1, SubPrf2])) :- pos(P1, out), pos(P2, out), ssort(P1, SP1), partition(Stoup, Stoup1, Stoup2), append(Gamma1, Gamma2, Delta), configsort(Gamma1, SP1), (!), p2r(Stoup1: Gamma1, f(P2, Psi), SubPrf1), p2r(Stoup2: Gamma2, f(P1, Phi), SubPrf2). p2r(Stoup: Delta, f(P np N, [pair, Phi, Psi]), prf(right(nprod), Stoup: Delta, f(P np N), [SubPrf1, SubPrf2])) :- pos(P, out), neg(N, out), ssort(P, SP), partition(Stoup, Stoup1, Stoup2), append(Gamma1, Gamma2, Delta), configsort(Gamma1, SP), p1(Stoup1: Gamma1, l(N, Psi), SubPrf1), p2r(Stoup2: Gamma2, f(P, Phi), SubPrf2). p2r(Stoup: Delta, f(N np P, [pair, Phi, Psi]), prf(right(nprod), Stoup: Delta, f(N np P), [SubPrf1, SubPrf2])) :- neg(N, out), pos(P, out), ssort(N, SN), partition(Stoup, Stoup1, Stoup2), append(Gamma1, Gamma2, Delta), configsort(Gamma1, SN), p2r(Stoup1: Gamma1, f(P, Psi), SubPrf1), p1(Stoup2: Gamma2, l(N, Phi), SubPrf2). p2r(Stoup: Delta, f(N1 np N2, [pair, Phi, Psi]), prf(right(nprod), Stoup: Delta, f(N1 np N2), [SubPrf1, SubPrf2])) :- neg(N1, out), neg(N2, out), ssort(N1, SN1), (!), partition(Stoup, Stoup1, Stoup2), append(Gamma1, Gamma2, Delta), configsort(Gamma1, SN1), p1(Stoup1: Gamma1, l(N2, Psi), SubPrf1), p1(Stoup2: Gamma2, l(N1, Phi), SubPrf2). % 49 p2r(Stoup: Delta, f(P1 ndp P2, [pair, Phi, Psi]), prf(right(ndprod), Stoup: Delta, f(P1 ndp P2), [SubPrf1, SubPrf2])) :- pos(P1, out), pos(P2, out), configsort(Delta, S), do_ones(S, Ls), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, [Gamma2|Ls], Delta), p2r(Stoup1: Gamma1, f(P1, Phi), SubPrf1), p2r(Stoup2: Gamma2, f(P2, Psi), SubPrf2). p2r(Stoup: Delta, f(P ndp N, [pair, Phi, Psi]), prf(right(ndprod), Stoup: Delta, f(P ndp N), [SubPrf1, SubPrf2])) :- pos(P, out), neg(N, out), configsort(Delta, S), do_ones(S, Ls), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, [Gamma2|Ls], Delta), p2r(Stoup1: Gamma1, f(P, Phi), SubPrf1), p1(Stoup2: Gamma2, l(N, Psi), SubPrf2). p2r(Stoup: Delta, f(N ndp P, [pair, Phi, Psi]), prf(right(ndprod), Stoup: Delta, f(N ndp P), [SubPrf1, SubPrf2])) :- neg(N, out), pos(P, out), configsort(Delta, S), do_ones(S, Ls), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, [Gamma2|Ls], Delta), p1(Stoup1: Gamma1, l(N, Phi), SubPrf1), p2r(Stoup2: Gamma2, f(P, Psi), SubPrf2). p2r(Stoup: Delta, f(N1 ndp N2, [pair, Phi, Psi]), prf(right(ndprod), Stoup: Delta, f(N1 ndp N2), [SubPrf1, SubPrf2])) :- neg(N1, out), neg(N2, out), configsort(Delta, S), do_ones(S, Ls), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, [Gamma2|Ls], Delta), p1(Stoup1: Gamma1, l(N1, Phi), SubPrf1), p1(Stoup2: Gamma2, l(N2, Psi), SubPrf2). p2r(Stoup: Delta, f(P1 ndp P2, [pair, Phi, Psi]), prf(right(ndprod), Stoup: Delta, f(P1 ndp P2), [SubPrf1, SubPrf2])) :- pos(P1, out), pos(P2, out), configsort(Delta, S), do_ones(S, Ls), append(Ls, [[Gamma2]], LsGamma2), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, LsGamma2, Delta), p2r(Stoup1: Gamma1, f(P1, Phi), SubPrf1), p2r(Stoup2: Gamma2, f(P2, Psi), SubPrf2). p2r(Stoup: Delta, f(P ndp N, [pair, Phi, Psi]), prf(right(ndprodn), Stoup: Delta, f(P ndp N), [SubPrf1, SubPrf2])) :- pos(P, out), neg(N, out), configsort(Delta, S), do_ones(S, Ls), append(Ls, [[Gamma2]], LsGamma2), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, LsGamma2, Delta), p2r(Stoup1: Gamma1, f(P, Phi), SubPrf1), p1(Stoup2: Gamma2, l(N, Psi), SubPrf2). p2r(Stoup: Delta, f(N ndp P, [pair, Phi, Psi]), prf(right(ndprod), Stoup: Delta, f(N ndp P), [SubPrf1, SubPrf2])) :- neg(N, out), pos(P, out), configsort(Delta, S), do_ones(S, Ls), append(Ls, [[Gamma2]], LsGamma2), (!), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, LsGamma2, Delta), p1(Stoup1: Gamma1, l(N, Phi), SubPrf1), p2r(Stoup2: Gamma2, f(P, Psi), SubPrf2). p2r(Stoup: Delta, f(N1 ndp N2, [pair, Phi, Psi]), prf(right(ndprod), Stoup: Delta, f(N1 ndp N2), [SubPrf1, SubPrf2])) :- neg(N1, out), neg(N2, out), configsort(Delta, S), do_ones(S, Ls), append(Ls, [[Gamma2]], LsGamma2), partition(Stoup, Stoup1, Stoup2), fold([1|S], Gamma1, LsGamma2, Delta), p1(Stoup1: Gamma1, l(N1, Phi), SubPrf1), p1(Stoup2: Gamma2, l(N2, Psi), SubPrf2). % 50 p2r(OMEGA, f(P1-P2, Psi), prf(right(diff), OMEGA, f(P1-P2), [SubPrf])) :- pos(P1, out), pos(P2, out), p2r(OMEGA, f(P1, Psi), SubPrf), \+(p2r(OMEGA, f(P2, _), _)). p2r(OMEGA, f(P-N, Psi), prf(right(diff), OMEGA, f(P-N), [SubPrf])) :- pos(P, out), neg(N, out), p2r(OMEGA, f(P, Psi), SubPrf), \+(p1(OMEGA, l(N, _), _)). p2r(OMEGA, f(N-P, Psi), prf(right(diff), OMEGA, l(N-P), [SubPrf])) :- neg(N, out), pos(P, out), p1(OMEGA, l(N, Psi), SubPrf), \+(p2r(OMEGA, f(P, _), _)). p2r(OMEGA, f(N1-N2, Psi), prf(right(diff), OMEGA, l(N1-N2), [SubPrf])) :- neg(N1, out), neg(N2, out), p1(OMEGA, l(N1, Psi), SubPrf), \+(p1(OMEGA, l(N2, _), _)). % tsubst(+Phi, +X, +Tin, -Tout) means that the result of substituting % Phi for X in term/type Tin is Tout. tsubst(_, _, V, V) :- var(V), (!). tsubst(Phi, X, X, Phi) :- (!). tsubst(_, _, C, C) :- (atom(C); integer(C)), (!). tsubst(Phi, X, T1, T2) :- T1 =.. [H|T], tsubstlst(Phi, X, T, TT), T2 =.. [H|TT]. tsubstlst(_, _, [], []) :- (!). tsubstlst(Phi, X, [H|T], [HH|TT]) :- tsubst(Phi, X, H, HH), tsubstlst(Phi, X, T, TT). % genins is like genwrap but only inserts individual focused items genins([], Is, Is, []). genins([1|Gamma], [1|Is], Isout, [1|Gamma1]) :- genins(Gamma, Is, Isout, Gamma1). genins([1|Gamma], [f(A, Phi, Int)|Is], Isout, [f(A, Phi, Int)|Gamma1]) :- genins(Gamma, Is, Isout, Gamma1). genins([l(A, Phi, Ls)|Gamma], Isin, Isout, [l(A, Phi, Ls1)|Gamma1]):- geninslst(Ls, Isin, Is, Ls1), genins(Gamma, Is, Isout, Gamma1). genins([b(Stoup: Gamma)|Gamma1], Isin, Isout, [b(Stoup: Gamma2)|Gamma3]) :- genins(Gamma, Isin, Is, Gamma2), genins(Gamma1, Is, Isout, Gamma3). geninslst([], Is, Is, []). geninslst([L|Ls], Isin, Isout, [L1|Ls1]):- genins(L, Isin, Is, L1), geninslst(Ls, Is, Isout, Ls1). % kappend(+S, -L1, -L2, +L) means that L is the concatenation of L1 % and L2 and the length of L1 is the same as that of the sort S. kappend([], [], L, L). kappend([1|S], [H|L1], L2, [H|L]) :- kappend(S, L1, L2, L). configsort(Gamma, M) :- configsort(Gamma, M, []). configsort([], M, M). configsort([1|Gamma], [1|M1], M2) :- configsort(Gamma, M1, M2). configsort([l(_,_,Ls)|Gamma], M1, M3) :- configsortlst(Ls, M1, M2), configsort(Gamma, M2, M3). configsort([f(_,_,Ls)|Gamma], M1, M3) :- configsortlst(Ls, M1, M2), configsort(Gamma, M2, M3). configsort([b(_: Gamma)|Gamma1], M1, M3) :- configsort(Gamma, M1, M2), configsort(Gamma1, M2, M3). configsortlst([], M, M). configsortlst([H|T], M1, M3) :- configsort(H, M1, M2), configsortlst(T, M2, M3). % fold(+S, -Gamma, -Deltas, +Gamma1) means that configuration % Gamma is of sort S and Gamma1 is the result of replacing % in order the separators of Gamma by the configurations in Deltas. fold(S, Gamma, Deltas, Gamma1) :- gfold(S, [], Gamma, Deltas, [], Gamma1). % gfold(+Sin, ?Sout, -Gamma, -Deltasin, ?Deltasout, +Gamma1) % means that configuration % Gamma is of sort Sin-Sout and Gamma1 is the result of replacing % in order the separators of Gamma by the configurations in Deltasin % and Deltasout remain. gfold(S, S, [], Deltas, Deltas, []). gfold([1|S], Sout, [1|Gamma], [Delta|Deltas], Deltasout, Gamma1) :- append(Delta, Gamma2, Gamma1), gfold(S, Sout, Gamma, Deltas, Deltasout, Gamma2). gfold(Sin, Sout, [l(A, Phi, Ls)|Gamma], Deltasin, Deltasout, [l(A, Phi, Ls1)|Gamma1]):- gfoldlst(Sin, S, Ls, Deltasin, Deltas, Ls1), gfold(S, Sout, Gamma, Deltas, Deltasout, Gamma1). gfold(Sin, Sout, [f(A, Phi, Ls)|Gamma], Deltasin, Deltasout, [f(A, Phi, Ls1)|Gamma1]):- gfoldlst(Sin, S, Ls, Deltasin, Deltas, Ls1), gfold(S, Sout, Gamma, Deltas, Deltasout, Gamma1). gfold(Sin, Sout, [b(Stoup: Gamma)|Gamma1], Deltasin, Deltasout, [b(Stoup: Gamma2)|Gamma3]) :- gfold(Sin, S, Gamma, Deltasin, Deltas, Gamma2), gfold(S, Sout, Gamma1, Deltas, Deltasout, Gamma3). gfoldlst(S, S, [], Deltas, Deltas, []). gfoldlst(Sin, Sout, [L|Ls], Deltasin, Deltasout, [L1|Ls1]):- gfold(Sin, S, L, Deltasin, Deltas, L1), gfoldlst(S, Sout, Ls, Deltas, Deltasout, Ls1). % lexical insertion lookuptop(Str, Gamma, A) :- lookup(Str, Gamma, [0,0,0,0,0,0,0,0], [0,0,0,0,0,0,0,0], Minout, Maxout), typecount(min, out, A, Min), listminus(Min, Minout, Mi), allmlezero(Mi), typecount(max, out, A, Max), listminus(Max, Maxout, Ma), allmgezero(Ma). lookup([], [], Min, Max, Min, Max). lookup(Ws, [X|Xs], Minin, Maxin, Minout, Maxout) :- append([H|W1], W2, Ws), lookup1([H|W1], X, MaxV, MinV), listplus(Minin, MaxV, Min), listplus(Maxin, MinV, Max), lookup(W2, Xs, Min, Max, Minout, Maxout). lookup1(Ws, l(A, Phi, []), MaxV, MinV) :- lex(Ws, A, Phi), typecount(max, inp, A, MaxV), typecount(min, inp, A, MinV). lookup1(Ws, l(A, Phi, [Gamma]), MaxV, MinV) :- nappend([W1, W2, W3], Ws), append(W1, [1|W3], W4), lex(W4, A, Phi), lookup(W2, Gamma, [0,0,0,0,0,0,0,0], [0,0,0,0,0,0,0,0], MaxV, MinV). lookup1(Ws, l(A, Phi, [Gamma1, Gamma2]), MaxV, MinV) :- nappend([W1, W2, W3, W4, W5], Ws), nappend([W1, [1|W3], [1|W5]], W6), lex(W6, A, Phi), lookup(W2, Gamma1, [0,0,0,0,0,0,0,0], [0,0,0,0,0,0,0,0], MaxV2, MinV2), lookup(W4, Gamma2, MaxV2, MinV2, MaxV, MinV). lookup1(Ws, l(A, Phi, [[1]]), MaxV, MinV) :- append(W1, W3, Ws), append(W1, [1|W3], W4), lex(W4, A, Phi), typecount(max, inp, A, MaxV), typecount(min, inp, A, MinV). lookup1([b(Ws)], b([]: Gamma), MaxV, MinV) :- lookup(Ws, Gamma, [1,0,0,0,0,0,0,0], [1,0,0,0,0,0,0,0], MaxV, MinV). % ppsem(+out, +Phi) pretty prints semantic form Phi. % ppsem(user, [up, Phi]) :- (!), write('^'), % ppsem(user, Phi). % ppsem(latex(S), [up, Phi]) :- (!), write(S, '\\mbox{\\^{ }}'), % ppsem(latex(S), Phi). % ppsem(user, [dn, Phi]) :- (!), write('v'), % ppsem(user, Phi). % ppsem(latex(S), [dn, Phi]) :- (!), write(S, '\\mbox{\\v{ }}'), % ppsem(latex(S), Phi). ppsem(user, [app, Phi, Psi]) :- (!), write('('), ppsem(user, Phi), write(' '), ppsem(user, Psi), write(')'). ppsem(latex(S), [app, Phi, Psi]) :- (!), write(S, '('), ppsem(latex(S), Phi), write(S, '\\ '), ppsem(latex(S), Psi), write(S, ')'). ppsem(user, [pair, Phi, Psi]) :- (!), write('('), ppsem(user, Phi), write(', '), ppsem(user, Psi), write(')'). ppsem(user, [case, Chi, X, Phi, Y, Psi]) :- (!), write('('), ppsem(user, Chi), write('->'), write(X), write('.'), ppsem(user, Phi), write('; '), write(Y), write('.'), ppsem(user, Psi), write(')'). ppsem(latex(S), [case, Chi, X, Phi, Y, Psi]) :- (!), write(S, '('), ppsem(latex(S), Chi), write(S, '\\rightarrow '), write(S, X), write(S, '.'), ppsem(latex(S), Phi), write(S, '; '), write(S, Y), write(S, '.'), ppsem(latex(S), Psi), write(S, ')'). ppsem(latex(S), [pair, Phi, Psi]) :- (!), write(S, '('), ppsem(latex(S), Phi), write(S, ', '), ppsem(latex(S), Psi), write(S, ')'). ppsem(user, [lmd, X, Phi]) :- (!), write('L'), write(X), ppsem(user, Phi). ppsem(latex(S), [lmd, X, Phi]) :- (!), write(S, '\\lambda '), write(S, X), ppsem(latex(S), Phi). ppsem(latex(S), [mapPhin, N, J]) :- (!), write(S, '({\\Phi^n}^+\\ '), ppsem(latex(S), N), write(S, '\\ '), ppsem(latex(S), J), write(S, ')'). ppsem(latex(S), [mapapply, N, J]) :- (!), write(S, '({\\alpha}^+\\ '), ppsem(latex(S), N), write(S, '\\ '), ppsem(latex(S), J), write(S, ')'). ppsem(latex(S), [listapply, N, J]) :- (!), write(S, '({\\beta}^+\\ '), ppsem(latex(S), N), write(S, '\\ '), ppsem(latex(S), J), write(S, ')'). ppsem(user, [fst, Phi]) :- (!), write('pi1'), ppsem(user, Phi). ppsem(latex(S),[fst, Phi]) :- (!), write(S, '\\pi_1'), ppsem(latex(S), Phi). ppsem(user, [snd, Phi]) :- (!), write('pi2'), ppsem(user,Phi). ppsem(latex(S), [snd, Phi]) :- (!), write(S, '\\pi_2'), ppsem(latex(S), Phi). ppsem(user, [1, Phi]) :- (!), write('iota1'), ppsem(user, Phi). ppsem(latex(S),[1, Phi]) :- (!), write(S, '\\iota_1'), ppsem(latex(S), Phi). ppsem(user, [2, Phi]) :- (!), write('iota2'), ppsem(user,Phi). ppsem(latex(S), [2, Phi]) :- (!), write(S, '\\iota_2'), ppsem(latex(S), Phi). ppsem(user, [iota, X, Phi]) :- (!), write('i'), write(X), ppsem(user, Phi). ppsem(latex(S), [iota, X, Phi]) :- (!), write(S, '\\iota '), write(S, X), ppsem(latex(S), Phi). ppsem(latex(S), iota) :- (!), write(S, '\\iota '). ppsem(user, [xst, X, Phi]) :- (!), write('E'), write(X), ppsem(user, Phi). ppsem(latex(S), [xst, X, Phi]) :- (!), write(S, '\\exists '), write(S, X), ppsem(latex(S), Phi). ppsem(user, [all, X, Phi]) :- (!), write('A'), write(X), ppsem(user, Phi). ppsem(latex(S), [all, X, Phi]) :- (!), write(S, '\\forall '), write(S, X), ppsem(latex(S), Phi). ppsem(user, [xst2, X, Phi]) :- (!), write('E^2'), write(X), ppsem(user, Phi). ppsem(latex(S), [xst2, X, Phi]) :- (!), write(S, '\\exists^2'), write(S, X), ppsem(S, Phi). ppsem(user, [up, Phi]) :- (!), write('^'), ppsem(user, Phi). ppsem(latex(S), [up, Phi]) :- (!), write(S, '\\mbox{\\^{}}'), ppsem(latex(S), Phi). ppsem(user, [dn, Phi]) :- (!), write('v'), ppsem(user, Phi). ppsem(latex(S), [dn, Phi]) :- (!), write(S, '\\mbox{\\v{}}'), ppsem(latex(S), Phi). ppsem(user, [or, Phi, Psi]) :- (!), write('['), ppsem(user, Phi), write(' v '), ppsem(user, Psi), write(']'). ppsem(latex(S), [or, Phi, Psi]) :- (!), write(S, '['), ppsem(latex(S), Phi), write(S, '\\vee '), ppsem(latex(S), Psi), write(S, ']'). ppsem(user, [and, Phi, Psi]) :- (!), write('['), ppsem(user, Phi), write(' & '), ppsem(user, Psi), write(']'). ppsem(latex(S), [and, Phi, Psi]) :- (!), write(S, '['), ppsem(latex(S), Phi), write(S, '\\wedge '), ppsem(latex(S), Psi), write(S, ']'). ppsem(user, [imply, Phi, Psi]) :- (!), write('['), ppsem(user, Phi), write(' -> '), ppsem(user, Psi), write(']'). ppsem(latex(S), [imply, Phi, Psi]) :- (!), write(S, '['), ppsem(latex(S), Phi), write(S, '\\rightarrow '), ppsem(latex(S), Psi), write(S, ']'). ppsem(user, [eq, Phi, Psi]) :- (!), write('['), ppsem(user, Phi), write(' = '), ppsem(user, Psi), write(']'). ppsem(latex(S), [eq, Phi, Psi]) :- (!), write(S, '['), ppsem(latex(S), Phi), write(S, '='), ppsem(latex(S), Psi), write(S, ']'). ppsem(user, [more_than, Phi, Psi]) :- (!), write('['), ppsem(user, Phi), write(' > '), ppsem(user, Psi), write(']'). ppsem(latex(S), [more_than, Phi, Psi]) :- (!), write(S, '['), ppsem(latex(S), Phi), write(S, '>'), ppsem(latex(S), Psi), write(S, ']'). ppsem(user, [group, Phi, Psi]) :- (!), write('['), ppsem(user, Phi), write(' grp '), ppsem(user, Psi), write(']'). ppsem(latex(S), [group, Phi, Psi]) :- (!), write(S, '['), ppsem(latex(S), Phi), write(S, ' grp '), ppsem(latex(S), Psi), write(S, ']'). ppsem(user, [plusubset, Phi, Psi]) :- (!), write('['), ppsem(user, Phi), write(' pss '), ppsem(user, Psi), write(']'). ppsem(latex(S), [plusubset, Phi, Psi]) :- (!), write(S, '['), ppsem(latex(S), Phi), write(S, ' pss '), ppsem(latex(S), Psi), write(S, ']'). ppsem(user, [card, Phi]) :- (!), write('|'), ppsem(user, Phi), write('|'). ppsem(latex(S), [card, Phi]) :- (!), write(S, '|'), ppsem(latex(S), Phi), write(S, '|'). ppsem(user, [when, Phi, Psi]) :- (!), write('['), ppsem(user, Psi), write(' when '), ppsem(user, Phi), write(']'). ppsem(latex(S), [when, Phi, Psi]) :- (!), write(S, '['), ppsem(latex(S), Psi), write(' when '), ppsem(latex(S), Phi), write(S, ']'). ppsem(user, [not, Phi]) :- (!), write('-'), ppsem(user, Phi). ppsem(latex(S), [not, Phi]) :- (!), write(S, '\\neg '), ppsem(latex(S), Phi). ppsem(user, Phi) :- write(Phi). ppsem(latex(Stream), Phi) :- write(Stream, '{\\it '), write(Stream, Phi), write(Stream, '}'). % eval(+Phi, -NF) means that NF is the result of normalising the % semantic form Phi eval(Phi, NF) :- numbervars(Phi, 0, _), eval1(Phi, NF). % eval1(+Phi, -NF) means that NF is the result of normalising % the frozen semantic form Phi eval1(Phi, NF) :- contract(Phi, Phi1), (!), eval1(Phi1, NF). eval1(Phi, Phi). % contract(+Phi, -Phi1) means that Phi1 is the result of applying one % contraction step to the frozen semantic form Phi contract([app, [lmd, X, Phi], Psi], Chi) :- subst(Psi, X, Phi, Chi). contract([fst, [pair, X, _]], X). contract([snd, [pair, _, Y]], Y). contract([case, [1, Chi], X, Phi, _, _], Omega) :- subst(Chi, X, Phi, Omega). contract([case, [2, Chi], _, _, Y, Psi], Omega) :- subst(Chi, Y, Psi, Omega). contract([dn, [up, Phi]], Phi). contract([H|T], [H|T1]) :- contractlist(T, T1). contract([mapapply, [X], Z], [[app, X, Z]]). contract([mapapply, [X, Y|L], Z], [[app, X, Z]|[mapapply, [Y|L], Z]]). contract([app, [app, [mapPhin, 0, J], Z], [X]], [J, X, Z]). contract([app, [app, [mapPhin, 0, J], Z], [X, Y|L]], [J, X, [app, [app, [mapPhin, 0, J], Z], [Y|L]]]). contract([app, [app, [app, [mapPhin, [app, s, N], J], Y], L], Z], [app, [app, [mapPhin, N, J], [app, Y, Z]], [mapapply, L, Z]]). contract([listapply, [X], [Z]], [[app, X, Z]]). contract([listapply, [X, Y|L], [Z|W]], [[app, X, Z]|[listapply, [Y|L], W]]). contract([eq, Phi, Phi], true). contract([and, Phi, true], Phi). contract([and, true, Phi], Phi). contractlist([Phi|Phis], [Phi1|Phis]) :- contract(Phi, Phi1). contractlist([Phi|Phis], [Phi|Phis1]) :- contractlist(Phis, Phis1). % subst(+Phi, +X, +Psi, -NPsi) means that NPsi is the result of replacing % by Phi all Xs in the frozen semantic form Psi subst(Phi, X, X, Phi) :- (!). subst(_, _, C, C) :- atom(C), (!). subst(_, _, C, C) :- integer(C), (!). subst(_, _, X, X) :- X = '$VAR'(_), (!). subst(Phi, X, [H|T], [H1|T1]) :- subst(Phi, X, H, H1), subst(Phi, X, T, T1). subst(_, _, [], []). % pppros(+Out, +Pros) pretty prints prosodic form Pros. pppros(user, [b(Ws)]) :- (!), write('['), pppros(user, Ws), write(']'). pppros(user, [b(Ws)|Ws2]) :- (!), write('['), pppros(user, Ws), write(']'), write('+'), pppros(user, Ws2). pppros(user, [W]) :- (!), write(W). pppros(user, [W1, W2|Ws]) :- (!), write(W1), write('+'), pppros(user, [W2|Ws]). pppros(user, Alpha) :- write(Alpha). pppros(latex(S), [b(Ws)]) :- (!), write(S, '['), pppros(latex(S), Ws), write(S, ']'). pppros(latex(S), [b(Ws)|Ws2]) :- (!), write(S, '['), pppros(latex(S), Ws), write(S, ']'), write(S, '{+}'), pppros(latex(S), Ws2). pppros(latex(S), [W]) :- (!), write(S, '{\\bf '), write(S, W), write(S, '}'). pppros(latex(S), [W1, W2|Ws]) :- (!), write(S, '{\\bf '), write(S, W1), write(S, '}'), write(S, '{+}'), pppros(latex(S), [W2|Ws]). pppros(latex(S), Alpha) :- write(S, Alpha). % pptype(+Out, +A) pretty prints type A. pptype(Out, A) :- (!), pptype(Out, outer, A). % pptype(+Out, +M, +A) pretty prints type A omitting outer parentheses % if M IS 'outer' but not if it is 'inner'. pptype(user, _, n(G)) :- (!), write('N'), write(G). pptype(user, _, s(F)) :- (!), write('S'), write(F). pptype(user, _, cp(C)) :- (!), write('CP'), write(C). pptype(user, _, pp(F)) :- (!), write('PP'), write(F). pptype(user, _, cn(G)) :- (!), write('CN'), write(G). pptype(user, _, si) :- (!), write('Si'). pptype(user, _, q) :- (!), write('Q'). pptype(user, M, A bs C) :- (!), % 1 doopenparen(user, M, A), write('\\'), docloseparen(user, M, C). pptype(user, M, C/B) :- (!), % 2 doopenparen(user, M, C), write('/'), docloseparen(user, M, B). pptype(user, M, A*B) :- (!), % 3 doopenparen(user, M, A), write('*'), docloseparen(user, M, B). pptype(user, _, i) :- (!), write('I'). % 4 pptype(user, M, A in C) :- (!), % 5+ doopenparen(user, M, A), write('in'), docloseparen(user, M, C). pptype(user, M, A inn C) :- (!), % 5- doopenparen(user, M, A), write('inn'), docloseparen(user, M, C). pptype(user, M, C ci B) :- (!), % 6+ doopenparen(user, M, C), write('ci'), docloseparen(user, M, B). pptype(user, M, C cin B) :- (!), % 6- doopenparen(user, M, C), write('cin'), docloseparen(user, M, B). pptype(user, M, A dp B) :- (!), % 7+ doopenparen(user, M, A), write('dp'), docloseparen(user, M, B). pptype(user, M, A dpn B) :- (!), % 7- doopenparen(user, M, A), write('dpn'), docloseparen(user, M, B). pptype(user, _, j) :- (!), write('J'). % 8 pptype(user, M, A&B) :- (!), % 9 doopenparen(user, M, A), write('&'), docloseparen(user, M, B). pptype(user, M, A+B) :- (!), % 10 doopenparen(user, M, A), write('+'), docloseparen(user, M, B). pptype(user, _, X u A) :- (!), % 11 write('AA'), write(X), pptype(user, inner, A). pptype(user, _, X e A) :- (!), % 12 write('AE'), write(X), pptype(user, inner, A). pptype(user, _, nL A) :- (!), % 13 write(nL), pptype(user, inner, A). pptype(user, _, nM A) :- (!), % 14 write(nM), pptype(user, inner, A). pptype(user, _, ab A) :- (!), % 15 write('[]-1'), pptype(user, inner, A). pptype(user, _, br A) :- (!), % 16 write('<>'), pptype(user, inner, A). pptype(user, _, ue A) :- (!), % 17 write(ue), pptype(user, inner, A). pptype(user, _, ee A) :- (!), % 18 write(ee), pptype(user, inner, A). pptype(user, _, M een A) :- (!), write(ee), write(M), pptype(user, inner, A). pptype(user, M, A lca B) :- (!), % 19 doopenparen(user, M, A), write(' lca '), docloseparen(user, M, B). pptype(user, _, w(W)) :- (!), % 20 write('W'), write(W). pptype(user, M, A liu C) :- (!), % 21 doopenparen(user, M, A), write('-o'), docloseparen(user, M, C). pptype(user, M, C lio B) :- (!), % 22 doopenparen(user, M, B), write('*-'), docloseparen(user, M, C). pptype(user, M, A lip B) :- (!), % 23 doopenparen(user, M, A), write('.o'), docloseparen(user, M, B). pptype(user, M, A riu C) :- (!), % 24 doopenparen(user, M, A), write('-*'), docloseparen(user, M, C). pptype(user, M, C rio B) :- (!), % 25 doopenparen(user, M, C), write('o-'), docloseparen(user, M, B). pptype(user, M, A rip B) :- (!), % 26 doopenparen(user, M, A), write('o.'), docloseparen(user, M, B). pptype(user, M, A uii C) :- (!), % 27+ doopenparen(user, M, A), write('uii'), docloseparen(user, M, C). pptype(user, M, A uiin C) :- (!), % 27- doopenparen(user, M, A), write('uiin'), docloseparen(user, M, C). pptype(user, M, C uic B) :- (!), % 28+ doopenparen(user, M, C), write('uic'), docloseparen(user, M, B). pptype(user, M, C uicn B) :- (!), % 28+ doopenparen(user, M, C), write('uicn'), docloseparen(user, M, B). pptype(user, M, A uidp B) :- (!), % 29+ doopenparen(user, M, A), write('uidp'), docloseparen(user, M, B). pptype(user, M, A uidpn B) :- (!), % 29- doopenparen(user, M, A), write('uidpn'), docloseparen(user, M, B). pptype(user, M, A lii C) :- (!), % 30+ doopenparen(user, M, A), write('lii'), docloseparen(user, M, C). pptype(user, M, A liin C) :- (!), % 30- doopenparen(user, M, A), write('liin'), docloseparen(user, M, C). pptype(user, M, C lic B) :- (!), % 31+ doopenparen(user, M, B), write('lic'), docloseparen(user, M, C). pptype(user, M, C licn B) :- (!), % 31- doopenparen(user, M, C), write('lic'), docloseparen(user, M, B). pptype(user, M, A lidp B) :- (!), % 32+ doopenparen(user, M, A), write('lidp'), docloseparen(user, M, B). pptype(user, M, A lidpn B) :- (!), % 32- doopenparen(user, M, A), write('lidpn'), docloseparen(user, M, B). pptype(user, M, A iac B) :- (!), % 33 doopenparen(user, M, A), write('|&|'), docloseparen(user, M, B). pptype(user, M, A iad B) :- (!), % 34 doopenparen(user, M, A), write('|+|'), docloseparen(user, M, B). pptype(user, _, X iu A) :- (!), % 35 write('A'), write(X), pptype(user, inner, A). pptype(user, _, X ie A) :- (!), % 36 write('E'), write(X), pptype(user, inner, A). pptype(user, _, iL A) :- (!), % 37 write('iL'), pptype(user, inner, A). pptype(user, _, iM A) :- (!), % 38 write('iM'), pptype(user, inner, A). pptype(user, _, lp A) :- (!), % 39 write('<|-1'), pptype(user, inner, A). pptype(user, _, li A) :- (!), % 40 write('<|'), pptype(user, inner, A). pptype(user, _, rp A) :- (!), % 41 write('|>-1'), pptype(user, inner, A). pptype(user, _, ri A) :- (!), % 42 write('|>'), pptype(user, inner, A). pptype(user, _, sp A) :- (!), % 43+ write('v'), pptype(user, inner, A). pptype(user, _, spn A) :- (!), % 43- write('v-'), pptype(user, inner, A). pptype(user, _, bg A) :- (!), % 44+ write('^'), pptype(user, inner, A). pptype(user, _, bgn A) :- (!), % 44- write('^-'), pptype(user, inner, A). pptype(user, M, C nd B) :- (!), % 45 doopenparen(user, M, C), write('nd'), docloseparen(user, M, B). pptype(user, M, A np B) :- (!), % 46 doopenparen(user, M, A), write('np'), docloseparen(user, M, B). pptype(user, M, A nin C) :- (!), % 47 doopenparen(user, M, A), write('nin'), docloseparen(user, M, C). pptype(user, M, C nci B) :- (!), % 48 doopenparen(user, M, C), write('nci'), docloseparen(user, M, B). pptype(user, M, A ndp B) :- (!), % 49 doopenparen(user, M, A), write('nwrap'), docloseparen(user, M, B). pptype(user, M, A-B) :- (!), % 50 doopenparen(user, M, A), write('-'), docloseparen(user, M, B). pptype(latex(S), _, n(G)) :- (!), write(S, 'N'), write(S, G). pptype(latex(S), _, s(F)) :- (!), write(S, 'S'), write(S, F). pptype(latex(S), _, cp(C)) :- (!), write(S, '{\\it CP}'), write(S, C). pptype(latex(S), _, pp(F)) :- (!), write(S, '{\\it PP}'), write(S, '{\\it '), write(S, F), write(S, '}'). pptype(latex(S), _, cn(G)) :- (!), write(S, '{\\it CN}'), write(S, '{\\it '), write(S, G), write(S, '}'). pptype(latex(S), _, si) :- (!), write(S, 'Si'). pptype(latex(S), _, q) :- (!), write(S, 'Q'). pptype(latex(S), M, A bs C) :- (!), % 1 doopenparen(latex(S), M, A), write(S, '\\backslash '), docloseparen(latex(S), M, C). pptype(latex(S), M, C/B) :- (!), % 2 doopenparen(latex(S), M, C), write(S, '/'), docloseparen(latex(S), M, B). pptype(latex(S), M, A*B) :- (!), % 3 doopenparen(latex(S), M, A), write(S, '{\\bullet}'), docloseparen(latex(S), M, B). pptype(latex(S), _, i) :- (!), % 4 write(S, 'I'). pptype(latex(S), M, A in C) :- (!), % 5+ doopenparen(latex(S), M, A), write(S, '{\\stackrel{\\downarrow}{}}'), docloseparen(latex(S), M, C). pptype(latex(S), M, A inn C) :- (!), % 5- doopenparen(latex(S), M, A), write(S, '{\\stackrel{\\downarrow}{_{_-}}}'), docloseparen(latex(S), M, C). pptype(latex(S), M, C ci B) :- (!), % 6+ doopenparen(latex(S), M, C), write(S, '{\\stackrel{\\uparrow}{}}'), docloseparen(latex(S), M, B). pptype(latex(S), M, C cin B) :- (!), % 6- doopenparen(latex(S), M, C), write(S, '{\\stackrel{\\uparrow}{_{_-}}}'), docloseparen(latex(S), M, B). pptype(latex(S), M, A dp B) :- (!), % 7+ doopenparen(latex(S), M, A), write(S, '{\\stackrel{\\odot}{}}'), docloseparen(latex(S), M, B). pptype(latex(S), M, A dpn B) :- (!), % 7- doopenparen(latex(S), M, A), write(S, '{\\stackrel{\\odot}{_{_-}}}'), docloseparen(latex(S), M, B). pptype(latex(S), _, j) :- % 8 (!), write(S, 'J'). pptype(latex(S), M, A&B) :- (!), % 9 doopenparen(latex(S), M, A), write(S, '{\\&}'), docloseparen(latex(S), M, B). pptype(latex(S), M, A+B) :- (!), % 10 doopenparen(latex(S), M, A), write(S, '{\\oplus}'), docloseparen(latex(S), M, B). pptype(latex(S), _, X u A) :- (!), % 11 write(S, '{\\bigwedge}'), write(S, X), pptype(latex(S), inner, A). pptype(latex(S), _, X e A) :- (!), % 12 write(S, '{\\bigvee}'), write(S, X), pptype(latex(S), inner, A). pptype(latex(S), _, nL A) :- (!), % 13 write(S, '{\\square}'), pptype(latex(S), inner, A). pptype(latex(S), _, nM A) :- (!), % 14 write(S, '{\\Diamond}'), pptype(latex(S), inner, A). pptype(latex(S), _, ab A) :- (!), % 15 write(S, '{[]^{-1}}'), pptype(latex(S), inner, A). pptype(latex(S), _, br A) :- (!), % 16 write(S, '{\\langle\\rangle}'), pptype(latex(S), inner, A). pptype(latex(S), _, ue A) :- (!), % 17 write(S, '!'), pptype(latex(S), inner, A). pptype(latex(S), _, ee A) :- (!), % 18 write(S, '?'), pptype(latex(S), inner, A). pptype(latex(S), _, M een A) :- (!), write(S, '?'), write(S, '_'), write(S, M), pptype(latex(S), inner, A). pptype(latex(S), M, B lca A) :- (!), % 19 doopenparen(latex(S), M, B), write(S, '{|}'), docloseparen(latex(S), M, A). pptype(latex(S), _, w(W)) :- (!), % 20 write(S, 'W'), write(S, W). pptype(latex(S), M, A liu C) :- (!), % 21 doopenparen(latex(S), M, A), write(S, '{\\multimap}'), docloseparen(latex(S), M, C). pptype(latex(S), M, C lio B) :- (!), % 22 doopenparen(latex(S), M, B), write(S, '{\\multimapdotinv}'), docloseparen(latex(S), M, C). pptype(latex(S), M, A lip B) :- (!), % 23 doopenparen(latex(S), M, A), write(S, '{\\LEFTcircle}'), docloseparen(latex(S), M, B). pptype(latex(S), M, A riu C) :- (!), % 24 doopenparen(latex(S), M, A), write(S, '{\\multimapdot}'), docloseparen(latex(S), M, C). pptype(latex(S), M, C rio B) :- (!), % 25 doopenparen(latex(S), M, C), write(S, '{\\multimapinv}'), docloseparen(latex(S), M, B). pptype(latex(S), M, A rip B) :- (!), % 26 doopenparen(latex(S), M, A), write(S, '{\\RIGHTcircle}'), docloseparen(latex(S), M, B). pptype(latex(S), M, A uii C) :- (!), % 27+ doopenparen(latex(S), M, A), write(S, '{\\stackrel{%\\begin{picture}(7,8)(0,-2)\\put(0.7,7){\\rotatebox{-90}{$\\multimap$}}\\end{picture}}{_{}}}'), docloseparen(latex(S), M, C). pptype(latex(S), M, A uiin C) :- (!), % 27- doopenparen(latex(S), M, A), write(S, '{\\stackrel{\\begin{picture}(7,8)(0,-2)\\put(0.7,7){\\rotatebox{-90}{$\\multimap$}}\\end{picture}}{_{_-}}}'), docloseparen(latex(S), M, C). pptype(latex(S), M, C uic B) :- (!), % 28+ doopenparen(latex(S), M, C), write(S, '{\\stackrel{\\begin{picture}(7,7)(0,-2)\\put(1.5,-3){\\rotatebox{90}{$\\multimapdot$}}\\end{picture}}{_{}}}'), docloseparen(latex(S), M, B). pptype(latex(S), M, C uicn B) :- (!), % 28- doopenparen(latex(S), M, C), write(S, '{\\stackrel{\\begin{picture}(7,7)(0,-2)\\put(1.5,-3){\\rotatebox{90}{$\\multimapdot$}}\\end{picture}}{_{_-}}}'), docloseparen(latex(S), M, B). pptype(latex(S), M, A uidp B) :- (!), % 29+ doopenparen(latex(S), M, A), write(S, '{\\stackrel{\\begin{picture}(7,7)(0,0)\\put(0,5.5){\\rotatebox{-90}{$\\LEFTcircle$}}\\end{picture}}{_{}}}'), docloseparen(latex(S), M, B). pptype(latex(S), M, A uidpn B) :- (!), % 29- doopenparen(latex(S), M, A), write(S, '{\\stackrel{\\begin{picture}(7,7)(0,0)\\put(0,5.5){\\rotatebox{-90}{$\\LEFTcircle$}}\\end{picture}}{_{_-}}}'), docloseparen(latex(S), M, B). pptype(latex(S), M, A lii C) :- (!), % 30+ doopenparen(latex(S), M, A), write(S, '{\\stackrel{\\begin{picture}(7,8)(0,-2)\\put(0.7,7){\\rotatebox{-90}{$\\multimapdot$}}\\end{picture}}{_{}}}'), docloseparen(latex(S), M, C). pptype(latex(S), M, A liin C) :- (!), % 30- doopenparen(latex(S), M, A), write(S, '{\\stackrel{\\begin{picture}(7,8)(0,-2)\\put(0.7,7){\\rotatebox{-90}{$\\multimapdot$}}\\end{picture}}{_{_-}}}'), docloseparen(latex(S), M, C). pptype(latex(S), M, C lic B) :- (!), % 31+ doopenparen(latex(S), M, B), write(S, '{\\stackrel{\\begin{picture}(7,7)(0,-2)\\put(1.5,-3){\\rotatebox{90}{$\\multimap$}}\\end{picture}}{_{}}}'), docloseparen(latex(S), M, C). pptype(latex(S), M, C licn B) :- (!), % 31- doopenparen(latex(S), M, C), write(S, '{\\stackrel{\\begin{picture}(7,7)(0,-2)\\put(1.5,-3){\\rotatebox{90}{$\\multimap$}}\\end{picture}}{_{_-}}}'), docloseparen(latex(S), M, B). pptype(latex(S), M, A lidp B) :- (!), % 32+ doopenparen(latex(S), M, A), write(S, '{\\stackrel{\\begin{picture}(7,7)(0,0)\\put(0,5.5){\\rotatebox{-90}{$\\RIGHTcircle$}}\\end{picture}}{_{}}}'), docloseparen(latex(S), M, B). pptype(latex(S), M, A lidpn B) :- (!), % 32- doopenparen(latex(S), M, A), write(S, '{\\stackrel{\\begin{picture}(7,7)(0,0)\\put(0,5.5){\\rotatebox{-90}{$\\RIGHTcircle$}}\\end{picture}}{_{_-}}}'), docloseparen(latex(S), M, B). pptype(latex(S), M, A iac B) :- (!), % 33 doopenparen(latex(S), M, A), write(S, '{\\sqcap}'), docloseparen(latex(S), M, B). pptype(latex(S), M, A iad B) :- (!), % 34 doopenparen(latex(S), M, A), write(S, '{\\sqcup}'), docloseparen(latex(S), M, B). pptype(latex(S), _, X iu A) :- (!), % 35 write(S, '{\\forall}'), write(S, X), pptype(latex(S), inner, A). pptype(latex(S), _, X ie A) :- (!), % 36 write(S, '{\\exists}'), write(S, X), pptype(latex(S), inner, A). pptype(latex(S), _, iL A) :- (!), % 37 write(S, '{\\blacksquare}'), pptype(latex(S), inner, A). pptype(latex(S), _, iM A) :- (!), % 38 write(S, '{\\blacklozenge}'), pptype(latex(S), inner, A). pptype(latex(S), _, lp A) :- (!), % 39 write(S, '\\mbox{$\\lhd^{-1}$}'), pptype(latex(S), inner, A). pptype(latex(S), _, li A) :- (!), % 40 write(S, '\\mbox{$\\lhd$}'), pptype(latex(S), inner, A). pptype(latex(S), _, rp A) :- (!), % 41 write(S, '\\mbox{$\\rhd^{-1}$}'), pptype(latex(S), inner, A). pptype(latex(S), _, ri A) :- (!), % 42 write(S, '\\mbox{$\\rhd$}'), pptype(latex(S), inner, A). pptype(latex(S), _, sp A) :- (!), % 43+ write(S, '\\mbox{$\\check{\\ }$}'), pptype(latex(S), inner, A). pptype(latex(S), _, spn A) :- (!), % 43- write(S, '\\mbox{$\\check{_{_-}}$}'), pptype(latex(S), inner, A). pptype(latex(S), _, bg A) :- (!), % 44+ write(S, '\\mbox{$\\hat{\\ }$}'), pptype(latex(S), inner, A). pptype(latex(S), _, bgn A) :- (!), % 44- write(S, '\\mbox{$\\hat{_{_-}}$}'), pptype(latex(S), inner, A). pptype(latex(S), M, C nd B) :- (!), % 45 doopenparen(latex(S), M, C), write(S, '{\\div}'), docloseparen(latex(S), M, B). pptype(latex(S), M, A np B) :- (!), % 46 doopenparen(latex(S), M, A), write(S, '{\\times}'), docloseparen(latex(S), M, B). pptype(latex(S), M, A nin C) :- (!), % 47 doopenparen(latex(S), M, A), write(S, '{\\Downarrow}'), docloseparen(latex(S), M, C). pptype(latex(S), M, C nci B) :- (!), % 48 doopenparen(latex(S), M, C), write(S, '{\\Uparrow}'), docloseparen(latex(S), M, B). pptype(latex(S), M, A ndp B) :- (!), % 49 doopenparen(latex(S), M, A), write(S, '\\mbox{\\footnotesize\\begin{picture}(0,0)\\put(2.2, 1){$\\circ$}\\put(0, 1){$\\bigcirc$}\\end{picture}\\ \\ \\ }'), docloseparen(latex(S), M, B). pptype(latex(S), M, A-B) :- (!), % 50 doopenparen(latex(S), M, A), write(S, '{-}'), docloseparen(latex(S), M, B). pptype(user, _, A) :- write(A). pptype(latex(Stream), _, A) :- write(Stream, A). pptypelst(user, [A]) :- (!), pptype(user, outer, A). pptypelst(user, [H|T]) :- pptype(user, outer, H), write(', '), pptypelst(user, T). pptypelst(latex(S), [A]) :- (!), pptype(latex(S), outer, A). pptypelst(latex(S), [H|T]) :- pptype(latex(S), outer, H), write(S, ', '), pptypelst(latex(S), T). doopenparen(user, inner, A) :- write('('),pptype(user, inner, A). doopenparen(user, outer, A) :- pptype(user, inner, A). doopenparen(latex(S), inner, A) :- write(S, '('),pptype(latex(S), inner, A). doopenparen(latex(S), outer, A) :- pptype(latex(S), inner, A). docloseparen(user, inner, A) :- pptype(user, inner, A), write(')'). docloseparen(user, outer, A) :- pptype(user, inner, A). docloseparen(latex(S), inner, A) :- pptype(latex(S), inner, A), write(S, ')'). docloseparen(latex(S), outer, A) :- pptype(latex(S), inner, A). pplex :- lex(Alpha, A, Phi), numbervars((A, Phi), 0, _), pppros(user, Alpha), write(': '), pptype(user, A), write(': '), numbervars(Phi, 0, _), ppsem(user, Phi), nl, fail. pplex. pplexlatex :- open('lex.tex', write, S), nl(S), pplexlatex(S). pplexlatex(S) :- nl(S), write(S, '$'),%\\begin{array}{l} lex(Alpha, A, Phi), numbervars((A, Phi), 0, _), nl(S), pppros(latex(S), Alpha), write(S, ': '), pptype(latex(S), A), write(S, ': '), numbervars(Phi, 0, _), ppsem(latex(S), Phi), write(S, '\\\\'), fail. pplexlatex(S) :- write(S, '$'), nl(S),%\\end{array} close(S). % ppconfig(Out, +S, +Gamma) pretty prints the configuration Gamma % including semantics if S is 'yes' but not if it is 'no'. It writes % to the user if Out is 'user' and writes to Stream if Out is % latex(Stream). ppconfig(_, _, []). ppconfig(Out, S, [F]) :- ppfactor(Out, S, F). ppconfig(user, S, [F1, F2|Gamma]) :- ppfactor(user, S, F1), write(', '), ppconfig(user, S, [F2|Gamma]). ppconfig(latex(Stream), S, [F1, F2|Gamma]) :- ppfactor(latex(Stream), S, F1), write(Stream, ', '), ppconfig(latex(Stream), S, [F2|Gamma]). ppfactor(user, _, 1) :- write('1'). ppfactor(latex(Stream), _, 1) :- write(Stream, '{\\tt 1}'). ppfactor(Stream, S, l(A, Phi, Ls)) :- pptypefactor(Stream, S, A, Ls), dosem(Stream, S, Phi). ppfactor(user, S, f(A, Phi, Ls)) :- pptypefactor(user, S, A, Ls), dosem(user, S, Phi). ppfactor(latex(Stream), S, f(A, Phi, Ls)) :- write(Stream, '\\mbox{\\fbox{$'), pptypefactor(latex(Stream), S, A, Ls), dosem(latex(Stream), S, Phi), write(Stream, '$}}'). ppfactor(user, S, b([]: Gamma)) :- write('['), ppconfig(user, S, Gamma), write(']'). ppfactor(latex(Stream), S, b([]: Gamma)) :- write(Stream, '['), ppconfig(latex(Stream), S, Gamma), write(Stream, ']'). ppfactor(user, S, b([H|T]: Gamma)) :- write('['), ppconfig(user, S, [H|T]), write(';'), ppconfig(user, S, Gamma), write(']'). ppfactor(latex(Stream), S, b([]: Gamma)) :- write(Stream, '['), ppconfig(latex(Stream), S, Gamma), write(Stream, ']'). ppfactor(latex(Stream), S, b([H|T]: Gamma)) :- write(Stream, '['), ppconfig(latex(Stream), S, [H|T]), write(Stream, ';'), ppconfig(latex(Stream), S, Gamma), write(Stream, ']'). dosem(user, yes, Phi) :- write(': '), assert(copy(Phi)), retract(copy(Phi1)), numbervars(Phi1, 0, _), ppsem(user, Phi1). dosem(latex(Stream), yes, Phi) :- write(Stream, ': '), assert(copy(Phi)), retract(copy(Phi1)), numbervars(Phi1, 0, _), ppsem(latex(Stream), Phi1). dosem(_, no, _). pptypefactor(Out, _, A, []) :- pptype(Out, outer, A). pptypefactor(user, S, A, [L|Ls]) :- pptype(user, A), write('{'), ppconfiglst(user, S, [L|Ls]), write('}'). pptypefactor(latex(Stream), S, A, [L|Ls]) :- pptype(latex(Stream), A), write(Stream, '\\{'), ppconfiglst(latex(Stream), S, [L|Ls]), write(Stream, '\\}'). ppconfiglst(Out, S, [L]) :- ppconfig(Out, S, L). ppconfiglst(user, S, [L1, L2|Ls]) :- ppconfig(user, S, L1), write(' : '), ppconfiglst(user, S, [L2|Ls]). ppconfiglst(latex(Stream), S, [L1, L2|Ls]) :- ppconfig(latex(Stream), S, L1), write(Stream, ': '), ppconfiglst(latex(Stream), S, [L2|Ls]). % ppseq(+Out, +S, +Gamma, +A) pretty prints the sequent Gamma => A % including semantics if S is 'yes' but not if it is 'no'. It writes % to the user if Out is 'user' and writes to Stream if Out is % latex(Stream). ppseq(Out, S, Gamma, A) :- \+(\+((numbervars((Gamma, A), 0, _), ppseq2(Out, S, Gamma, A)))). ppseq2(user, S, []: Gamma, A) :- ppconfig(user, S, Gamma), write(' => '), ppsucc(user, A). ppseq2(user, S, [H|T]: Gamma, A) :- ppconfig(user, S, [H|T]), write('; '), ppconfig(user, S, Gamma), write(' => '), ppsucc(user, A). ppseq2(latex(Stream), S, []: Gamma, A) :- ppconfig(latex(Stream), S, Gamma), write(Stream,'\\ \\Rightarrow\\ '), ppsucc(latex(Stream), A). ppseq2(latex(Stream), S, [H|T]: Gamma, A) :- ppconfig(latex(Stream), S, [H|T]), write(Stream, ';\\ '), ppconfig(latex(Stream), S, Gamma), write(Stream,'\\ \\Rightarrow\\ '), ppsucc(latex(Stream), A). ppsucc(user, l(A)) :- pptype(user, outer, A). ppsucc(user, f(A)) :- pptype(user, outer, A). ppsucc(latex(Stream), l(A)) :- pptype(latex(Stream), outer, A). ppsucc(latex(Stream), f(A)) :- write(Stream, '\\fbox{$'), pptype(latex(Stream), outer, A), write(Stream, '$}'). % ppprf(+Out +S, +N, Prf) pretty prints sequent proof Prf at indentation % N including semantics if S is 'yes' but not if it is 'no'. It writes % to the user if Out is 'user' and writes to Stream if Out is % latex(Stream). ppprf(user, S, N, prf(id, Gamma, A, [])) :- (!), dotab(N), ppseq(user, S, Gamma, A). ppprf(user, S, N, prf(Rule, Gamma, A, SubPrfs)) :- dotab(N), ppseq(user, S, Gamma, A), write(' ['), writerule(user, Rule), write(']'), ppprflst(user, S, s(s(s(s(N)))), SubPrfs). ppprf(latex(Stream), S, N, Prf) :- nl(Stream), write(Stream, '\\resizebox{\\textwidth}{!}{'), ppprf2(latex(Stream), S, N, Prf), write(Stream, '}'). ppprf2(latex(Stream), S, _, prf(id, Gamma, A, [])) :- (!), nl(Stream), write(Stream, '\\prooftree'), nl(Stream), write(Stream, '\\justifies'), nl(Stream), ppseq(latex(Stream), S, Gamma, A), nl(Stream), write(Stream, '\\endprooftree'). ppprf2(latex(Stream), S, _, prf(Rule, Gamma, A, SubPrfs)) :- nl(Stream), write(Stream, '\\prooftree'), ppprflst2(latex(Stream), S, _, SubPrfs), nl(Stream), write(Stream, '\\justifies'), nl(Stream), ppseq(latex(Stream), S, Gamma, A), nl(Stream), write(Stream, '\\using '), writerule(latex(Stream), Rule), nl(Stream), write(Stream, '\\endprooftree'). ppprflst(user, _, _, []). ppprflst(user, S, N, [H|T]) :- nl, ppprf(user,S, N, H), ppprflst(user, S, N, T). ppprflst2(latex(_), _, _, []). ppprflst2(latex(Stream), S, N, [H|T]) :- ppprf2(latex(Stream),S, N, H), ppprflst2(latex(Stream), S, N, T). dotab(0). dotab(s(N)) :- write(' '), dotab(N). connwriting(under, '\\', '{\\backslash}'). % 1 connwriting(over, '/', '{/}'). % 2 connwriting(product, '*', '{\\bullet}'). % 3 connwriting(productunit, 'I', '{\\it I}'). % 4 connwriting(infix, 'in', '{\\downarrow}'). % 5+ connwriting(infixn, 'inn', '{\\stackrel{\\downarrow}{_{_-}}}'). % 5- connwriting(circumfix, 'ci', '{\\uparrow}'). % 6+ connwriting(circumfixn, 'cin', '{\\stackrel{\\uparrow}{_{_-}}}').% 6- connwriting(dprod, 'dp', '{\\odot}'). % 7+ connwriting(dprodn, 'dpn', '{\\stackrel{\\odot}{_{_-}}}'). % 7- connwriting(dproductunit, 'J', '{\\it J}'). % 8 connwriting(aconj, '&', '{\\&}'). % 9 connwriting(adisj, '+', '{\\oplus}'). % 10 connwriting(univq, '/\\', '{\\bigwedge}'). % 11 connwriting(exstq, '\\/', '{\\bigvee}'). % 12 connwriting(umod, 'L', '{\\Box}'). % 13 connwriting(emod, 'M', '{\\diamond}'). % 14 connwriting(abrack, '[]-1', '{[]^{-1}}'). % 15 connwriting(brack, '<>', '{\\langle\\rangle}'). % 16 connwriting(uexp, '!', '{!}'). % 17 connwriting(eexp, '?', '{?}'). % 18 connwriting(a, '|', '{|}'). % 20 connwriting(words, 'W', '{\\it W}'). % 20 connwriting(liunder, '-o', '{\\multimap}'). % 21 connwriting(liover, '*-', '{\\multimapdotinv}'). % 22 connwriting(liproduct, '.o', '{\\LEFTcircle}'). % 23 connwriting(riunder, '-*', '{\\multimapdot}'). % 24 connwriting(riover, 'o-', '{\\multimapinv}'). % 25 connwriting(riproduct, 'o.', '{\\RIGHTcircle}'). % 26 connwriting(uiinfix, 'uii', '{\\stackrel{%\\begin{picture}(7,8)(0,-2)\\put(0.7,7){\\rotatebox{-90}{$\\multimap$}}\\end{picture}}{_{}}}'). % 27+ connwriting(uiinfixn, 'uiin', '{\\stackrel{%\\begin{picture}(7,8)(0,-2)\\put(0.7,7){\\rotatebox{-90}{$\\multimap$}}\\end{picture}}{_{-}}}'). % 27- connwriting(uicircum, 'uic', '{\\stackrel{\\begin{picture}(7,7)(0,-2)\\put(1.5,-3){\\rotatebox{90}{$\\multimapdot$}}\\end{picture}}{_{}}}'). % 28+ connwriting(uicircumn, 'uicn', '{\\stackrel{\\begin{picture}(7,7)(0,-2)\\put(1.5,-3){\\rotatebox{90}{$\\multimapdot$}}\\end{picture}}{_{-}}}'). % 28- connwriting(uidprod, 'uidp', '{\\stackrel{\\begin{picture}(7,7)(0,0)\\put(0,5.5){\\rotatebox{-90}{$\\LEFTcircle$}}\\end{picture}}{_{}}}'). % 29+ connwriting(uidprodn, 'uidpn', '{\\stackrel{\\begin{picture}(7,7)(0,0)\\put(0,5.5){\\rotatebox{-90}{$\\LEFTcircle$}}\\end{picture}}{_{-}}}'). % 29- connwriting(liinfix, 'lii', '{\\stackrel{\\begin{picture}(7,8)(0,-2)\\put(0.7,7){\\rotatebox{-90}{$\\multimapdot$}}\\end{picture}}{_{}}}'). % 30+ connwriting(liinfixn, 'liin', '{\\stackrel{\\begin{picture}(7,8)(0,-2)\\put(0.7,7){\\rotatebox{-90}{$\\multimapdot$}}\\end{picture}}{_{-}}}'). % 30- connwriting(licircum, 'lic', '{\\stackrel{\\begin{picture}(7,7)(0,-2)\\put(1.5,-3){\\rotatebox{90}{$\\multimap$}}\\end{picture}}{_{}}}'). % 31+ connwriting(licircumn, 'licn', '{\\stackrel{\\begin{picture}(7,7)(0,-2)\\put(1.5,-3){\\rotatebox{90}{$\\multimap$}}\\end{picture}}{_{-}}}'). % 31- connwriting(lidprod, 'lidp', '{\\stackrel{\\begin{picture}(7,7)(0,0)\\put(0,5.5){\\rotatebox{-90}{$\\RIGHTcircle$}}\\end{picture}}{_{}}}'). % 32+ connwriting(lidprodn, 'lidpn', '{\\stackrel{\\begin{picture}(7,7)(0,0)\\put(0,5.5){\\rotatebox{-90}{$\\RIGHTcircle$}}\\end{picture}}{_{-}}}'). % 32- connwriting(iaconj, '|&|', '{\\sqcap}'). % 33 connwriting(iadisj, '|+|', '{\\sqcup}'). % 34 connwriting(iunivq, 'A', '{\\forall}'). % 35 connwriting(iexstq, 'E', '{\\exists}'). % 36 connwriting(iumod, iL, '{\\blacksquare}'). % 37 connwriting(iemod, iM, '{\\blacklozenge}'). % 38 connwriting(lproj, '<|-1', '{\\lhd^{-1}}'). % 39 connwriting(linj, '<|', '{\\lhd}'). % 40 connwriting(rproj, '|>-1', '{\\rhd^{-1}}'). % 41 connwriting(rinj, '|>', '{\\rhd}'). % 42 connwriting(split, 'v', '\\mbox{$\\check{\\ }$}'). % 43+ connwriting(splitn, '^-', '\\mbox{$\\check{_{_-}}$}'). % 43- connwriting(bridge, '^', '\\mbox{$\\hat{\\ }$}'). % 44+ connwriting(bridgen, '^-', '\\mbox{$\\hat{_{_-}}$}'). % 44- connwriting(ndiv, '-:-', '{\\div}'). % 45 connwriting(nprod, 'X', '{\\times}'). % 46 connwriting(ninfix, 'nin', '{\\Downarrow}'). % 47 connwriting(ncircumfix, 'nci', '{\\Uparrow}'). % 48 connwriting(ndprod, 'ndp', '\\mbox{\\footnotesize\\begin{picture}(0,0)\\put(2.2, 1){$\\circ$}\\put(0, 1){$\\bigcirc$}\\end{picture}\\ \\ \\ }'). % 49 connwriting(diff, '-', '{-}'). % 50 writeruleuser(Op) :- connwriting(Op, T, _), write(T). writerulelatex(S, Op) :- connwriting(Op, _, T), write(S, T). writerule(user, left(Op)) :- writeruleuser(Op), write(iL ). writerule(user, right(Op)) :- writeruleuser(Op), write('R'). writerule(user, perm(Op)) :- writeruleuser(Op), write('P'). writerule(user, contr(Op)) :- writeruleuser(Op), write('C'). writerule(user, expan(Op)) :- writeruleuser(Op), write('E'). writerule(latex(S), left(Op)) :- writerulelatex(S, Op), write(S, iL ). writerule(latex(S), right(Op)) :- writerulelatex(S, Op), write(S, 'R'). writerule(latex(S), perm(Op)) :- writerulelatex(S, Op), write(S, 'P'). writerule(latex(S), contr(Op)) :- writerulelatex(S, Op), write(S, 'C'). writerule(latex(S), expan(Op)) :- writerulelatex(S, Op), write(S, 'E'). writerule(user, id) :- write('id'). writerule(latex(Stream), id) :- write(Stream, '{\\it id}'). ?- write('This is CatLog3. Copyright 2018 (C) Glyn V. Morrill.'), nl, write('CatLog3 comes with ABSOLUTELY NO WARRENTY. This is free software.').