(* ::Package:: *)

BeginPackage["RhoLog`"];


Congruent::usage="\[Congruent] denotes syntactic identity: x \[Congruent] y holds iff x and y are the same.";
Rules::usage="Rules[l] returns the list of rules declared so far for strategy with name l.";
ApplyRule::usage="ApplyRule[stg,e] where stg is a strategy and e is a ground expression, computes an expression e' such that e \[Rule]_stg e' holds. If such an Expr' does not exist, it returns \"No solution found.\".";
ApplyRuleList::usage="ApplyRuleList[stg,e] where stg is a strategy and e is a ground expression, computes the list of all expressions e' such that e \[Rule]_stg e'.";
Request::usage="Request[{L1,...,Ln}] where L1,...,Ln are \[Rho]Log literals.\nThe call decides whether the query Exists[{R1,...,Rk},L1 \[And] ... \[And] Ln] has a solution, where R1, ..., Rk are the variables which occur in L1,\[Ellipsis],Ln. If the query has a solution {R1\[Rule]v1,...,Rk\[Rule]vk}, the call tries to compute an expression {\"R1\"\[Rule]\[LeftAngleBracket]v1\[RightAngleBracket],\[Ellipsis],\"Rk\"\[Rule]\[LeftAngleBracket]vk\[RightAngleBracket]}. The call returns \"No solution found.\" if it is unable to find a solution.\nOPTIONS:\n\n Depth \[Rule] nnn imposes the limit \!\(\*
StyleBox[\"nnn\",\nFontSlant->\"Italic\"]\) on the maximum number of transformation steps during the resolution of L1 \[And] ... \[And] Ln.\n\n \!\(\*
StyleBox[\"Trace\",\nFontColor->RGBColor[0, 0.25098, 0]]\) \[Rule] True|False enables/disables tracing. If the option Trace \[Rule] True is given, the call generates a notebook with a trace of the search for a solution.\n\n \!\(\*
StyleBox[\"ProofSimplify\",\nFontColor->RGBColor[0, 0.25098, 0]]\) \[Rule] True|False enables/disables the simplification of the proofs produced by tracing.\n~~~~~~~~~~\nREMARKS: A \[Rho]Log literal is either\n\t(1) a boolean expression, or\n\t(2) a matching formula s \[Congruent] t, or\n\t(3) a reducibility formula e1 \[Rule]_stg e2, or\n\t(4) a reducibility atom stg\[Because]e, or\n\t(5) an 
ucibility formula e1 \[RightArrowBar]_stg e2.";
RequestAll::usage="RequestAll[{L1,...,Ln}] where L1,...,Ln are \[Rho]Log literals.\nThe call attempts to compute the list {\[Tau]1,\[Tau]2,\[Ellipsis]} of all expressions \[Tau]i={\"R1\"\[Rule]\[LeftAngleBracket]v1\[RightAngleBracket],\[Ellipsis],\"Rk\"\[Rule]\[LeftAngleBracket]vk\[RightAngleBracket]} such that {R1\[Rule]v1,...,Rk\[Rule]vk} is a solution of the query Exists[{R1,\[Ellipsis],Rk},L1\[And]...\[And]Ln] where R1,...,Rk are the pattern names which occur in L1,...,Ln.\nOPTIONS:\n\n \!\(\*
StyleBox[\"Depth\",\nFontColor->RGBColor[0, 0.25098, 0]]\) \[Rule] \!\(\*
StyleBox[\"nnn\",\nFontSlant->\"Italic\"]\) imposes the limit nnn on the maximum number of transformation steps during the resolution of L1 \[And] ... \[And] Ln.\n\n \!\(\*
StyleBox[\"Trace\",\nFontColor->RGBColor[0, 0.25098, 0]]\) \[Rule] True|False enables/disables tracing. If the option Trace \[Rule] True is given, the call generates a notebook with a trace of the search for solutions.\n\n \!\(\*
StyleBox[\"MaxSols\",\nFontColor->RGBColor[0, 0.25098, 0]]\) \[Rule] \!\(\*
StyleBox[\"nnn\",\nFontSlant->\"Italic\"]\) imposes the limit \!\(\*
StyleBox[\"nnn\",\nFontSlant->\"Italic\"]\) on the maximum number of solutions which should be found for the query Exists[{R1,\[Ellipsis],Rk},Expr \[Rule]_l patt].\n\n \!\(\*
StyleBox[\"ProofSimplify\",\nFontColor->RGBColor[0, 0.25098, 0]]\) \[Rule] True|False enables/disables the simplification of the proofs produced by tracing.\n~~~~~~~~~~\nREMARKS: A \[Rho]Log literal is either\n\t(1) a boolean expression, or\n\t(2) a matching formula s \[Congruent] t, or\n\t(3) a reducibility formula e1 \[Rule]_stg e2, or\n\t(4) a reducibility atom stg\[Because]e, or\n\t(5) an irreducibility formula e1 \[RightArrowBar]_stg e2.";


DeclareRules::usage="DeclareRules[\[Rho]1,\[Ellipsis],\[Rho]n] declares the rules \[Rho]1,\[Ellipsis],\[Rho]n. It has the same effect as the sequence of commands DeclareRule[\[Rho]1]; \[Ellipsis]; DeclareRule[\[Rho]n];";
DeclareRule::usage="DeclareRule[\[Rho]] declares the rule \[Rho]. A rule is of the form l\!\(\*SubscriptBox[\(->\), \(stg\)]\)r or t\!\(\*SubscriptBox[\(->\), \(stg\)]\)r\[DoubleLongLeftArrow](\!\(\*SubscriptBox[\(cond\), \(1\)]\)&&\!\(\*SubscriptBox[\(\[Ellipsis]cond\), \(m\)]\)).";
ClearRules::usage="ClearRules[l1,...,ln] clears the rules with labels l1,\[Ellipsis],ln.";
Proportion::usage;


(* Usage of some options of some commands *)


MaxSols::usage="MaxSols is an option for RequestAll and ApplyRuleList. It controls the maximum number of solutions to be computed.";
ProofSimplify::usage="ProofSimplify is an option for RequestAll. The option ProofSimplify \[Rule] True enables rhe simplification of the proofs produced when tracing is enables with the option Trace \[Rule] True is given.";


Begin["`Private`"];


SetAttributes[{\[Bullet],\[Bullet]S,\[Bullet]P,Problem},HoldAll];


Problem/:MakeBoxes[Problem[{},Ls_],form_]:=MakeBoxes[Ls,form];
Problem/:MakeBoxes[Problem[{},Ls__],form_]:=MakeBoxes[And[Ls],form]
Problem/:MakeBoxes[Problem[{vs__},Ls_],form_]:=RowBox[{SubscriptBox["\[Exists]",MakeBoxes[{vs},form]],MakeBoxes[Ls,form]}];
Problem/:MakeBoxes[Problem[{vs__},Ls__],form_]:=RowBox[{SubscriptBox["\[Exists]",MakeBoxes[{vs},form]],MakeBoxes[And[Ls],form]}];


(* MAIN DATA STRUCTURES *)
Clear[Rules,MmaRules];
Rules[_]:={};
MmaRules[_]:={};


(* LOW-LEVEL PARSING *)


(* Variables Vi[x],Vc[x],Vs[x],Vf[x] *)
SetAttributes[{Vi,Vs,Vc,Vf},HoldAll];


MakeExpression[SuperscriptBox[x_,"i"],form_]:=MakeExpression[RowBox[{"RhoLog`Private`Vi","[",x,"]"}],form];
MakeExpression[SuperscriptBox[x_,"c"],form_]:=MakeExpression[RowBox[{"RhoLog`Private`Vc","[",x,"]"}],form];
MakeExpression[SuperscriptBox[x_,"s"],form_]:=MakeExpression[RowBox[{"RhoLog`Private`Vs","[",x,"]"}],form];
MakeExpression[SuperscriptBox[x_,"f"],form_]:=MakeExpression[RowBox[{"RhoLog`Private`Vf","[",x,"]"}],form];

Vi/:MakeBoxes[Vi[x_],form_]:=SuperscriptBox[MakeBoxes[x,form],"i"];
Vc/:MakeBoxes[Vc[x_],form_]:=SuperscriptBox[MakeBoxes[x,form],"c"];
Vs/:MakeBoxes[Vs[x_],form_]:=SuperscriptBox[MakeBoxes[x,form],"s"];
Vf/:MakeBoxes[Vf[x_],form_]:=SuperscriptBox[MakeBoxes[x,form],"f"];


Clear[RuleQ];
RuleQ[_RedFml|_RedAtom]:=True;
RuleQ[_]:=False;


(* Reducibility and irreducibility formulas *)
SetAttributes[{RedFml,IredFml,RedAtom},HoldRest];

MakeExpression[RowBox[{s_,SubscriptBox["->",stg_],t_}],form_]:=
  MakeExpression[RowBox[{"RhoLog`Private`RedFml","[",RowBox[{"{", 
  RowBox[{stg, ",", s}], "}"}],",",t,"]"}],form];

MakeExpression[RowBox[{s_,SubscriptBox["\[RightArrowBar]",stg_],t_}],form_]:=
  MakeExpression[RowBox[{"RhoLog`Private`IredFml","[",RowBox[{"{", 
  RowBox[{stg, ",", s}], "}"}],",",t,"]"}],form];
  
MakeExpression[RowBox[{stg_,"\[Proportion]",RowBox[{s_,"\[DoubleLongLeftArrow]",cond_}]}],form_]:=
  MakeExpression[RowBox[{"RhoLog`Private`RedAtom","[",RowBox[{"{", 
  RowBox[{stg, ",", s}], "}"}],",",cond,"]"}],form];  

MakeExpression[RowBox[{stg_,"\[Proportion]",s_}],form_]:=
  MakeExpression[RowBox[{"RhoLog`Private`RedAtom","[",RowBox[{"{", 
  RowBox[{stg, ",", s}], "}"}],"]"}],form];

RedFml/:MakeBoxes[RedFml[{stg_,s_},t_],form_]:=
  RowBox[{MakeBoxes[s,form],SubscriptBox["->",MakeBoxes[stg,form]],MakeBoxes[t,form]}];
  
IredFml/:MakeBoxes[IredFml[{stg_,s_},t_],form_]:=
  RowBox[{MakeBoxes[s,form],SubscriptBox["\[RightArrowBar]",MakeBoxes[stg,form]],MakeBoxes[t,form]}];

RedAtom/:MakeBoxes[RedAtom[{stg_,s_},cond_],form_]:=
  RowBox[{MakeBoxes[stg,form],"\[Proportion]",RowBox[{MakeBoxes[s,form],"\[DoubleLongLeftArrow]",MakeBoxes[cond,form]}]}];

RedAtom/:MakeBoxes[RedAtom[{stg_,s_}],form_]:=
  RowBox[{MakeBoxes[stg,form],"\[Proportion]",MakeBoxes[s,form]}];    


(* MISCELLANEOUS *)


Clear[VarSubst];
Off[RuleDelayed::rhs];
VarSubst[v:(Vi|Vf)[x_]]:=v->Pattern[x,Blank[]];
VarSubst[v:Vs[x_]]:=v->Pattern[x,BlankNullSequence[]];


(* bVars *)
Clear[bVars];
bVars[{vars___}]:=ReleaseHold[\[Bullet][vars]/.{Vi|Vf|Vs|Vc->Hold}]


(* Inadmissible[r] *)
Inadmissible/:MakeBoxes[Inadmissible[rule_],form_]:=
  RowBox[{"Rule ",MakeBoxes[rule,form]," is inadmissible."}];


(* Declarations of reduction rules *)
ClearAttributes[{ClearRules,DeclareRules,DeclareRule},{HoldAll,ReadProtected,Protected}];
SetAttributes[DoubleLongLeftArrow,HoldRest];


DeclareRules[rules___?RuleQ]:=Catch[Scan[DeclareRule,{rules}]];
DeclareRule[r:_[sl_,_]]:=declRule[RenameVars[bVars[getVars[sl]],"\[DoubleDot]",r]];
DeclareRule[RedAtom[sl_]]:=declRule[RenameVars[bVars[getVars[sl]],"\[DoubleDot]",RedAtom[sl,And[]]]];
ClearRules[ls__String]:=Scan[(Rules[#]=.;MmaRules[#]=.;)&,{ls}];


SetAttributes[{ClearRules,DeclareRules,DeclareRule},{HoldAll,ReadProtected,Protected}]


declRule[r:_[{s_,l_},_]]:=Module[{ok,rCond,V,rId},
   rCond=canonicForm[r];
   ok=admissibleQ[V=getVars[{s,l}],rCond];
   If[ok===False,Print[Inadmissible[r]];Throw["Stopped"]];
   rId=StrategyId[s];
   AppendTo[Rules[rId],r];
   If[FreeQ[l,Vc],
     AppendTo[MmaRules[rId],makeMmaRule[V,bVars[V],rCond]],
     V=Append[getVars[s],Vi[RhoLog`\[DoubleDot]x]];
     AppendTo[MmaRules[rId],makeMmaRule[V,bVars[V],ctxRule[Vi[RhoLog`\[DoubleDot]x],rCond]]]];
   rId];


(* admissibleQ[V0,_[L1,...,Ln]] checks if L1 && \[Ellipsis] && Ln is V0-admissible. 
   If yes, it returns the list of variables in the query, otherwise it returns False *)
Clear[admissibleQ];
admissibleQ[V0_,RedFml[_,DoubleLongLeftArrow[r_,\[Bullet][Ls___]]]] := admissibleQ[V0,\[Bullet][Ls,r]];
admissibleQ[V0_,RedAtom[_,\[Bullet][Ls___]]] := admissibleQ[V0,\[Bullet][Ls]];
admissibleQ[V0_,Q_] := Module[{V=V0},Catch[For[i=1,i<=Length[Q],i++,
  V=checkAndUpdate[#1,#2]&[Extract[Q,i,Hold],V]];V]];


(*Scan[(V=checkAndUpdate[#,V])&,Q];*)


canonicForm[RedFml[sl_,DoubleLongLeftArrow[r_,And[Ls___]]]]:=RedFml[sl,DoubleLongLeftArrow[r,\[Bullet][Ls]]];
canonicForm[RedFml[sl_,DoubleLongLeftArrow[r_,L_]]]:=RedFml[sl,DoubleLongLeftArrow[r,\[Bullet][L]]];
canonicForm[RedFml[sl_,r_]]:=RedFml[sl,DoubleLongLeftArrow[r,\[Bullet][]]];

canonicForm[RedAtom[sl_,And[Ls___]]]:=RedAtom[sl,\[Bullet][Ls]];
canonicForm[RedAtom[sl_,L_]]:=RedAtom[sl,\[Bullet][L]];
canonicForm[RedAtom[sl_]]:=RedAtom[sl,\[Bullet][]];


ctxRule[newl_,RedFml[{s_,l_},DoubleLongLeftArrow[r_,_[Ls___]]]] := 
   RedFml[{s,newl},DoubleLongLeftArrow[r,And[newl\[Congruent]l,Ls]]];
ctxRule[newl_,RedAtom[{s_,l_},_[Ls___]]] := RedAtom[{s,newl},And[newl\[Congruent]l,Ls]];   


(* UTILITY FUNCTIONS *)


Clear[StrategyId];
StrategyId[l_String|l_String[___]]:=l;


SetAttributes[getVars,HoldAll];
getVars[expr_] := Union[Cases[Unevaluated[expr],Vi[_Symbol]|Vf[_Symbol]|Vc[_Symbol]|Vs[_Symbol],{0,\[Infinity]},Heads->True]];


MmaPattern[V_][sl_] := ReplaceAll[ReplaceAll[sl,{Vi[_Blank]|Vf[_Blank]->_,Vs[_Blank]->___}],Map[VarSubst,V]];


(* RenameVars[\[Bullet][v1,..,,vn],sfx,form] replaces symbols v1,...,vn in form 
  with w1,...,wn, where every wi is obtained by adding suffix sfx to vi *)
RenameVars[_[vars___],sfx_String,form_]:=Module[{vsNames,newVs},
   Block[{vars},
     vsNames = ("RhoLog`"<>ToString[#] <> sfx)& /@ {vars};
     newVs = Symbol /@ vsNames;
     form/.Inner[Rule,{vars},newVs,List]]];


(* AddRenaming *)
AddRenaming[lbl_,subst_,_[vars___], RedFml[patt_,DoubleLongLeftArrow[r_,_[Ls___]]]] :=
    patt:>Module[{vars},True/;(TellStart[\[Bullet]["\[Rho]", lbl, subst, \[Bullet][Ls,r\[Congruent]#1,##2]]];Interpret[Ls,r\[Congruent]#1,##2])];
AddRenaming[lbl_,subst_,_[vars___], RedAtom[patt_,_[Ls___]]] :=
    patt:>Module[{vars},True/;(TellStart[\[Bullet]["\[Rho]", lbl, subst, \[Bullet][Ls,##]]];Interpret[Ls,##])];


makeMmaRule[V_,_[vars___],rule_]:=Block[{vars},
  Module[{newRule,\[Mu],lbl},
    lbl=StrategyId[rule[[1,1]]];
    newRule=MapAt[MmaPattern[V],rule,1]/.Map[Rule[#,First[#]]&,V];
    AddRenaming[lbl[Length[Rules[lbl]]],Map[Rule[ToString[#],AngleBracket[#]]&,{vars}],bVars[getVars@@{newRule}],newRule]]];


(* makeMatchingRule *) (* TellMatcher["match",#2] *)
Clear[makeMatchingRule];
SetAttributes[makeMatchingRule,HoldRest];
makeMatchingRule[t_,Ls___]:=Module[{V=getVars[t],\[Mu],patt,subst},
   \[Mu]=Map[Rule[ToString[#],AngleBracket[#]]&,Map[First,V]];
   patt=MmaPattern[V][t];
   subst = Map[(#->First[#])&,V];
   ((#1:>True/;(TellStart[\[Bullet]["\[Mu]", #2, #3, \[Bullet][Ls]]];IAux[Ls]))&[patt,ToString[patt],\[Mu]])/.subst];


(* checkAndUpdate *)
Clear[checkAndUpdate];
SetAttributes[checkAndUpdate,{HoldFirst}];
checkAndUpdate[_[fml:(RedFml|Congruent)[sl_,r_]],V_] :=
 Module[{vs1=getVars[Unevaluated[sl]],vs2=getVars[Unevaluated[r]]},
  If[Complement[vs1,V]=!={},Throw[False]];
  Union[V,vs2]];
checkAndUpdate[_[e:(sl_\[TildeTilde]v_Vc)],V_] := 
  If[Complement[getVars[Unevaluated[sl]],V]=!={},Throw[False],Union[{v},V]];
checkAndUpdate[_[fml:(IredFml[sl_,_]|sl_)],V_] := 
   If[Complement[getVars[Unevaluated[sl]],V]=!={},Throw[False],V];


(* makeRuleCode *)
SetAttributes[{makeRuleCode}, HoldRest]; 
makeRuleCode[code_, r_, Ls___] := code&[Unevaluated[r], Unevaluated[Ls]];     


(* MISCELLANEOUS *)


(* Request and RequestAll *)


SetAttributes[{Request,RequestAll}, {HoldAll}]; 
Options[Request] = Options[RequestAll] = {Trace -> False, Depth -> 10000, MaxSols -> \[Infinity], ProofSimplify -> True}; 


Request[(List|And)[Ls___], opts___?OptionQ]:=Block[{},
   Qaux[RenameVars[bVars[getVars[\[Bullet][Ls]]],"\[ReverseDoublePrime]",\[Bullet][Ls]],True,opts]];
Request[L_,opts___?OptionQ]:=Request[{L},opts];
RequestAll[(List|And)[Ls___], opts___?OptionQ]:=Block[{},
   Qaux[RenameVars[bVars[getVars[\[Bullet][Ls]]],"\[ReverseDoublePrime]",\[Bullet][Ls]],False,opts]];
RequestAll[L_,opts___?OptionQ]:=RequestAll[{L},opts];


(* ApplyRule*)
Clear[ApplyRule];
SetAttributes[{ApplyRule,ApplyRuleList}, HoldAll]; 

ApplyRule[l_, expr_, opts___] := Module[{res},
   res=Request[RedFml[{l,expr},Vi[RhoLog`x]],opts];
   If[StringQ[res], expr, res[[1, 2]]]]; 
   
ApplyRuleList[l_, expr_, opts___] := Module[{},
   Map[Function[#[[1,2]]],RequestAll[RedFml[{l,expr},Vi[RhoLog`x]],opts]]]


(* Qaux *)
Qaux[Q_,one_,opts___] := Module[{okV,subst,tmpList},
   okV = admissibleQ[{},Q];
   If[okV===False, Print["The query is inadmissible."]; Return[]];
   tmpList = Map[If[Head[#]===Vc,#["\[SmallCircle]"],If[Head[#]===Vs,AngleBracket[#],#]]&,okV]; 
   subst=Map[Rule[StringDrop[ToString[#[[1]]],-1],#[[2]]]&, Transpose[{Map[First,okV],tmpList}]];
   Block[{$Depth, $MaxSols, $Solutions = {}, $Proof, $CutPosns, $Strip, 
             $RecursionLimit, $IterationLimit, $QueryStop = one, TRACE, TOUCH, CRT},
    $RecursionLimit = $IterationLimit = \[Infinity];
    TOUCH[_] := False; 
    CRT = 0;
    {$Proof, $CutPosns} = {$NODE[Append[Q, tmpList]], {1}};
    Set[{TRACE, $Depth, $MaxSols, $Strip}, {Trace, Depth, MaxSols,
                 ProofSimplify} /. Join[{opts}, Options[Request]]];
    ask = Catch[Interpret @@ {Q,subst}];
    If[TRACE,  
       $Proof = $Proof/.Sequence->Hold//ReleaseHold; (* Mma trick *)
       DisplayProof[]];
    If[one, If[ask, First[$Solutions], "No solution found."], $Solutions]]];


(* Interpret *)
SetAttributes[Interpret, HoldRest]; 
Interpret[\[Bullet][Ls___], subst_] := Interpret[Ls, subst];
Interpret[\[Bullet][Ls___]] := Interpret[Ls];
Interpret[Ls___] := If[And[$Depth>0,$MaxSols>0],
  IAux[Ls],
  If[TRACE,
     Tell[PP[Ls]];TellEnd[],
     False]]; 


Clear[Congruent];
Congruent[t_,t_];


Clear[ResumeIAux];
ResumeIAux[\[Bullet][Ls___]] := IAux[Ls];


(* IAux *)
SetAttributes[IAux,HoldRest];
IAux[]:=Throw[True];


IAux[soln_List] :=Block[{},
   AppendTo[$Solutions, soln];
   If[TRACE,
        Tell[SS[soln]];
        $MaxSols--;
        If[$QueryStop,
            ResumeProof[]; Throw[True],
            TellEnd[]],
        $MaxSols--;
        If[$QueryStop,Throw[True], False]
    ]];


IAux[True,Ls___] := IAux[Ls];
IAux[False,___] := If[TRACE, Tell[\[Bullet]["F"]]; TellEnd[], False];


(* Created by "Comp" *)
IAux[gt_ \[Congruent] "\[Bullet]", RedFml[{stg_, "\[Bullet]"}, t_], Ls___] :=
    IAux[RedFml[{stg, gt}, t], Ls]; 

IAux[gt_ \[Congruent] "\[Bullet]", "!"[d_], Ls___] := 
    ($Depth = d; Throw[\[Bullet][gt \[Congruent] "\[Bullet]", Ls]]); 
     
(* Created by "Comp" and "Fst" *)
IAux[gt_ \[Congruent] "\[Bullet]", \[WatchIcon][n_], Ls___] := (TOUCH[n] = True; IAux[gt \[Congruent] "\[Bullet]", Ls]);

(* Created by "NF" *)
IAux[gt_ \[Congruent] "\[Bullet]"[n_], Ls___] := (TOUCH[n] = True; IAux[gt \[Congruent] "\[Bullet]", Ls]);

(* Created by "Fst" *)
IAux[\[WatchIcon][n_], Ls___] := (TOUCH[n] = True; IAux[Ls]);

(* Created by "Cut" *)
IAux["!"[d_],Ls___] := ($Depth = d;Throw[\[Bullet][Ls]]);


(* Handling of context variables *)
IAux[gt_\[TildeTilde]xc_Vc,Ls___]:=Interpret[ReplaceAll[\[Bullet][Ls],{xc[s\[DoubleDot]_]:>#}]&[gt/."\[SmallCircle]"->s\[DoubleDot]]];
IAux[gt_\[Congruent]Vc[_Blank][t_],Ls___]:=Block[{},
  Replace[gt,{
    _:>True/;(TellStart[\[Bullet]["\[Mu]","\!\(\*SuperscriptBox[\(_\), \(c\)]\)",{"\!\(\*SuperscriptBox[\(_\), \(c\)]\)"->"\[SmallCircle]"},\[Bullet][gt\[Congruent]t,Ls]]];IAux[gt\[Congruent]t,Ls]),
    _[___,x_,___]:>True/;(TellStart[\[Bullet]["\[Mu]","\!\(\*SuperscriptBox[\(_\), \(c\)]\)",{"\!\(\*SuperscriptBox[\(_\), \(c\)]\)"->"\!\(\*SuperscriptBox[\(_\), \(f\)]\)[\!\(\*SuperscriptBox[\(_\), \(s\)]\),\[SmallCircle],\!\(\*SuperscriptBox[\(_\), \(s\)]\)]"},\[Bullet][x\[Congruent]t,Ls]]];IAux[x\[Congruent]t,Ls])}];
  TellEnd[]];


(* Matching with ctx. vars *)
IAux[gt_\[Congruent](xc:_Vc)[t_],Ls___] := Module[{RhoLog`z\[DoubleDot]},
  Replace[gt,{
    _:>True/;(
       TellStart[\[Bullet]["\[Mu]",xc,{xc->"\[SmallCircle]"},\[Bullet]["\[SmallCircle]"\[TildeTilde]xc,gt\[Congruent]t,Ls]]];
       IAux["\[SmallCircle]"\[TildeTilde]xc,gt\[Congruent]t,Ls]),
    f\[DoubleDot]_[s1\[DoubleDot]___,x\[DoubleDot]_,s2\[DoubleDot]___]:>True/;(
       TellStart[
        \[Bullet]["\[Mu]",xc,{xc->f\[DoubleDot][s1\[DoubleDot],Vc[RhoLog`z\[DoubleDot]]["\[SmallCircle]"],s2\[DoubleDot]]}, 
           \[Bullet][x\[DoubleDot]\[Congruent]Vc[RhoLog`z\[DoubleDot]][t],f\[DoubleDot][s1\[DoubleDot],Vc[RhoLog`z\[DoubleDot]]["\[SmallCircle]"],s2\[DoubleDot]]\[TildeTilde]xc,Ls]]];
       IAux[x\[DoubleDot]\[Congruent]Vc[RhoLog`z\[DoubleDot]][t],f\[DoubleDot][s1\[DoubleDot],Vc[RhoLog`z\[DoubleDot]]["\[SmallCircle]"],s2\[DoubleDot]]\[TildeTilde]xc,Ls])}];
  TellEnd[]];


IAux[gt_\[Congruent]t_/;Not[FreeQ[t,Vc]],Ls___] := With[{xi = Module[{RhoLog`x}, Vi[RhoLog`x]], p = Last[Position[t, _Vc[_]]]},
        IAux[gt \[Congruent] #1, xi \[Congruent] #2, Ls]&[ReplacePart[t, p -> xi], Part[t, Sequence @@ p]]];


IAux[gt_\[Congruent]t_,Ls___] := Module[{V=getVars[t],\[Mu],patt},
   \[Mu]=Map[Rule[ToString[#],AngleBracket[#]]&,Map[First,V]];
   patt=MmaPattern[V][t];
   Replace[gt, makeMatchingRule[t,Ls]];
   TellEnd[]];


IAux[RedFml[{"Cut"[stg_],gt_},t_],Ls___] := Function[If[# === False,False,ResumeIAux[#]]][Catch[IAux[RedFml[{stg,gt},t],"!"[#], Ls]&[$Depth]]];
IAux[RedAtom[{"Cut"[stg_],gt_}],Ls___] := Function[If[# === False,False,ResumeIAux[#]]][Catch[IAux[RedAtom[{stg,gt}],"!"[#], Ls]&[$Depth]]]


IAux[RedFml[{"Fst"[stg1_, stg2_], gt_}, t_], Ls___] :=
  Apply[Function[
      If[TOUCH[#1],
         #2,
         If[TRACE,TellStart[\[Bullet]["?", IredFml[{stg1, gt}, t], \[Bullet][RedFml[{stg2, gt}, t], Ls]]]];
         IAux[RedFml[{stg2, gt}, t], Ls]]],
     {#,IAux[RedFml[{stg1, gt}, t], \[WatchIcon][#], Ls]}&[CRT++]];
     
IAux[RedFml[{"Fst"[stg_, stgs__], gt_}, t_], Ls___] :=
  Apply[Function[
      If[TOUCH[#1],
         #2,
         If[TRACE,TellStart[\[Bullet]["?", IredFml[{stg, gt}, t], \[Bullet][RedFml[{"Fst"[stgs], gt}, t], Ls]]]];
         IAux[RedFml[{"Fst"[stgs], gt}, t], Ls]]],
     {#,IAux[RedFml[{stg, gt}, t], \[WatchIcon][#], Ls]}&[CRT++]];   


IAux[RedFml[{"Comp"[s1_,s2_], gt_}, t_], Ls___] := Block[{},
   TellStart[\[Bullet]["\[Rho]","Comp",{},\[Bullet][RedFml[{s1, gt},"\[Bullet]"], RedFml[{s2, "\[Bullet]"}, t], Ls]]];
   IAux[RedFml[{s1, gt},"\[Bullet]"], RedFml[{s2, "\[Bullet]"}, t], Ls];TellEnd[]];   
   
IAux[RedFml[{"Comp"[s1_,ss2__], gt_}, t_], Ls___] := Block[{},
   TellStart[\[Bullet]["\[Rho]","Comp",{},\[Bullet][RedFml[{s1, gt},"\[Bullet]"], RedFml[{"Comp"[ss2], "\[Bullet]"}, t], Ls]]];
   IAux[RedFml[{s1, gt},"\[Bullet]"], RedFml[{"Comp"[ss2], "\[Bullet]"}, t], Ls];TellEnd[]];


IAux[RedFml[{stg:("Or"[___]), gt_}, t_], Ls___] := Block[{},
  Scan[(TellStart[\[Bullet]["|", #]]; IAux[RedFml[{#, gt}, t], Ls])&, stg];
  TellEnd[]];

IAux[RedAtom[{stg:("Or"[___]), gt_}], Ls___] := Block[{},
  Scan[(TellStart[\[Bullet]["|", #]]; IAux[RedAtom[{#, gt}], Ls])&, stg];
  TellEnd[]];


IAux[RedFml[{"NF"[stg_], gt_}, t_], Ls___] :=
    Apply[Function[
      If[TOUCH[#1],
         #2,
         If[TRACE, TellStart[\[Bullet]["?", IredFml[{stg, gt}, "_"],\[Bullet][gt \[Congruent] t, Ls]]]];
         IAux[gt \[Congruent] t, Ls]]],
      {#, IAux[RedFml[{stg,gt},"\[Bullet]"[#]],RedFml[{"NF"[stg],"\[Bullet]"},t],Ls]}&[CRT++]];


IAux[RedFml[sl:{stg_, gt_}, t_], Ls___] :=
   Block[{},
     If[And[$Depth > 0,$MaxSols > 0],
       $Depth--;
       Replace[sl,makeRuleCode[MmaRules[StrategyId[stg]],t,Ls]];
       $Depth++;
       TellEnd[]]];
       
IAux[RedAtom[sl:{stg_, gt_}], Ls___] :=
   Block[{},
     If[And[$Depth > 0,$MaxSols > 0],
       $Depth--;
       Replace[sl,makeRuleCode[MmaRules[StrategyId[stg]],Ls]];
       $Depth++;
       TellEnd[]]]       


IAux[IredFml[sl_, t_], Ls___] :=
    If[Block[{$Depth, $MaxSols, TRACE, $QueryStop},
            {$Depth, $MaxSols, TRACE, $QueryStop} = {\[Infinity], 1, False, True};
            Catch[IAux[RedFml[sl, t]]]] === True,
        If[Trace, Tell[\[Bullet]["?", RedFml[sl,t], \[Bullet][False]]]];
        TellEnd[],
        If[Trace, Tell[\[Bullet]["?", IredFml[sl, t], \[Bullet][Ls]]]];
        IAux[Ls]
    ];
IAux[Ls__]:=(Print[{"Wrong syntax:",Ls}];Abort[]); 


(* MakeMyBoxes *)
MakeMyBoxes[_[_, _, _, _[as___,_]]] := MakeBoxes[\[Bullet][as]];
MkMyB[_[as___,_]]:=MakeBoxes[\[Bullet][as]];


\[Bullet]/:MakeBoxes[\[Bullet][],form_] := MakeBoxes["\[Square]",form];
\[Bullet]/:MakeBoxes[\[Bullet][L_],form_] := MakeBoxes[L,form];
\[Bullet]/:MakeBoxes[\[Bullet][Ls___],form_] := MakeBoxes[And[Ls],form];


\[WatchIcon]/:MakeBoxes[\[WatchIcon][_],form_] := MakeBoxes["",form];


(* MAIN COMMANDS *)


(* ResumeIAux *)
ResumeIAux[r:\[Bullet][Ls___]] := IAux[Ls]; 


(* RedQ *)
RedQ[_[as__], t_, f_] :=
    Block[{$Depth, $MaxSols, TRACE = False},
        $Depth = $MaxSols = \[Infinity];
        Catch[Interpret[RhoRF[as]]; False]]; 


(* TRACING: Tell, TellStart, TellEnd *)


Tell[info_] := AppendTo[$Proof, info]; 

TellStart[info_] :=
    If[TRACE,
        PrependTo[$CutPosns, Length[$Proof]];
        AppendTo[$Proof, info]]; 

TellEnd[] := Block[{},
  If[TRACE,
     With[{p = First[$CutPosns]},
          $CutPosns = Rest[$CutPosns];
          $Proof = Append[Take[$Proof, p], Drop[$Proof, p]]]];
  False];


(* PROOF PRESENTATION *)


(* $FNODE *)
$FNODE[as___,n:(SS[___]|$SNODE[___]),bs___]:=$SNODE[as,n,bs];
$FNODE[as___,n:(PP[___]|$PNODE[___]),bs___]:=$PNODE[as,n,bs];


(* $EFNODE *)
$EFNODE[as___,n:(SS[___]|$SNODE[___]),bs___]:=DeleteCases[$SNODE[as,n,bs],_$FNODE|_$PNODE|PP[___]];
$EFNODE[as___,n:(PP[___]|$PNODE[___]),bs___]:=DeleteCases[$PNODE[as,n,bs],_$FNODE];
$EFNODE[as___]:=$FNODE[as];


(* GetExplanations *)
GetExplanations[PP[___]]:=
  {Cell[TextData[StyleBox["Pending proof \[Ellipsis]",FontSlant->"Italic",FontColor->GrayLevel[.6]]],"Text"]};
GetExplanations[SS[soln_]]:=
  {Cell[TextData[StyleBox["Thus, we have found the solution"]],"Text",ShowCellBracket->False],
   Cell[BoxData[RowBox[{ToBoxes[soln]}]],"Program",CellFrame->True,Background->GrayLevel[.8]]};
GetExplanations[Nd:n_[x:\[Bullet][type_,ts___],as___]]:=Module[{cls},
 Switch[type,
  "F",{Cell[TextData[{"This problem has no solutions."}],"Text",ShowCellBracket->False]},
  "?",
       Join[{Cell[TextData[{"Since"}],"Text"],
             Cell[BoxData[RowBox[{ToBoxes[x[[2]]]}]],"Program",TextAlignment->Center,ShowCellBracket->False],
             Cell[TextData[{"the problem reduces to"}],"Text",ShowCellBracket->False],
             Cell[BoxData[RowBox[{MkMyB[x[[3]]]}]],"Program",ShowCellBracket->False]
             (* Cell[BoxData[RowBox[{ToBoxes[x[[3]]]}]],"Program",TextAlignment->Center,ShowCellBracket->False] *)},
            GetExplanations[n[as]]],
  "|",If[Length[{as}]==0,
         {Cell[TextData[{"Alternative case ",Cell[BoxData[FormBox[StyleBox[ToBoxes[ts],FontColor->RGBColor[0,0,1]],TraditionalForm]]]," fails."}],ShowCellBracket->False]},
         {Cell[CellGroupData[Prepend[GetExplanations[n[as]],Cell[TextData[{"Alternative case ",Cell[BoxData[FormBox[StyleBox[ToBoxes[ts],FontColor->RGBColor[0,0,1]],TraditionalForm]]]}]]],Closed]]}],
  "\[Mu]",Join[{Cell[TextData[{"Matching against ",Cell[BoxData[FormBox[StyleBox[ToBoxes[x[[2]]]],Text]]]," with matcher ",
                           Cell[BoxData[FormBox[StyleBox[ToBoxes[x[[3]]],FontColor->RGBColor[.5,0,0]],TraditionalForm]]],
                           " yields the goal"}]],
            Cell[BoxData[RowBox[{MakeMyBoxes[x]}]],"Program",ShowCellBracket->False]},
           GetExplanations[n[as]]],
  "\[Rho]",Join[{Cell[TextData[{"The application of rule ",Cell[BoxData[FormBox[StyleBox[ToBoxes[x[[2]]],FontColor->RGBColor[0,0,1]],TraditionalForm]]]," with matcher ",
                            Cell[BoxData[FormBox[StyleBox[ToBoxes[x[[3]]],FontColor->RGBColor[.5,0,0]],TraditionalForm]]],
                            " yields the goal"}]],
            Cell[BoxData[RowBox[{MakeMyBoxes[x]}]],"Program",ShowCellBracket->False]},
           GetExplanations[n[as]]],
  _,{}]];


GetExplanations[_[Nd:($SNODE[___]|$FNODE[___]|$PNODE[___]|PP[___]|SS[___]),as___]]:=Module[{cls},
 If[Length[cls=Map[GetExplanations,{Nd,as}]]>1,
   cls=Map[Cell[CellGroupData[#,Closed]]&,cls];
   {Cell[CellGroupData[Prepend[cls,Cell[TextData[{"There are ",StyleBox["more alternatives",FontSlant->"Italic"]," to continue."}],"Text"]],Closed]]},
   Flatten[cls,1]]];
GetExplanations[x_]:={};


(* DisplayProof *)
DisplayProof[]:=Block[{$NODE=If[$Strip,$EFNODE,$FNODE]},
  If[MatchQ[$Proof,on_[on_[___]]],$Proof=First[$Proof]];
  NotebookPut[Notebook[
     Append[TellProblem[First[$Proof]],
       Cell[CellGroupData[Join[
        {Cell[TextData[StyleBox["Justification"]],"Subsubsection",
           CellDingbat->None,
           ShowCellBracket->False]},
        GetExplanations[Rest[$Proof]],
        {Cell[TextData["\[EmptySquare]"],
           TextAlignment->Right,
           CellMargins->{{Inherited,Inherited},{Inherited,0}},
           ShowCellBracket->False]}]]]],
     CellGrouping->"Manual",
     StyleDefinitions->"ArticleClassic.nb",
     Evaluator-> "None",
     Deletable->False,
     Editable->False]]];


(* TellProblem *)
TellProblem[p:_[Ls___, vs_]] :=
    Module[{c1},
        c1 = {Cell[TextData[StyleBox["Decide"]], "Subsubsection", CellDingbat
             -> None, ShowCellBracket -> False], Cell[TextData[StyleBox["the satisfiability of"
            ]], "Text", ShowCellBracket -> False], Cell[BoxData[FormBox[StyleBox[
            ToBoxes[Problem[vs, Ls]]], TraditionalForm]], CellFrame -> True, Background
             -> GrayLevel[0.8], ShowCellBracket -> False], Cell[TextData[StyleBox[
            "Answer"]], "Subsubsection", CellDingbat -> None, ShowCellBracket -> False]};
        Switch[Head[$Proof],
            $FNODE | $EFNODE,
                AppendTo[c1, Cell["The formula is unsatisfiable.", "Text", ShowCellBracket -> False]],
            $SNODE,
                If[First[$Solutions] == {},
                    AppendTo[c1, Cell["The formula holds.", "Text", ShowCellBracket -> False]],
                    c1 = Join[c1, {Cell["The formula holds for ", "Text",
                         ShowCellBracket -> False]}, Cell[BoxData[RowBox[{ToBoxes[#]}]], "Program",
                         CellFrame -> True, Background -> GrayLevel[0.8], ShowCellBracket -> False]& /@ $Solutions]
                ],
            $PNODE,
                AppendTo[c1, Cell["Could not decide.", "Text", ShowCellBracket -> False]]
        ];
        AppendTo[c1, Cell["", "Text", CellFrame -> {{0, 0}, {0.25, 0}}, 
            ShowCellBracket -> False, CellMargins -> {{10, 10}, {Inherited, Inherited}}, 
            CellElementSpacings -> {"CellMinHeight" -> 5}, CellSize -> {Inherited, 5}]]
    ]; 


(* ResumeProof *)
ResumeProof[] := Module[{i},For[i=1,i<=Length[$CutPosns],i++,TellEnd[]]];


End[];


(* Some predefined strategies *)
DeclareRules[
\!\(
\*SuperscriptBox[\(x\), \(i\)]
\*SubscriptBox[\(->\), \("\<Id\>"\)]
\*SuperscriptBox[\(x\), \(i\)]\),
\!\(\({
\*SuperscriptBox[\(_\), \(s\)], 
\*SuperscriptBox[\(x\), \(i\)], 
\*SuperscriptBox[\(_\), \(s\)]}\)
\*SubscriptBox[\(->\), \("\<Elem\>"\)]
\*SuperscriptBox[\(x\), \(i\)]\),
\!\(
\*SuperscriptBox[\(x\), \(i\)]
\*SubscriptBox[\(->\), \("\<Repeat\>"[
\*SuperscriptBox[\(_\), \(i\)]]\)]
\*SuperscriptBox[\(x\), \(i\)]\),
\!\(
\*SuperscriptBox[\(x\), \(i\)]
\*SubscriptBox[\(->\), \("\<Repeat\>"[
\*SuperscriptBox[\(s\), \(i\)]]\)]\(
\*SuperscriptBox[\(y\), \(i\)]\[DoubleLongLeftArrow]\((
\*SuperscriptBox[\(x\), \(i\)]
\*SubscriptBox[\(->\), \("\<Comp\>"[
\*SuperscriptBox[\(s\), \(i\)], "\<Repeat\>"[
\*SuperscriptBox[\(s\), \(i\)]]]\)]
\*SuperscriptBox[\(y\), \(i\)])\)\)\),
\!\(
\*SuperscriptBox[\(x\), \(i\)]
\*SubscriptBox[\(->\), \("\<Repeat\>"[
\*SuperscriptBox[\(_\), \(i\)], 0]\)]
\*SuperscriptBox[\(x\), \(i\)]\),
\!\(
\*SuperscriptBox[\(x\), \(i\)]
\*SubscriptBox[\(->\), \("\<Repeat\>"[
\*SuperscriptBox[\(s\), \(i\)], 
\*SuperscriptBox[\(n\), \(i\)] /; IntegerQ[n] && \((n > 0)\)]\)]\(
\*SuperscriptBox[\(y\), \(i\)]\[DoubleLongLeftArrow]\((
\*SuperscriptBox[\(x\), \(i\)]
\*SubscriptBox[\(->\), \("\<Comp\>"[
\*SuperscriptBox[\(s\), \(i\)], "\<Repeat\>"[
\*SuperscriptBox[\(s\), \(i\)], 
\*SuperscriptBox[\(n\), \(i\)] - 1]]\)]
\*SuperscriptBox[\(y\), \(i\)])\)\)\),
\!\(\(
\(\*SuperscriptBox[\(c\), \(c\)]\)[
\*SuperscriptBox[\(x\), \(i\)]]\)
\*SubscriptBox[\(->\), \("\<Rw\>"[
\*SuperscriptBox[\(s\), \(i\)]]\)]\(
\(\*SuperscriptBox[\(c\), \(c\)]\)[
\*SuperscriptBox[\(y\), \(i\)]]\[DoubleLongLeftArrow]\((
\*SuperscriptBox[\(x\), \(i\)]
\*SubscriptBox[\(->\), 
SuperscriptBox[\(s\), \(i\)]]
\*SuperscriptBox[\(y\), \(i\)])\)\)\),
\!\(
\*SuperscriptBox[\(x\), \(i\)]
\*SubscriptBox[\(->\), \("\<Irr\>"[
\*SuperscriptBox[\(s\), \(i\)]]\)]\(
\*SuperscriptBox[\(x\), \(i\)]\[DoubleLongLeftArrow]\((
\*SuperscriptBox[\(x\), \(i\)]
\*SubscriptBox[\(\[RightArrowBar]\), 
SuperscriptBox[\(s\), \(i\)]]
\*SuperscriptBox[\(_\), \(i\)])\)\)\),
\!\(\(
\(\*SuperscriptBox[\(f\), \(f\)]\)[
\*SuperscriptBox[\(xs\), \(s\)], 
\*SuperscriptBox[\(x\), \(i\)], 
\*SuperscriptBox[\(ys\), \(s\)]]\)
\*SubscriptBox[\(->\), \("\<Rw1\>"[
\*SuperscriptBox[\(s\), \(i\)]]\)]\(
\(\*SuperscriptBox[\(f\), \(f\)]\)[
\*SuperscriptBox[\(xs\), \(s\)], 
\*SuperscriptBox[\(y\), \(i\)], 
\*SuperscriptBox[\(ys\), \(s\)]]\[DoubleLongLeftArrow]\((
\*SuperscriptBox[\(x\), \(i\)]
\*SubscriptBox[\(->\), 
SuperscriptBox[\(s\), \(i\)]]
\*SuperscriptBox[\(y\), \(i\)])\)\)\),
\!\(
\*SuperscriptBox[\(x\), \(i\)]
\*SubscriptBox[\(->\), \("\<Outer\>"[
\*SuperscriptBox[\(s\), \(i\)]]\)]\(
\*SuperscriptBox[\(y\), \(i\)]\[DoubleLongLeftArrow]\((
\*SuperscriptBox[\(x\), \(i\)]
\*SubscriptBox[\(->\), \("\<Fst\>"[
\*SuperscriptBox[\(s\), \(i\)], "\<Rw1\>"["\<Outer\>"[
\*SuperscriptBox[\(s\), \(i\)]]]]\)]
\*SuperscriptBox[\(y\), \(i\)])\)\)\),
\!\(
\*SuperscriptBox[\(x\), \(i\)]
\*SubscriptBox[\(->\), \("\<Inner\>"[
\*SuperscriptBox[\(s\), \(i\)]]\)]\(
\*SuperscriptBox[\(y\), \(i\)]\[DoubleLongLeftArrow]\((
\*SuperscriptBox[\(x\), \(i\)]
\*SubscriptBox[\(->\), \("\<Fst\>"["\<Rw1\>"["\<Inner\>"[
\*SuperscriptBox[\(s\), \(i\)]]], 
\*SuperscriptBox[\(s\), \(i\)]]\)]
\*SuperscriptBox[\(y\), \(i\)])\)\)\),
\!\(
\*SuperscriptBox[\(x\), \(i\)]
\*SubscriptBox[\(->\), \("\<LazyEval\>"[
\*SuperscriptBox[\(s\), \(i\)]]\)]\(
\*SuperscriptBox[\(y\), \(i\)]\[DoubleLongLeftArrow]\((
\*SuperscriptBox[\(x\), \(i\)]
\*SubscriptBox[\(->\), \("\<NF\>"["\<Outer\>"[
\*SuperscriptBox[\(s\), \(i\)]]]\)]
\*SuperscriptBox[\(y\), \(i\)])\)\)\),
\!\(
\*SuperscriptBox[\(x\), \(i\)]
\*SubscriptBox[\(->\), \("\<StrictEval\>"[
\*SuperscriptBox[\(s\), \(i\)]]\)]\(
\*SuperscriptBox[\(y\), \(i\)]\[DoubleLongLeftArrow]\((
\*SuperscriptBox[\(x\), \(i\)]
\*SubscriptBox[\(->\), \("\<NF\>"["\<Inner\>"[
\*SuperscriptBox[\(s\), \(i\)]]]\)]
\*SuperscriptBox[\(y\), \(i\)])\)\)\),
\!\(\(
\*SuperscriptBox[\(l\), \(i\)] /; ListQ[l]\)
\*SubscriptBox[\(->\), \("\<Perm\>"\)]\(
\*SuperscriptBox[\(r\), \(i\)]\[DoubleLongLeftArrow]\((
\*SuperscriptBox[\(l\), \(i\)]
\*SubscriptBox[\(->\), \("\<permI\>"[1, Length[Permutations[
\*SuperscriptBox[\(l\), \(i\)]]]]\)]
\*SuperscriptBox[\(r\), \(i\)])\)\)\),
\!\(
\*SuperscriptBox[\(l\), \(i\)]
\*SubscriptBox[\(->\), \("\<permI\>"[
\*SuperscriptBox[\(n\), \(i\)], 
\*SuperscriptBox[\(_\), \(i\)]]\)]\(\(Permutations[
\*SuperscriptBox[\(l\), \(i\)]]\)[\([
\*SuperscriptBox[\(n\), \(i\)]]\)]\)\),
\!\(
\*SuperscriptBox[\(l\), \(i\)]
\*SubscriptBox[\(->\), \("\<permI\>"[
\*SuperscriptBox[\(n\), \(i\)], 
\*SuperscriptBox[\(m\), \(i\)]]\)]\(
\*SuperscriptBox[\(r\), \(i\)]\[DoubleLongLeftArrow]\((\((
\*SuperscriptBox[\(n\), \(i\)] < 
\*SuperscriptBox[\(m\), \(i\)])\) && \((
\*SuperscriptBox[\(l\), \(i\)]
\*SubscriptBox[\(->\), \("\<permI\>"[
\*SuperscriptBox[\(n\), \(i\)] + 1, 
\*SuperscriptBox[\(m\), \(i\)]]\)]
\*SuperscriptBox[\(r\), \(i\)])\))\)\)\),
\!\(\(
\*SuperscriptBox[\(l\), \(i\)] /; ListQ[l]\)
\*SubscriptBox[\(->\), \("\<Subset\>"\)]\(
\*SuperscriptBox[\(r\), \(i\)]\[DoubleLongLeftArrow]\((
\*SuperscriptBox[\(l\), \(i\)]
\*SubscriptBox[\(->\), \("\<ssI\>"[1, 2^Length[
\*SuperscriptBox[\(l\), \(i\)]]]\)]
\*SuperscriptBox[\(r\), \(i\)])\)\)\),
\!\(
\*SuperscriptBox[\(l\), \(i\)]
\*SubscriptBox[\(->\), \("\<ssI\>"[
\*SuperscriptBox[\(n\), \(i\)], 
\*SuperscriptBox[\(_\), \(i\)]]\)]\(\(Subsets[
\*SuperscriptBox[\(l\), \(i\)]]\)[\([
\*SuperscriptBox[\(n\), \(i\)]]\)]\)\),
\!\(
\*SuperscriptBox[\(l\), \(i\)]
\*SubscriptBox[\(->\), \("\<ssI\>"[
\*SuperscriptBox[\(n\), \(i\)], 
\*SuperscriptBox[\(m\), \(i\)]]\)]\(
\*SuperscriptBox[\(r\), \(i\)]\[DoubleLongLeftArrow]\((\((
\*SuperscriptBox[\(n\), \(i\)] < 
\*SuperscriptBox[\(m\), \(i\)])\) && \((
\*SuperscriptBox[\(l\), \(i\)]
\*SubscriptBox[\(->\), \("\<ssI\>"[
\*SuperscriptBox[\(n\), \(i\)] + 1, 
\*SuperscriptBox[\(m\), \(i\)]]\)]
\*SuperscriptBox[\(r\), \(i\)])\))\)\)\)
];


EndPackage[];
