Initialization

Needs["Theorema`"]

SetGlobals[TraceLevel->0];

SetGlobals[JuxtapositionForTimes->True];

Use[⟨Built–in["Numbers"],Built–in["Operators"],Built–in["Complex Numbers"],Built–in["Quantifiers"],Built–in["Tuples"],Built–in["Connectives"],Built–in["Sets"]⟩]

SetOptions[FlattenKB,ExpandFunctors->"replace"];

Off[General::"spell1"];

Unprotect[Or];ClearAll[Or];Protect[Or];

Off[Unset::"write"]

DeclareAsIdentifiers[(OverTilde[\[Placeholder]])]

Number Domains

Natural Numbers

Definition["ℕ",ℕ=NaturalNumbers[]]

Definition["Natural Numbers" ,any[],
NaturalNumbers[]=Functor[N,any[x,y],
	({{𝕤=⟨⟩}, {({{
(Underscript[∈, N])[x]⟺is–natural[x]}, {x(Underscript[>, N])y⇔x>y}, {(Underscript[⬚, N])=0}, {x(Underscript[*, N])y=x+y}, {(Underscript[lcm, N])[x,y]={({{x, ⇐, x>y}, {y, ⇐, True}})} }})}})
	]]

Mma Auxiliary Functions

Clear[mymult];

Begin["System`"];

mymult[x_,y_]:=x*y;

End[];

Built–in["Mult",
™MyMult->mymult]

Clear[myminus];

Begin["System`"];

myminus[x_,y_]:=x-y;

End[];

Built–in["Minus",
™MyMinus->myminus]

Clear[isnumber];

Begin["System`"];

isnumber[™D|L|R|A|B|⌈x__⌉|x|(x^(m_))]:=False;

isnumber[™Times[™D,m__]|™Times[L,m__]|™Times[R,m__]|™Times[A,m__]|™Times[B,m__]|™Times[™Ceiling[m__],y___]|™Times[x,y___]]:=False;

isnumber[x_]:=(x/.{™I->I,™E->E,™Times->Times,™Plus->Plus,™Minus->Minus,™Divide->Divide,™Power->Power})∈Complexes;

End[];

Built–in["IsNumber",
™IsNumber->isnumber]

Definition["Mma Auxiliary Functions" ,any[],
MmaAuxF[]=Functor[N,any[x,y],
	({{𝕤=⟨⟩}, {({{(Underscript[∈, N])[x]⟺™IsNumber[x]}, {x(Underscript[·, N])y=™MyMult[x,y]}, {x(Underscript[-, N])y=™MyMinus[x,y]}})}})
	]]

Reduction Field

Definition["Reduction Field" ,any[D],
ReductionField[D]=Functor[⟨N,extends[D]⟩,any[x,y],
	({{𝕤=⟨⟩}, {({{
(Underscript[∈, N])[x]⇔(Underscript[∈, D])[x]}, {(Underscript[0, N])=(Underscript[0, D])}, {(Underscript[1, N])=(Underscript[1, D])}, {x(Underscript[+, N])y=x(Underscript[+, D])y}, {(Underscript[-, N])x=(Underscript[-, D])x}, {x(Underscript[-, N])y=x(Underscript[-, D])y}, {x(Underscript[*, N])y=x(Underscript[*, D])y}, {x(Underscript[/, N])y=x(Underscript[/, D])y}, {x(Underscript[>, N])y⇔x(Underscript[>, D])y}, {x(Underscript[≻, N])y⇔((x≠(Underscript[0, D]))∧(y=(Underscript[0, D])))}, {(Underscript[rdm, N])[x,y]  (* the reduction multiplier of x modulo y  *) ={({{x(Underscript[/, D])y, ⇐, x≠(Underscript[0, D])∧y≠(Underscript[0, D])}, {(Underscript[0, D]), ⇐, otherwise}})} }, {(Underscript[lcrd, N])[x,y] (* the least common reducible of x and y  *) ={({{(Underscript[1, D]), ⇐, x≠(Underscript[0, D])∧y≠(Underscript[0, D])}, {(Underscript[0, D]), ⇐, otherwise}})}}})}})
	]]

Rational Number Field

Definition["ℚ",ℚ=RationalNumberField[]]

Definition["Rational Number Field" ,any[],
RationalNumberField[]=Functor[N,any[x,y],
	({{𝕤=⟨⟩}, {({{
(Underscript[∈, N])[x]⟺is–rational[x]}, {x(Underscript[>, N])y⇔x>y}, {(Underscript[0, N])=0}, {(Underscript[1, N])=1}, {x(Underscript[+, N])y=x+y}, {(Underscript[-, N])x=-x}, {x(Underscript[-, N])y=x-y}, {x(Underscript[*, N])y=x*y}, {(Underscript[∇, N])x=1/x}, {x(Underscript[/, N])y=x/y}, {(Underscript[power, N])[x,0]=(Underscript[1, N])}, {(Underscript[power, N])[x,y]=x(Underscript[*, N])(Underscript[power, N])[x,y-1]}})}})
	]]

Complex Numbers

IsComplex

Clear[IsComplex];

Begin["System`"];

IsComplex[x_]:=(x/.{™I->I,™E->E})∈Complexes;

End[];

Built–in["IsComplex",
™IsComplex->IsComplex]

$TmaOperatorTranslations=DeleteCases[$TmaOperatorTranslations,tr_/;MemberQ[tr,™E|™I,∞]];

ComplexLt

Clear[ComplexLt];

Begin["System`"];

ComplexLt[x_,x_]:=False;

ComplexLt[x_,y_]:=OrderedQ[{x,y}/.{™I->I,™E->E}] ;

End[];

Built–in["ComplexLt",
™ComplexLt->ComplexLt]

ComplexNumberField

Definition["ℂ",ℂ=ComplexNumberField[]]

Definition["Complex Number Field" ,any[],
ComplexNumberField[]=Functor[N,any[x,y,z],
	({{𝕤=⟨⟩}, {({{
(Underscript[∈, N])[x]⟺™IsComplex[x]}, {x(Underscript[>, N])y⇔™ComplexLt[y,x]}, {(Underscript[0, N])=0}, {(Underscript[1, N])=1}, {x(Underscript[+, N])y=x+y}, {x(Underscript[*, N])y=(Underscript[simplify, N])[x*y]}, {x(Underscript[*, N])y(Underscript[*, N])z=(x(Underscript[*, N])y)(Underscript[*, N])z}, {(Underscript[-, N])x=-x}, {x(Underscript[-, N])y=x-y}, {(Underscript[∇, N])x=1/x}, {x(Underscript[/, N])y=x/y}, {(Underscript[lcm, N])[x,y]={({{x, ⇐, x>y}, {y, ⇐, True}})} }, {(Underscript[power, N])[x,y]=Power[x,y]}, {(Underscript[exp, N])[x]=Exp[x]}, {(Underscript[simplify, N])[x]=mma–simplify[x]}, {(Underscript[PrettyPrint, N])[x]=x}})}})
	]]

ComplexNumbersMonoid

Definition["ℂM",ℂM=ComplexNumbers[]]

Definition["Complex Numbers" ,any[],
ComplexNumbers[]=Functor[N,any[x,y],
	({{𝕤=⟨⟩}, {({{
(Underscript[∈, N])[x]⟺™IsComplex[x]}, {x(Underscript[>, N])y⇔™ComplexLt[y,x]}, {(Underscript[⬚, N])=0}, {x(Underscript[*, N])y=x+y}, {(Underscript[lcm, N])[x,y]={({{x, ⇐, x>y}, {y, ⇐, True}})} }})}})
	]]

Word Monoids

Definition["Finite Chain",any[L],
FinChain[L]=Functor[C,any[x,y],
	({{𝕤=⟨⟩}, {({{(Underscript[∈, C])[x]⟺(x∈L)}, {x(Underscript[>, C])y⇔(Underscript[∃, i=1,…,\[LeftBracketingBar]L\[RightBracketingBar]])(Underscript[∃, j=i+1,…,\[LeftBracketingBar]L\[RightBracketingBar]])((x=(Subscript[L, i]))∧(y=(Subscript[L, j])))}})}})]]

Definition["Cartesian Product",any[D,(OverBar[D]),A,B],
({{CartesianProduct[D,(OverBar[D])]=Functor[N,any[X,Y,(OverBar[X]),(OverBar[Y])],
	({{𝕤=⟨⟩}, {({{(Underscript[∈, N])[X]⟺(is–tuple[X]∧(\[LeftBracketingBar]⟨D,(OverBar[D])⟩\[RightBracketingBar]=\[LeftBracketingBar]X\[RightBracketingBar])∧(Underscript[∀, j=1,…,\[LeftBracketingBar]⟨D,(OverBar[D])⟩\[RightBracketingBar]])((Underscript[∈, (Subscript[⟨D,(OverBar[D])⟩, j])])[(Subscript[X, j])]))}, {(Underscript[⬚, N])=⟨(Underscript[⬚, (Subscript[⟨D,(OverBar[D])⟩, j])])(Underscript[|, j=1,…,\[LeftBracketingBar]⟨D,(OverBar[D])⟩\[RightBracketingBar]])⟩}, {X(Underscript[>, N])Y⇔((Underscript[∃, k=1,…,\[LeftBracketingBar]⟨D,(OverBar[D])⟩\[RightBracketingBar]])(∧{({{(Subscript[X, k])(Underscript[>, (Subscript[⟨D,(OverBar[D])⟩, k])])(Subscript[Y, k])}, {(Underscript[∀, l=1,…,k-1])((Subscript[X, l])=(Subscript[Y, l]))}})}))}, {X(Underscript[*, N])Y=⟨(Subscript[X, m])(Underscript[*, (Subscript[⟨D,(OverBar[D])⟩, m])])(Subscript[Y, m])(Underscript[|, m=1,…,\[LeftBracketingBar]⟨D,(OverBar[D])⟩\[RightBracketingBar]])⟩}, {(Underscript[lcm, N])[⟨X,(OverBar[X])⟩,⟨Y,(OverBar[Y])⟩]=⟨(Underscript[lcm, (Subscript[⟨D,(OverBar[D])⟩, n])])[(Subscript[⟨X,(OverBar[X])⟩, n]),(Subscript[⟨Y,(OverBar[Y])⟩, n])](Underscript[|, n=1,…,\[LeftBracketingBar]⟨X,(OverBar[X])⟩\[RightBracketingBar]])⟩}})}})
	]}, {A\[Cross]B=CartesianProduct[A,B]}})]

Definition["Tuples Monoid",any[A],
TuplesMonoid[A]=Functor[N,any[x,y,z,(OverBar[x]),(OverBar[y]),X,Y],
	({{𝕤=⟨⟩}, {({{(Underscript[∈, N])[X]⟺((is–tuple[X]∧((Underscript[∀, i=1,…,\[LeftBracketingBar]X\[RightBracketingBar]])(Underscript[∈, A])[(Subscript[X, i])])∧((Subscript[X, \[LeftBracketingBar]X\[RightBracketingBar]])≠0))∨(X=⟨⟩))}, {(Underscript[⬚, N])=⟨⟩}, {(⟨x,(OverBar[x])⟩(Underscript[>, N])⟨⟩)⇔True}, {(⟨⟩(Underscript[>, N])⟨(OverBar[y])⟩)⇔False}, {(⟨x,(OverBar[x])⟩(Underscript[>, N])⟨y,(OverBar[y])⟩)⇔(∨{({{(x=y) ∧⟨(OverBar[x])⟩(Underscript[>, N])⟨(OverBar[y])⟩}, {x(Underscript[>, A])y}})} )}, {x(Underscript[*, N])⟨⟩=x}, {⟨⟩(Underscript[*, N])y=y}, {⟨(OverBar[x]),x⟩(Underscript[*, N])⟨(OverBar[y]),y⟩=
{({{⟨(Subscript[⟨(OverBar[x]),x⟩, k])(Underscript[*, A])(Subscript[⟨(OverBar[y]),y⟩, k])(Underscript[|, k=1,…,\[LeftBracketingBar]⟨(OverBar[x]),x⟩\[RightBracketingBar]])⟩, ⇐, (\[LeftBracketingBar]⟨(OverBar[y]),y⟩\[RightBracketingBar]=\[LeftBracketingBar]⟨(OverBar[x]),x⟩\[RightBracketingBar])}, {⟨(Subscript[⟨(OverBar[x]),x⟩, k])(Underscript[*, A])(Subscript[⟨(OverBar[y]),y⟩, k])(Underscript[|, k=1,…,\[LeftBracketingBar]⟨(OverBar[x]),x⟩\[RightBracketingBar]])⟩≍⟨(Subscript[⟨(OverBar[y]),y⟩, k])(Underscript[|, k=\[LeftBracketingBar]⟨(OverBar[x]),x⟩\[RightBracketingBar]+1,…,\[LeftBracketingBar]⟨(OverBar[y]),y⟩\[RightBracketingBar]])⟩, ⇐, \[LeftBracketingBar]⟨(OverBar[y]),y⟩\[RightBracketingBar]>\[LeftBracketingBar]⟨(OverBar[x]),x⟩\[RightBracketingBar]}, {⟨(Subscript[⟨(OverBar[x]),x⟩, k])(Underscript[*, A])(Subscript[⟨(OverBar[y]),y⟩, k])(Underscript[|, k=1,…,\[LeftBracketingBar]⟨(OverBar[y]),y⟩\[RightBracketingBar]])⟩≍⟨(Subscript[⟨(OverBar[x]),x⟩, k])(Underscript[|, k=\[LeftBracketingBar]⟨(OverBar[y]),y⟩\[RightBracketingBar]+1,…,\[LeftBracketingBar]⟨(OverBar[x]),x⟩\[RightBracketingBar]])⟩, ⇐, otherwise}})} }, {(Underscript[lcm, N])[x,⟨⟩]=x}, {(Underscript[lcm, N])[⟨⟩,y]=y}, {(Underscript[lcm, N])[⟨x,(OverBar[x])⟩,⟨y,(OverBar[y])⟩]={({{x⌣(Underscript[lcm, N])[⟨(OverBar[x])⟩,⟨(OverBar[y])⟩], ⇐, x(Underscript[>, A])y}, {y⌣(Underscript[lcm, N])[⟨(OverBar[x])⟩,⟨(OverBar[y])⟩], ⇐, otherwise}})} }})}})
	]]

Cartesian Product

Definition["Cartesian Power",any[D,n],
CartesianPower[D,n]=CartesianProduct[D(Underscript[|, i=1,…,n])]]

Definition["Word Monoid",any[L],
LexWords[L]=Functor[W,any[u,v,w,ξ,η,(OverBar[ξ]),(OverBar[η]),(OverBar[ζ])],
	({{𝕤=⟨⟩}, {({{(Underscript[∈, W])[w]⟺(∧{({{is–tuple[w]}, {(Underscript[∀, i=1,…,\[LeftBracketingBar]w\[RightBracketingBar]])(Underscript[∈, L])[(Subscript[w, i])]}})})}, {(Underscript[⬚, W])(* empty word *)=⟨⟩}, {v(Underscript[*, W])w(* multiplication of two words *)=v≍w}, {u(Underscript[*, W])v(Underscript[*, W])w(* multiplication of three words *)=(u(Underscript[*, W])v)(Underscript[*, W])w}, {(⟨(OverBar[η])⟩(Underscript[∣, W])⟨(OverBar[ζ]),(OverBar[η]),(OverBar[ξ])⟩)(* middle divisibility *)⇔True}, {(⟨(OverBar[η])⟩(Underscript[∣, W])⟨(OverBar[ξ])⟩)⇔False}, {(Underscript[rquot, W])[⟨⟩,v](* right quotient *)=(Underscript[⬚, W])}, {(Underscript[rquot, W])[⟨(OverBar[ξ]),(OverBar[η])⟩,⟨(OverBar[η])⟩]=(Underscript[⬚, W])}, {(Underscript[rquot, W])[w,v]=(Underscript[rquot, W])[⟨(Subscript[w, i])(Underscript[|, i=1,…,\[LeftBracketingBar]w\[RightBracketingBar]-1])⟩,v]⌢(Subscript[w, \[LeftBracketingBar]w\[RightBracketingBar]])}, {(Underscript[lquot, W])[w,v](* left quotient *)=⟨(Subscript[w, i])(Underscript[|, i=1,…,\[LeftBracketingBar]w\[RightBracketingBar]-\[LeftBracketingBar]v\[RightBracketingBar]-\[LeftBracketingBar](Underscript[rquot, W])[w,v]\[RightBracketingBar]])⟩ }, {(Underscript[lcm, W])[⟨(OverBar[η]),(OverBar[ζ])⟩,⟨(OverBar[ζ]),(OverBar[ξ])⟩](* the least common reducible *)=⟨(OverBar[η]),(OverBar[ζ]),(OverBar[ξ])⟩}, {(⟨η,(OverBar[η])⟩(Underscript[>, W])⟨⟩)(* lexicographic ordering *)⇔True}, {(⟨⟩(Underscript[>, W])⟨(OverBar[η])⟩)⇔False}, {(⟨η,(OverBar[η])⟩(Underscript[>, W])⟨ξ,(OverBar[ξ])⟩)⇔(∨{({{(η=ξ) ∧⟨(OverBar[η])⟩(Underscript[>, W])⟨(OverBar[ξ])⟩}, {η(Underscript[>, L])ξ}})} )}})}})]]

Definition["Word Monoid with Degree Ordering",any[L],
DegWords[L]=where[B=LexWords[L],
Functor[W,any[u,v,w,η,(OverBar[η])],
	({{𝕤=⟨⟩}, {({{(Underscript[∈, W])[w]⟺(Underscript[∈, B])[w]}, {(Underscript[⬚, W])=(Underscript[⬚, B])}, {v(Underscript[*, W])w=v(Underscript[*, B])w}, {u(Underscript[*, W])v(Underscript[*, W])w=u(Underscript[*, B])v(Underscript[*, B])w}, {(v(Underscript[∣, W])w)⇔(v(Underscript[∣, B])w)}, {(Underscript[rquot, W])[w,v]=(Underscript[rquot, B])[w,v]}, {(Underscript[lquot, W])[w,v]=(Underscript[lquot, B])[w,v] }, {(Underscript[lcm, W])[w,v]=(Underscript[lcm, B])[w,v]}, {(⟨η,(OverBar[η])⟩(Underscript[>, W])⟨⟩)(* degree ordering *)⇔True}, {(⟨⟩(Underscript[>, W])⟨(OverBar[η])⟩)⇔False}, {(v(Underscript[>, W])w)⇔(∨{({{\[LeftBracketingBar]v\[RightBracketingBar]>\[LeftBracketingBar]w\[RightBracketingBar]}, {∧{({{\[LeftBracketingBar]v\[RightBracketingBar]=\[LeftBracketingBar]w\[RightBracketingBar]}, {v(Underscript[>, B])w}})} }})} )}})}})]]]

Free Module

Definition["Free Module",any[K,B],
FreeModule[K,B]=Functor[V,any[c,d,x,y,ξ,η,A,(OverBar[x]),(OverBar[y])],
	({{𝕤=⟨⟩}, {({{(Underscript[∈, V])[x]⟺(where[z=\[LeftBracketingBar]x\[RightBracketingBar],∧{({{is–tuple[x]}, {(Underscript[∀, i=1,…,z])(∧{({{is–tuple[(Subscript[x, i])]}, {\[LeftBracketingBar](Subscript[x, i])\[RightBracketingBar]=2}, {(Underscript[is–coeff, V])[(Subscript[((Subscript[x, i])), 1])]}, {(Underscript[is–bvec, V])[(Subscript[((Subscript[x, i])), 2])]}})})}, {(Underscript[∀, i=1,…,z-1])(Subscript[((Subscript[x, i])), 2])(Underscript[>, B])(Subscript[((Subscript[x, i+1])), 2])}})}])}, {(Underscript[is–bvec, V])[ξ]⇔(Underscript[∈, B])[ξ]}, {(Underscript[is–coeff, V])[c]⇔((Underscript[∈, K])[c]∧c≠(Underscript[0, K]))}, {(Underscript[bvec, V])[ξ]=⟨⟨(Underscript[1, K]),ξ⟩⟩}, {(Underscript[to–bvec, V])[⟨⟨c,ξ⟩⟩]={({{ξ, ⇐, c=(Underscript[1, K])}, {(Underscript[⬚, B]), ⇐, otherwise}})} }, {(Underscript[to–bvec, V])[A]=(Underscript[⬚, B])}, {(Underscript[0, V])=⟨⟩}, {⟨⟩(Underscript[+, V])y=y}, {x(Underscript[+, V])⟨⟩=x}, {⟨⟨c,ξ⟩,(OverBar[x])⟩(Underscript[+, V])⟨⟨d,η⟩,(OverBar[y])⟩={({{⟨c,ξ⟩⌣(⟨(OverBar[x])⟩(Underscript[+, V])⟨⟨d,η⟩,(OverBar[y])⟩), ⇐, ξ(Underscript[>, B])η}, {⟨d,η⟩⌣(⟨⟨c,ξ⟩,(OverBar[x])⟩(Underscript[+, V])⟨(OverBar[y])⟩), ⇐, η(Underscript[>, B])ξ}, {⟨c(Underscript[+, K])d,ξ⟩⌣(⟨(OverBar[x])⟩(Underscript[+, V])⟨(OverBar[y])⟩), ⇐, (ξ=η)∧c(Underscript[+, K])d≠(Underscript[0, K])}, {⟨(OverBar[x])⟩(Underscript[+, V])⟨(OverBar[y])⟩, ⇐, otherwise}})} }, {V[+][x,(OverBar[x])]=x(Underscript[+, V])V[+][(OverBar[x])]}, {(Underscript[-, V])⟨⟩=⟨⟩}, {(Underscript[-, V])⟨⟨c,ξ⟩,(OverBar[x])⟩=⟨(Underscript[-, K])c,ξ⟩⌣((Underscript[-, V])⟨(OverBar[x])⟩)}, {x(Underscript[-, V])y=x(Underscript[+, V])((Underscript[-, V])y)}, {0(Underscript[·, V])y(* scalar multiplication *)=⟨⟩}, {c(Underscript[·, V])⟨⟩=⟨⟩}, {c(Underscript[·, V])⟨⟨d,η⟩,(OverBar[y])⟩=⟨c(Underscript[*, K])d,η⟩⌣c(Underscript[·, V])⟨(OverBar[y])⟩}, {y(Underscript[·, V])0=⟨⟩}, {⟨⟩(Underscript[·, V])c=⟨⟩}, {⟨⟨c,ξ⟩,(OverBar[x])⟩(Underscript[·, V])d=⟨c(Underscript[*, K])d,ξ⟩⌣⟨(OverBar[x])⟩(Underscript[·, V])d}, {(Underscript[coord, V])[⟨⟩,x](* coordinate wrt a basis *)=⟨⟩}, {(Underscript[coord, V])[⟨⟨c,ξ⟩,(OverBar[x])⟩,ξ]=c}, {(Underscript[coord, V])[⟨⟨c,ξ⟩,x,(OverBar[x])⟩,η]=(Underscript[coord, V])[⟨x,(OverBar[x])⟩,η]}, {(Underscript[coord, V])[⟨⟨c,ξ⟩⟩,η]=(Underscript[0, K])}, {(⟨⟩(Underscript[>, V])y)(* ordering *)⇔False}, {(⟨⟨c,ξ⟩,(OverBar[x])⟩(Underscript[>, V])⟨⟩)⇔True}, {(⟨⟨c,ξ⟩,(OverBar[x])⟩(Underscript[>, V])⟨⟨d,η⟩,(OverBar[y])⟩)⇔(∨{({{ξ(Underscript[>, B])η}, {∧{({{ξ=η}, {c(Underscript[>, K])d}})} }, {∧{({{ξ=η}, {c=d}, {⟨(OverBar[x])⟩(Underscript[>, V])⟨(OverBar[y])⟩}})} }})} )}})}})]]

Monoid Algebra

Definition["Monoid Algebra",any[K,W],
MonoidAlgebra[K,W]=where[V=FreeModule[K,W],
Functor[P,any[c,d,f,g,ξ,η,(OverBar[f]),(OverBar[m]),(OverBar[n])],
	({{𝕤=⟨⟩}, {({{(Underscript[∈, P])[f]⟺(Underscript[∈, V])[f]}, {(Underscript[is–bvec, P])[ξ]⇔(Underscript[is–bvec, V])[ξ]}, {(Underscript[is–coeff, P])[c]⇔(Underscript[is–coeff, V])[c]}, {(Underscript[0, P])=(Underscript[0, V])}, {P[+][(OverBar[f])]=V[+][(OverBar[f])]}, {(Underscript[-, P])f=(Underscript[-, V])f}, {f(Underscript[-, P])g=f(Underscript[-, V])g}, {(Underscript[ew, P])[ξ]=(Underscript[bvec, V])[ξ]}, {c(Underscript[·, P])f=c(Underscript[·, V])f}, {(Underscript[coord, P])[f,ξ]=(Underscript[coord, V])[f,ξ]}, {(Underscript[1, P])=⟨⟨(Underscript[1, K]),(Underscript[⬚, W])⟩⟩}, {⟨⟩(Underscript[*, P])g(* multiplication of two polynomials *)=⟨⟩}, {f(Underscript[*, P])⟨⟩=⟨⟩}, {⟨⟨c,ξ⟩,(OverBar[m])⟩(Underscript[*, P])⟨⟨d,η⟩,(OverBar[n])⟩=(⟨⟨c(Underscript[*, K])d,ξ(Underscript[*, W])η⟩⟩(Underscript[+, P])⟨⟨c,ξ⟩⟩(Underscript[*, P])⟨(OverBar[n])⟩)(Underscript[+, P])⟨(OverBar[m])⟩(Underscript[*, P])⟨⟨d,η⟩,(OverBar[n])⟩}, {P[*][f,(OverBar[f])]=f(Underscript[*, P])P[*][(OverBar[f])]}, {(⟨⟩(Underscript[>, P])g)(* ordering *)⇔False}, {(⟨⟨c,ξ⟩,(OverBar[m])⟩(Underscript[>, P])⟨⟩)⇔True}, {(⟨⟨c,ξ⟩,(OverBar[m])⟩(Underscript[>, P])⟨⟨d,η⟩,(OverBar[n])⟩)⇔(∨{({{ξ(Underscript[>, W])η}, {∧{({{ξ=η}, {c(Underscript[>, K])d}})} }, {∧{({{ξ=η}, {c=d}, {⟨(OverBar[m])⟩(Underscript[>, P])⟨(OverBar[n])⟩}})} }})} )}, {(Underscript[rrdm, P])[⟨⟩,g](* right reduction multiplier *)=(Underscript[0, P])}, {(Underscript[rrdm, P])[⟨⟨c,ξ⟩,(OverBar[m])⟩,⟨⟩]=(Underscript[0, P])}, {(Underscript[rrdm, P])[⟨⟨c,ξ⟩,(OverBar[m])⟩,⟨⟨d,η⟩,(OverBar[n])⟩]={({{⟨⟨(Underscript[rdm, K])[c,d],(Underscript[rquot, W])[ξ,η]⟩⟩, ⇐, (Underscript[rdm, K])[c,d]≠(Underscript[0, K])∧η(Underscript[∣, W])ξ}, {(Underscript[0, P]), ⇐, otherwise}})}}, {(Underscript[lrdm, P])[⟨⟩,f](* left reduction multiplier *)=(Underscript[0, P])}, {(Underscript[lrdm, P])[⟨⟨c,ξ⟩,(OverBar[m])⟩,⟨⟩]=(Underscript[0, P])}, {(Underscript[lrdm, P])[⟨⟨c,ξ⟩,(OverBar[m])⟩,⟨⟨d,η⟩,(OverBar[n])⟩]={({{⟨⟨(Underscript[1, K]),(Underscript[lquot, W])[ξ,η]⟩⟩, ⇐, (Underscript[rdm, K])[c,d]≠(Underscript[0, K])∧η(Underscript[∣, W])ξ}, {(Underscript[0, P]), ⇐, otherwise}})}}, {(Underscript[lcrd, P])[⟨⟨c,ξ⟩,(OverBar[m])⟩,⟨⟨d,η⟩,(OverBar[n])⟩](* least common reducible *)=⟨⟨(Underscript[lcrd, K])[c,d],(Underscript[lcm, W])[ξ,η]⟩⟩}})}})
]]]

Definition["Groebner Extension",any[P],
GB[P]=Functor[⟨G,extends[P]⟩,any[c,f,g,k,l,r,t,ξ,lhs1,lhs2,rhs1,rhs2,(OverBar[f]),(OverBar[m]),R,S],
	({{𝕤=⟨⟩}, {({{f(Underscript[>, G])g⇔f(Underscript[>, P])g}, {(Underscript[0, G])=(Underscript[0, P])}, {(Underscript[1, G])=(Underscript[1, P])}, {f(Underscript[+, G])g⇔f(Underscript[+, P])g}, {G[*][f,(OverBar[f])]=P[*][f,(OverBar[f])]}, {(Underscript[hredp, G])[f,g](* head reduction modulo polynomial *)=f(Underscript[-, P])(Underscript[lrdm, P])[f,g](Underscript[*, P])g(Underscript[*, P])(Underscript[rrdm, P])[f,g]}, {(Underscript[hredp, G])[f,g,l,r]=f(Underscript[-, P])l(Underscript[*, P])g(Underscript[*, P])r}, {(Underscript[hred, G])[f,S](* head reduction modulo system *)=where[q=S[f],
(Underscript[hredp, G])[f,(Subscript[q, 2]),(Subscript[q, 1]),(Subscript[q, 3])]]}, {(Underscript[sred, G])[⟨⟩,S,t](* step reduction modulo system at given position *)=(Underscript[0, P])}, {(Underscript[sred, G])[⟨⟨c,ξ⟩,(OverBar[m])⟩,S,1]=(Underscript[hred, G])[⟨⟨c,ξ⟩,(OverBar[m])⟩,S]}, {(Underscript[sred, G])[⟨⟨c,ξ⟩,(OverBar[m])⟩,S,t]=⟨⟨c,ξ⟩⟩(Underscript[+, G])(Underscript[sred, G])[⟨(OverBar[m])⟩,S,t-1]}, {(Underscript[sred, G])[f,S](* step reduction modulo system *)=(Underscript[cred, G])[f,S,1]}, {(Underscript[cred, G])[f,S,k](* complete reduction modulo system at given position *)=
where[f1=(Underscript[sred, G])[f,S,k],
{({{(Underscript[cred, G])[f,S,k+1], ⇐, (f1=f)∧(k<\[LeftBracketingBar]f\[RightBracketingBar])}, {f1, ⇐, otherwise}})} ]}, {(Underscript[ tred, G])[f,S] (* total reduction modulo system *)=where[q=(Underscript[sred, G])[f,S],
{({{(Underscript[tred, G])[q,S], ⇐, q≠f}, {f, ⇐, otherwise}})} ] }, {(Underscript[spol, G])[f,g](* the S-polynomial of f and g *)=where[L=(Underscript[lcrd, P])[f,g],
(Underscript[hredp, G])[L,f](Underscript[-, G])(Underscript[hredp, G])[L,g]]}, {(Underscript[spolred, G])[⟨f,g⟩,S]=(Underscript[tred, G])[(Underscript[spol, G])[f,g],S]}, {(Underscript[Gb, G])[R,S]=where[pairs=⟨⟨(Subscript[R, i]),(Subscript[R, j])⟩(Underscript[|, ({{i=1,…,\[LeftBracketingBar]R\[RightBracketingBar]}, {j=1,…,\[LeftBracketingBar]R\[RightBracketingBar]}})])(Subscript[R, i])≠(Subscript[R, j])⟩,
(Underscript[Gb, G])[R,pairs,S]]}, {(Underscript[Gb, G])[R,⟨⟩,S]=R}, {(Underscript[Gb, G])[R,⟨⟨f,g⟩,(OverBar[m])⟩,S]=where[h=(Underscript[spolred, G])[⟨f,g⟩,S],
{({{(Underscript[Gb, G])[R,⟨(OverBar[m])⟩,S], ⇐, h=(Underscript[0, P])}, {(Underscript[Gb, G])[R⌢h,((h⇥R)≍⟨(OverBar[m])⟩)≍(R⇤h),S], ⇐, otherwise}})}
]}})}})]]

Definition["Theorema general functions",any[F,l,r],
({{l⇥F=⟨⟨l,(Subscript[F, i])⟩(Underscript[\[VerticalSeparator], i=1,…,\[LeftBracketingBar]F\[RightBracketingBar]])⟩}, {F⇤r=⟨⟨(Subscript[F, i]),r⟩(Underscript[\[VerticalSeparator], i=1,…,\[LeftBracketingBar]F\[RightBracketingBar]])⟩}})]

Exponential Polynomials

MakeBoxes&MakeExpressions (Formatting&Parsing)

MakeExpression[RowBox[{SubscriptBox["∂",Q_],p_}],StandardForm]:=
MakeExpression[RowBox[{RowBox[{Q,"[","™Der","]"}],"[",p,"]"}],StandardForm];

MakeExpression[RowBox[{SubscriptBox["∫",Q_],p_}],StandardForm]:=
MakeExpression[RowBox[{RowBox[{Q,"[","™Int","]"}],"[",p,"]"}],StandardForm];

MakeBoxes[Q_[™Der][p_],StandardForm]:=
RowBox[{SubscriptBox["∂",MakeBoxes[Q,StandardForm]],MakeBoxes[p,StandardForm]}];

MakeBoxes[Q_[™Int][p_],StandardForm]:=
RowBox[{SubscriptBox["∫",MakeBoxes[Q,StandardForm]],MakeBoxes[p,StandardForm]}];

MakeExpression[RowBox[{"⌈",x_,"⌉"}],StandardForm]:=MakeExpression[RowBox[{"™Ceiling","[",x,"]"}],StandardForm];

MakeBoxes[™Ceiling[x_],StandardForm]:=RowBox[{"⌈",MakeBoxes[x,StandardForm],"⌉"}];

MakeExpression[RowBox[{"⌊",x_,"⌋"}],StandardForm]:=MakeExpression[RowBox[{"™Floor","[",x,"]"}],StandardForm];

MakeBoxes[™Floor[x_],StandardForm]:=RowBox[{"⌊",MakeBoxes[x,StandardForm],"⌋"}];

Built–ins

Begin["System`"];

MmaSimplify[p_]:=FullSimplify[p];

End[];

Built–in["MmaSimplify",
mma–simplify->MmaSimplify]

Exponential Polynomials

Definition["Exp Polys",any[K],
ExpPolys[K]=where[P=MonoidAlgebra[K,ℕ\[Cross]ℂM],
Functor[E,any[c,d,m,p,q,λ,ξ,(OverBar[m]),(OverBar[n])],
	({{𝕤=⟨⟩}, {({{(Underscript[∈, E])[p]⟺(Underscript[∈, P])[p]}, {(Underscript[0, E])=(Underscript[0, P])}, {(Underscript[1, E])=(Underscript[1, P])}, {p(Underscript[>, E])q⇔p(Underscript[>, P])q}, {p(Underscript[+, E])q=p(Underscript[+, P])q}, {(Underscript[-, E])p=(Underscript[-, P])p}, {p(Underscript[-, E])q=p(Underscript[-, P])q}, {c(Underscript[·, E])p=c(Underscript[·, P])p}, {p(Underscript[*, E])q=p(Underscript[*, P])q}, {(Underscript[ew, E])[p]=(Underscript[ew, P])[p]}, {(Underscript[coord, E])[p,ξ]=(Underscript[coord, P])[p,ξ]}, {(Underscript[is–bvec, E])[ξ]⇔(Underscript[is–bvec, P])[ξ]}, {(Underscript[is–coeff, E])[c]⇔(Underscript[is–coeff, P])[c]}, {(Underscript[lcrd, E])[⟨⟨c,λ⟩⟩,⟨⟨d,ξ⟩⟩]=⟨⟨(Underscript[lcrd, K])[c,d],(Underscript[lcm, ℕ\[Cross]ℂM])[λ,ξ]⟩⟩}, {(Underscript[is–scal, E])[⟨⟨c,(Underscript[⬚, ℕ\[Cross]ℂM])⟩⟩]⇔(Underscript[is–coeff, P])[c]}, {(Underscript[is–scal, E])[p]⇔False}, {(Underscript[to–scal, ℱ])[⟨⟩]=(Underscript[0, K])}, {(Underscript[to–scal, E])[⟨⟨c,(Underscript[⬚, ℕ\[Cross]ℂM])⟩⟩]=c}, {(Underscript[eval, E])[⟨⟩,d]=(Underscript[0, K])}, {(Underscript[eval, E])[⟨⟨c,⟨⟩⟩⟩,d]=c}, {(Underscript[eval, E])[⟨⟨c,⟨0,λ⟩⟩⟩,d]=c(Underscript[*, K])(Underscript[exp, K])[λ(Underscript[*, K])d]}, {(Underscript[eval, E])[⟨⟨c,⟨m,λ⟩⟩,(OverBar[m])⟩,d]=c(Underscript[*, K])(Underscript[power, K])[d,m](Underscript[*, K])(Underscript[exp, K])[λ(Underscript[*, K])d](Underscript[+, K])(Underscript[eval, E])[⟨(OverBar[m])⟩,d]}, {(∂_E)⟨⟩=(Underscript[0, P])}, {(∂_E)⟨⟨c,⟨⟩⟩⟩=(Underscript[0, P])}, {(∂_E)⟨⟨c,⟨0,λ⟩⟩,(OverBar[n])⟩=λ(Underscript[·, P])⟨⟨c,⟨0,λ⟩⟩⟩(Underscript[+, P])(∂_E)⟨(OverBar[n])⟩}, {(∂_E)⟨⟨c,⟨m,λ⟩⟩,(OverBar[n])⟩=⟨⟨c(Underscript[*, K])m,⟨m-1,λ⟩⟩⟩(Underscript[+, P])λ(Underscript[·, P])⟨⟨c,⟨m,λ⟩⟩⟩(Underscript[+, P])(∂_E)⟨(OverBar[n])⟩}, {(∫_E)⟨⟩=(Underscript[0, P])}, {(∫_E)⟨⟨c,⟨⟩⟩⟩=⟨⟨c,⟨1,0⟩⟩⟩}, {(∫_E)⟨⟨c,⟨m,0⟩⟩,(OverBar[n])⟩=⟨⟨c(Underscript[/, K])(m+1),⟨m+1,0⟩⟩⟩(Underscript[+, P])(∫_E)⟨(OverBar[n])⟩}, {(∫_E)⟨⟨c,⟨0,λ⟩⟩,(OverBar[n])⟩=(⟨⟨c(Underscript[/, K])λ,⟨0,λ⟩⟩⟩(Underscript[-, P])⟨⟨c(Underscript[/, K])λ,⟨0,0⟩⟩⟩)(Underscript[+, P])(∫_E)⟨(OverBar[n])⟩}, {(∫_E)⟨⟨c,⟨m,λ⟩⟩,(OverBar[n])⟩=(⟨⟨c(Underscript[/, K])λ,⟨m,λ⟩⟩⟩(Underscript[-, P])(∫_E)m(Underscript[·, P])⟨⟨c(Underscript[/, K])λ,⟨m-1,λ⟩⟩⟩)(Underscript[+, P])(∫_E)⟨(OverBar[n])⟩}, {(Underscript[PrettyPrint, E])[p]=™Plus[(Underscript[PrettyPrintM, E])[(Subscript[p, i])](Underscript[|, i=1,…,\[LeftBracketingBar]p\[RightBracketingBar]])]}, {(Underscript[PrettyPrint, E])[⟨m⟩]=(Underscript[PrettyPrintM, E])[m]}, {(Underscript[PrettyPrint, E])[⟨⟩]=0}, {(Underscript[PrettyPrintM, E])[⟨c,⟨m,λ⟩⟩]=™Times[c,™Times[(x^m),((™E)^(λ x))]]}})}})]]]

Built–ins

Begin["System`"];

Clear[CoeffQ,Mon,Coeff,SplitPoly,FuncOrder];

CoeffQ[expr_]:=FreeQ[expr,x];

Mon[t1_,t2___]:=Mon[t1*t2];

Mon[Times[c_?CoeffQ,t__]]:=Mon[t];

Mon[Times[c_,t__]]:=Mon[c]*Mon[t];

Mon[Power[E,Plus[λ_?NumericQ,μ_]]]:=Power[E,μ];

Mon[c_?CoeffQ]:=1;

Mon[s_]:=s;

Coeff[t1_,t2___]:=Coeff[t1*t2];

Coeff[Times[c_,t__]]:=Coeff[c]*Coeff[t];

Coeff[(E^(Plus[λ_?NumericQ,μ_]))]:=(E^λ);

Coeff[s_?CoeffQ]:=s ;

Coeff[s_]:=1 ;

SplitPoly[c_?CoeffQ]:={{c,mma[1]}};

SplitPoly[Plus[t1_,t2___]]:=Join[SplitPoly[t1],Flatten[SplitPoly/@{t2},1]];

SplitPoly[0]:=™Tuple[];

SplitPoly[s_]:={{FullSimplify[Coeff[s]],mma[Mon[s]]}};

SplitPoly[t1_,t2___]:=SplitPoly/@{t1,t2};

MySplitPoly[A_]:=SplitPoly[Expand[A]]/.List->™Tuple;

FuncOrder[p_,p_]:=False;

FuncOrder[p_,q_]:=OrderedQ[{p,q}];

FuncQ[mma[t___]]:=True;

FuncQ[s_]:=False;

Clear[ToMma];

ToMma[⟨m_,r___⟩]:=Plus[ToMma[m],ToMma[r]];

ToMma[⟨c_,mma[m_]⟩]:=Times[c,m];

ToMma[t1_,t2__]:=Plus[ToMma[t1],ToMma[t2]];

ToMma[⟨⟩]:=0;

ToMma[]:=0;

ToMma[c_]:=c;

Clear[MmaPlus,MmaMinus,MmaTimes,MmaDif,MmaInt];

MmaPlus[p_,q_]:=MySplitPoly[ToMma[p]+ToMma[q]];

MmaMinus[p_]:=MySplitPoly[-ToMma[p]];

MmaMinus[p_,q_]:=MySplitPoly[ToMma[p]-ToMma[q]];

MmaTimes[p_,q_]:=MySplitPoly[ToMma[p]*ToMma[q]];

MmaDiff[p_]:=MySplitPoly[Expand[D[ToMma[p],x]]];

MmaInt[p_]:=MySplitPoly[Expand[TrigToExp[Integrate[ToMma[p],{x,0,x}]]]];

MmaSubs[p_,c_]:=Subs[ToMma[p],c];

Subs[p_,c_]:=p/.x->c;

MmaSimplify[p_]:=FullSimplify[p];

SetOptions[TransformResultFromMma,PlusNegativeAsMinus->True,TimesNegPowerAsFraction->False,PowerRationalAsRoot->False,NegPowerAsReciprocal->False];

TmaTRFM[p_]:=TransformResultFromMma[p/.{™Times->Times,™Plus->Plus,™Minus->Minus,™Power->Power}];

End[];

Built–in["FuncOrder",
func–less->FuncOrder]

Built–in["FuncQ",
is–func->FuncQ]

Built–in["MmaDiff",
mma–diff->MmaDiff]

Built–in["MmaInt",
mma–int->MmaInt]

Built–in["ToMma",
™toMma->ToMma]

Built–in["MmaPlus",
mma–plus->MmaPlus]

Built–in["MmaMinus",
mma–minus->MmaMinus]

Built–in["MmaTimes",
mma–times->MmaTimes]

Built–in["MmaSubs",
mma–subs->MmaSubs]

Built–in["MmaSimplify",
mma–simplify->MmaSimplify]

Built–in["TmaTRFM",
tma–trfm->TmaTRFM]

Built–in["TmaSplit",
tma–split->MySplitPoly]

mytimes

Clear[mytimes];

mytimes/:MakeBoxes[mytimes[x_],StandardForm]:=MakeBoxes[x,StandardForm];

mytimes/:MakeBoxes[mytimes[x_,y_],StandardForm]:=RowBox[{MakeBoxes[x,StandardForm],MakeBoxes[y,StandardForm]}];

mytimes/:MakeBoxes[mytimes[x_,y_,z__],StandardForm]:=RowBox[{MakeBoxes[x,StandardForm],MakeBoxes[y,StandardForm],MakeBoxes[mytimes[z],StandardForm]}];

mytimes[1,x__]:=x;

mytimes[-1,x__]:=-x;

mytimes[x__,1]:=x;

mytimes[x__,-1]:=-x;

Mathematica Functions

Definition["Mma Functions",any[K],
MmaFct[K]=Functor[E,any[c,d,l,p,q,ξ],
	({{𝕤=⟨⟩}, {({{(Underscript[∈, E])[p]⟺(∧{({{is–tuple[p]}, {(Underscript[∀, i=1,…,\[LeftBracketingBar]p\[RightBracketingBar]])(∧{({{is–tuple[(Subscript[p, i])]}, {\[LeftBracketingBar](Subscript[p, i])\[RightBracketingBar]=2}, {(Underscript[is–coeff, E])[(Subscript[((Subscript[p, i])), 1])]}, {(Underscript[is–bvec, E])[(Subscript[((Subscript[p, i])), 2])]}})})}, {(Underscript[∀, i=1,…,\[LeftBracketingBar]p\[RightBracketingBar]-1])func–less[(Subscript[((Subscript[p, i+1])), 2]),(Subscript[((Subscript[p, i])), 2])]}})})}, {(Underscript[0, E])=⟨⟩}, {(Underscript[1, E])=⟨⟨1,mma[1]⟩⟩}, {p(Underscript[>, E])q⇔func–less[q,p]}, {p(Underscript[+, E])q=mma–plus[p,q]}, {(Underscript[-, E])p=mma–minus[p]}, {p(Underscript[-, E])q=mma–minus[p,q]}, {c(Underscript[·, E])q=mma–times[c,q]}, {p(Underscript[*, E])q=mma–times[p,q]}, {(Underscript[is–bvec, E])[ξ]⇔is–func[ξ]}, {(Underscript[is–coeff, E])[c]⇔((Underscript[∈, K])[c]∧c≠(Underscript[0, K]))}, {(Underscript[is–scal, E])[⟨⟨c,mma[1]⟩⟩]⇔(Underscript[is–coeff, E])[c]}, {(Underscript[is–scal, E])[p]⇔False}, {(Underscript[to–scal, E])[⟨⟩]=(Underscript[0, K])}, {(Underscript[to–scal, E])[⟨⟨c,mma[1]⟩⟩]=c}, {(Underscript[eval, E])[p,d]=mma–subs[p,d]}, {(∂_E)p=mma–diff[p]}, {(∫_E)p=mma–int[p]}, {(Underscript[wronmin, E])[l]=tma–wronmin[l]}, {(Underscript[simplify, E])[p]=mma–simplify[p]}})}})]]

Integro-Differential Operators

Definition["Basis",any[ℱ],
Basis[ℱ]=Functor[B,any[ξ,η],
	({{𝕤=⟨⟩}, {({{(Underscript[∈, B])[⟨"⌈⌉",ξ⟩]⟺(Underscript[is–bvec, ℱ])[ξ]}, {⟨"⌈⌉",ξ⟩(Underscript[>, B])⟨"⌈⌉",η⟩⇔ξ(Underscript[>, ℱ])η}})}})]]

Definition["Basis for Characters",any[K],
CharBasis[K]=Functor[C,any[c,d],
	({{𝕤=⟨⟩}, {({{(Underscript[∈, C])[⟨"⌊⌋",c⟩]⟺((Underscript[∈, K])[c])}, {⟨"⌊⌋",c⟩(Underscript[>, C])⟨"⌊⌋",d⟩⇔c(Underscript[>, K])d}, {𝔼=⟨"⌊⌋",0⟩}})}})]]

Definition["Double Basis",any[B,C],
DoubleBasis[B,C]=Functor[D,any[d,e],
	({{𝕤=⟨⟩}, {({{(Underscript[∈, D])[d]⟺(((Underscript[∈, B])[d])∨((Underscript[∈, C])[d]))}, {⟨"⌈⌉",d⟩(Underscript[>, D])⟨"⌈⌉",e⟩⇔⟨"⌈⌉",d⟩(Underscript[>, B])⟨"⌈⌉",e⟩}, {⟨"⌊⌋",d⟩(Underscript[>, D])⟨"⌊⌋",e⟩⇔⟨"⌊⌋",d⟩(Underscript[>, C])⟨"⌊⌋",e⟩}, {⟨"⌈⌉",d⟩(Underscript[>, D])⟨"⌊⌋",e⟩⇔True}, {⟨"⌊⌋",d⟩(Underscript[>, D])⟨"⌈⌉",e⟩⇔False}})}})]]

Definition["⥛",any[l,L],
l⥛L=Functor[E,any[x,y],
	({{𝕤=⟨⟩}, {({{(Underscript[∈, E])[x]⟺((Underscript[∈, L])[x]∨(x=l))}, {l(Underscript[>, E])x⇔(l≠x)}, {y(Underscript[>, E])l⇔False}, {x(Underscript[>, E])y⇔x(Underscript[>, L])y}})}})]]

Definition["Green System",any[ℱ,K],
GreenSystem[ℱ,K]=where[𝒜=FreeIntDiffOp[ℱ,K],
Functor[Gr,any[c,f,g,φ,ψ,ξ,(OverBar[q]),(OverBar[u]),(OverBar[v]),A],
	({{𝕤=⟨⟩}, {({{(Underscript[rule, Gr])[⟨(OverBar[u]),⟨"⌈⌉",f⟩,⟨"⌈⌉",g⟩,(OverBar[v])⟩]=⟨⟨(OverBar[u])⟩,⟨⟨(Underscript[1, K]),⟨⟨"⌈⌉",f⟩,⟨"⌈⌉",g⟩⟩⟩⟩(Underscript[-, 𝒜])
(Underscript[fun–to–op, 𝒜])[(Underscript[ew, 𝒜])[f(Underscript[*, ℱ])g]],⟨(OverBar[v])⟩⟩}, {(Underscript[rule, Gr])[⟨(OverBar[u]),⟨"⌊⌋",φ⟩,⟨"⌊⌋",ψ⟩,(OverBar[v])⟩]=⟨⟨(OverBar[u])⟩,⟨⟨(Underscript[1, K]),⟨⟨"⌊⌋",φ⟩,⟨"⌊⌋",ψ⟩⟩⟩⟩(Underscript[-, 𝒜])
⟨⟨(Underscript[1, K]),⟨⟨"⌊⌋",ψ⟩⟩⟩⟩,⟨(OverBar[v])⟩⟩}, {(Underscript[rule, Gr])[⟨(OverBar[u]),⟨"⌊⌋",φ⟩,⟨"⌈⌉",f⟩,(OverBar[v])⟩]=⟨⟨(OverBar[u])⟩,⟨⟨(Underscript[1, K]),⟨⟨"⌊⌋",φ⟩,⟨"⌈⌉",f⟩⟩⟩⟩(Underscript[-, 𝒜])
(⟨⟨"⌊⌋",φ⟩⟩(Underscript[⋄, 𝒜])(Underscript[ew, 𝒜])[f])(Underscript[*, 𝒜])⟨⟨(Underscript[1, K]),⟨⟨"⌊⌋",φ⟩⟩⟩⟩,⟨(OverBar[v])⟩⟩}, {(Underscript[rule, Gr])[⟨(OverBar[u]),"∂",⟨"⌈⌉",f⟩,(OverBar[v])⟩]=⟨⟨(OverBar[u])⟩,(⟨⟨(Underscript[1, K]),⟨"∂",⟨"⌈⌉",f⟩⟩⟩⟩(Underscript[-, 𝒜])
⟨"∂"⟩(Underscript[⋄, 𝒜])(Underscript[ew, 𝒜])[f])(Underscript[-, 𝒜])⟨⟨(Underscript[1, K]),⟨⟨"⌈⌉",f⟩,"∂"⟩⟩⟩,⟨(OverBar[v])⟩⟩}, {(Underscript[rule, Gr])[⟨(OverBar[u]),"∂",⟨"⌊⌋",φ⟩,(OverBar[v])⟩]=⟨⟨(OverBar[u])⟩,⟨⟨(Underscript[1, K]),⟨"∂",⟨"⌊⌋",φ⟩⟩⟩⟩,⟨(OverBar[v])⟩⟩}, {(Underscript[rule, Gr])[⟨(OverBar[u]),"∂","∫",(OverBar[v])⟩]=⟨⟨(OverBar[u])⟩,⟨⟨(Underscript[1, K]),⟨"∂","∫"⟩⟩⟩(Underscript[-, 𝒜])(Underscript[1, 𝒜]),⟨(OverBar[v])⟩⟩}, {(Underscript[rule, Gr])[⟨(OverBar[u]),"∫",⟨"⌈⌉",f⟩,"∫",(OverBar[v])⟩]=
⟨⟨(OverBar[u])⟩,(⟨⟨(Underscript[1, K]),⟨"∫",⟨"⌈⌉",f⟩,"∫"⟩⟩⟩(Underscript[-, 𝒜])⟨"∫"⟩(Underscript[⋄, 𝒜])(Underscript[ew, 𝒜])[f](Underscript[*, 𝒜])⟨⟨(Underscript[1, K]),⟨"∫"⟩⟩⟩)(Underscript[+, 𝒜])⟨⟨(Underscript[1, K]),⟨"∫"⟩⟩⟩(Underscript[*, 𝒜])⟨"∫"⟩(Underscript[⋄, 𝒜])(Underscript[ew, 𝒜])[f],⟨(OverBar[v])⟩⟩}, {(Underscript[rule, Gr])[⟨(OverBar[u]),"∫",⟨"⌈⌉",f⟩,"∂",(OverBar[v])⟩]=
⟨⟨(OverBar[u])⟩,((⟨⟨(Underscript[1, K]),⟨"∫",⟨"⌈⌉",f⟩,"∂"⟩⟩⟩(Underscript[-, 𝒜])⟨⟨(Underscript[1, K]),⟨⟨"⌈⌉",f⟩⟩⟩⟩)(Underscript[+, 𝒜])⟨⟨(Underscript[1, K]),⟨"∫"⟩⟩⟩(Underscript[*, 𝒜])⟨"∂"⟩(Underscript[⋄, 𝒜])(Underscript[ew, 𝒜])[f])(Underscript[+, 𝒜])
(⟨𝔼⟩(Underscript[⋄, 𝒜])(Underscript[ew, 𝒜])[f])(Underscript[*, 𝒜])⟨⟨(Underscript[1, K]),⟨𝔼⟩⟩⟩,⟨(OverBar[v])⟩⟩}, {(Underscript[rule, Gr])[⟨(OverBar[u]),"∫",⟨"⌈⌉",f⟩,⟨"⌊⌋",φ⟩,(OverBar[v])⟩]=⟨⟨(OverBar[u])⟩,⟨⟨(Underscript[1, K]),⟨"∫",⟨"⌈⌉",f⟩,⟨"⌊⌋",φ⟩⟩⟩⟩(Underscript[-, 𝒜])
⟨"∫"⟩(Underscript[⋄, 𝒜])(Underscript[ew, 𝒜])[f](Underscript[*, 𝒜])⟨⟨(Underscript[1, K]),⟨⟨"⌊⌋",φ⟩⟩⟩⟩,⟨(OverBar[v])⟩⟩}, {(Underscript[rule, Gr])[⟨(OverBar[u]),"∫","∫",(OverBar[v])⟩]=⟨⟨(OverBar[u])⟩,(⟨⟨(Underscript[1, K]),⟨"∫","∫"⟩⟩⟩(Underscript[-, 𝒜])⟨"∫"⟩(Underscript[⋄, 𝒜])(Underscript[ew, 𝒜])[f](Underscript[*, 𝒜])⟨⟨(Underscript[1, K]),⟨"∫"⟩⟩⟩)(Underscript[+, 𝒜])⟨⟨(Underscript[1, K]),⟨"∫"⟩⟩⟩(Underscript[*, 𝒜])⟨"∫"⟩(Underscript[⋄, 𝒜])(Underscript[ew, 𝒜])[f],⟨(OverBar[v])⟩⟩}, {(Underscript[rule, Gr])[⟨(OverBar[u]),"∫","∂",(OverBar[v])⟩]=⟨⟨(OverBar[u])⟩,(⟨⟨(Underscript[1, K]),⟨"∫","∂"⟩⟩⟩(Underscript[-, 𝒜])(Underscript[1, 𝒜]))(Underscript[+, 𝒜])⟨⟨(Underscript[1, K]),⟨𝔼⟩⟩⟩,⟨(OverBar[v])⟩⟩}, {(Underscript[rule, Gr])[⟨(OverBar[u]),"∫",⟨"⌊⌋",φ⟩,(OverBar[v])⟩]=⟨⟨(OverBar[u])⟩,⟨⟨(Underscript[1, K]),⟨"∫",⟨"⌊⌋",φ⟩⟩⟩⟩(Underscript[-, 𝒜])(⟨"∫"⟩(Underscript[⋄, 𝒜])(Underscript[ew, 𝒜])[f])(Underscript[*, 𝒜])⟨⟨(Underscript[1, K]),⟨⟨"⌊⌋",φ⟩⟩⟩⟩,⟨(OverBar[v])⟩⟩}, {(Underscript[rule, Gr])[⟨(OverBar[u]),𝔼,⟨"⌊⌋",φ⟩,(OverBar[v])⟩]=⟨⟨(OverBar[u])⟩,⟨⟨(Underscript[1, K]),⟨𝔼,⟨"⌊⌋",φ⟩⟩⟩⟩(Underscript[-, 𝒜])⟨⟨(Underscript[1, K]),⟨⟨"⌊⌋",φ⟩⟩⟩⟩,⟨(OverBar[v])⟩⟩}, {(Underscript[rule, Gr])[⟨(OverBar[u]),⟨"⌊⌋",φ⟩,𝔼,(OverBar[v])⟩]=⟨⟨(OverBar[u])⟩,⟨⟨(Underscript[1, K]),⟨⟨"⌊⌋",φ⟩,𝔼⟩⟩⟩(Underscript[-, 𝒜])⟨⟨(Underscript[1, K]),⟨𝔼⟩⟩⟩,⟨(OverBar[v])⟩⟩}, {(Underscript[rule, Gr])[⟨(OverBar[u]),𝔼,⟨"⌈⌉",f⟩,(OverBar[v])⟩]=⟨⟨(OverBar[u])⟩,⟨⟨(Underscript[1, K]),⟨𝔼,⟨"⌈⌉",f⟩⟩⟩⟩(Underscript[-, 𝒜])(⟨𝔼⟩(Underscript[⋄, 𝒜])(Underscript[ew, 𝒜])[f])(Underscript[*, 𝒜])⟨⟨(Underscript[1, K]),⟨𝔼⟩⟩⟩,⟨(OverBar[v])⟩⟩}, {(Underscript[rule, Gr])[⟨(OverBar[u]),⟨"⌊⌋",0⟩,"∫",(OverBar[v])⟩]=⟨⟨(OverBar[u])⟩,⟨⟨(Underscript[1, K]),⟨𝔼,"∫"⟩⟩⟩,⟨(OverBar[v])⟩⟩}, {(Underscript[rule, Gr])[⟨(OverBar[u]),"∂",𝔼,(OverBar[v])⟩]=⟨⟨(OverBar[u])⟩,⟨⟨(Underscript[1, K]),⟨"∂",𝔼⟩⟩⟩,⟨(OverBar[v])⟩⟩}, {(Underscript[rule, Gr])[⟨(OverBar[u]),"∫",⟨"⌈⌉",f⟩,𝔼,(OverBar[v])⟩]=⟨⟨(OverBar[u])⟩,⟨⟨(Underscript[1, K]),⟨"∫",⟨"⌈⌉",f⟩,𝔼⟩⟩⟩(Underscript[-, 𝒜])⟨"∫"⟩(Underscript[⋄, 𝒜])(Underscript[ew, 𝒜])[f](Underscript[*, 𝒜])⟨⟨(Underscript[1, K]),⟨𝔼⟩⟩⟩,⟨(OverBar[v])⟩⟩}, {(Underscript[rule, Gr])[⟨(OverBar[u]),𝔼,𝔼,(OverBar[v])⟩]=⟨⟨(OverBar[u])⟩,⟨⟨(Underscript[1, K]),⟨𝔼,𝔼⟩⟩⟩(Underscript[-, 𝒜])⟨⟨(Underscript[1, K]),⟨𝔼⟩⟩⟩,⟨(OverBar[v])⟩⟩}, {(Underscript[rule, Gr])[⟨(OverBar[u]),"∫",⟨"⌈⌉",⟨⟨c,f⟩⟩⟩,(OverBar[v])⟩]={({{⟨⟨(OverBar[u])⟩,⟨⟨(Underscript[1, K]),⟨"∫",⟨"⌈⌉",⟨⟨c,f⟩⟩⟩⟩⟩⟩(Underscript[-, 𝒜])⟨⟨(Underscript[1, K]),⟨⟨"⌈⌉",⟨⟨c,f⟩⟩⟩,"∫"⟩⟩⟩,⟨(OverBar[v])⟩⟩, ⇐, (Underscript[is–const, ℱ])[c]}, {⟨⟨⟩,⟨⟩,⟨⟩⟩, ⇐, otherwise}})} }, {(Underscript[rule, Gr])[A]=⟨(Underscript[0, 𝒜]),(Underscript[0, 𝒜]),(Underscript[0, 𝒜])⟩}, {(Underscript[𝒢, Gr])[⟨⟨c,ξ⟩,(OverBar[q])⟩]=where[l=⟨⟨(Underscript[1, K]),(Subscript[((Underscript[rule, Gr])[ξ]), 1])⟩⟩,m=c(Underscript[·, 𝒜])(Subscript[((Underscript[rule, Gr])[ξ]), 2]),r=⟨⟨(Underscript[1, K]),(Subscript[((Underscript[rule, Gr])[ξ]), 3])⟩⟩,
{({{⟨l,m,r⟩, ⇐, m≠(Underscript[0, 𝒜])}, {⟨l,(Underscript[0, 𝒜]),r⟩, ⇐, otherwise}})}]}})}})]]]

Definition["Groebner Basis Normal Form",any[G,S],
GBNF[G,S]=Functor[C,any[a,b,c,(OverBar[a]),ℬ,F],
	({{𝕤=⟨⟩}, {({{(Underscript[NF, C])[a]=(Underscript[tred, G])[a,S]}, {(Underscript[0, C])=(Underscript[0, G])}, {(Underscript[1, C])=(Underscript[1, G])}, {C[+][(OverBar[a])]=G[+][(OverBar[a])]}, {(Underscript[-, C])a=(Underscript[-, G])a}, {a(Underscript[-, C])b=a(Underscript[-, G])b}, {C[*][(OverBar[a])]=G[*][(OverBar[a])]}, {c(Underscript[·, C])a=c(Underscript[·, G])a}, {(Underscript[ew, C])[a]=(Underscript[ew, G])[a]}, {(Underscript[EvalMat, C])[ℬ,F]=(Underscript[EvalMat, G])[ℬ,F]}})}})
]]

Definition["Quotient Algebra",any[G],
QuotAlg[G]=Functor[Q,any[a,b,c,(OverBar[a]),ℬ,F],
	({{𝕤=⟨⟩}, {({{(Underscript[∈, Q])[a]⟺((Underscript[NF, G])[a]=a)}, {(Underscript[0, Q])=(Underscript[0, G])}, {(Underscript[1, Q])=(Underscript[1, G])}, {Q[+][(OverBar[a])]=(Underscript[NF, G])[G[+][(OverBar[a])]]}, {(Underscript[-, Q])a=(Underscript[NF, G])[(Underscript[-, G])a]}, {a(Underscript[-, Q])b=(Underscript[NF, G])[a(Underscript[-, G])b]}, {Q[*][(OverBar[a])]=(Underscript[NF, G])[G[*][(OverBar[a])]]}, {c(Underscript[·, Q])a=(Underscript[NF, G])[c(Underscript[·, G])a]}, {(Underscript[ew, Q])[a]=(Underscript[ew, G])[a]}, {(Underscript[EvalMat, Q])[ℬ,F]=(Underscript[EvalMat, G])[ℬ,F]}})}})
]]

Definition["FreeIntDiffOp",any[ℱ,K],
FreeIntDiffOp[ℱ,K]=where[ℳ=MonoidAlgebra[K,DegWords["∂"⥛("∫"⥛(DoubleBasis[Basis[ℱ],CharBasis[K]]))]],
Functor[𝒜,any[b,c,d,f,g,α,β,ξ,w,(OverBar[f]),(OverBar[g]),(OverBar[m]),(OverBar[w]),ℬ,F,J],
	({{𝕤=⟨⟩}, {({{(Underscript[∈, 𝒜])[f]⟺(Underscript[∈, ℳ])[f]}, {(Underscript[0, 𝒜])=(Underscript[0, ℳ])}, {𝒜[+][(OverBar[f])]=ℳ[+][(OverBar[f])]}, {(Underscript[-, 𝒜])f=(Underscript[-, ℳ])f}, {f(Underscript[-, 𝒜])g=f(Underscript[-, ℳ])g}, {c(Underscript[·, 𝒜])f=c(Underscript[·, ℳ])f}, {𝒜[*][(OverBar[f])]=ℳ[*][(OverBar[f])]}, {(Underscript[is–bvec, 𝒜])[b]⇔(Underscript[is–bvec, ℳ])[b]}, {(Underscript[is–scal, 𝒜])[⟨⟨c,⟨⟩⟩⟩]⇔((Underscript[∈, K])[c])}, {(Underscript[is–scal, 𝒜])[b]⇔False}, {(Underscript[lrdm, 𝒜])[f,g]=(Underscript[lrdm, ℳ])[f,g]}, {(Underscript[rrdm, 𝒜])[f,g]=(Underscript[rrdm, ℳ])[f,g]}, {f(Underscript[>, 𝒜])g⇔f(Underscript[>, ℳ])g}, {(Underscript[lcm, 𝒜])[f,g]=(Underscript[lcm, DegWords["∂"⥛("∫"⥛(DoubleBasis[Basis[ℱ],CharBasis[K]]))]])[f,g]}, {(Underscript[lcrd, 𝒜])[⟨⟨c,f⟩,(OverBar[f])⟩,⟨⟨d,g⟩,(OverBar[g])⟩](* least common reducible *)=⟨⟨(Underscript[lcrd, K])[c,d],(Underscript[lcm, 𝒜])[f,g]⟩⟩}, {(Underscript[1, 𝒜])=⟨⟨(Underscript[1, K]),⟨⟩⟩⟩}, {(Underscript[ew, 𝒜])[⟨⟩]=⟨⟩}, {(Underscript[ew, 𝒜])[⟨⟨⟨⟩,g⟩⟩]=⟨⟩}, {(Underscript[ew, 𝒜])[⟨⟨⟨⟨⟨⟨c,w⟩⟩,⟨⟨α⟩,β,J⟩⟩,(OverBar[w])⟩,g⟩,(OverBar[m])⟩]=(α(Underscript[*, K])c)(Underscript[·, ℳ])(Underscript[ew, ℳ])[⟨⟨⟨⟨⟨⟨1,w⟩⟩,⟨⟨1⟩,β,J⟩⟩⟩,g⟩⟩](Underscript[+, MonoidAlgebra[K,ℱ]])(Underscript[ew, 𝒜])[⟨⟨⟨(OverBar[w])⟩,g⟩⟩](Underscript[+, MonoidAlgebra[K,ℱ]])(Underscript[ew, 𝒜])[⟨(OverBar[m])⟩]}, {(Underscript[ew, 𝒜])[⟨⟨⟨⟨⟨⟨c,w⟩⟩,ξ⟩,(OverBar[w])⟩,g⟩,(OverBar[m])⟩]=c(Underscript[·, ℳ])(Underscript[ew, ℳ])[⟨⟨⟨⟨⟨⟨1,w⟩⟩,ξ⟩⟩,g⟩⟩](Underscript[+, MonoidAlgebra[K,ℱ]])(Underscript[ew, 𝒜])[⟨⟨⟨(OverBar[w])⟩,g⟩⟩](Underscript[+, MonoidAlgebra[K,ℱ]])(Underscript[ew, 𝒜])[⟨(OverBar[m])⟩]}, {(Underscript[to–scal, 𝒜])[⟨⟩]=0}, {(Underscript[to–scal, 𝒜])[⟨⟨c,(Underscript[⬚, DegWords["∂"⥛("∫"⥛(DoubleBasis[Basis[ℱ],CharBasis[K]]))]])⟩⟩]=c}, {(Underscript[op–to–fun, 𝒜])[⟨⟩](* integro-diff operators to functions *)=⟨⟩}, {(Underscript[op–to–fun, 𝒜])[⟨⟨c,⟨⟩⟩⟩]=c(Underscript[·, ℱ])(Underscript[1, ℱ])}, {(Underscript[op–to–fun, 𝒜])[⟨⟨c,⟨⟨"⌈⌉",ξ⟩⟩⟩,(OverBar[m])⟩]=⟨c,ξ⟩⌣(Underscript[op–to–fun, 𝒜])[⟨(OverBar[m])⟩]}, {(Underscript[fun–to–op, 𝒜])[⟨⟩](* functions to integro-diff operators *)=⟨⟩}, {(Underscript[fun–to–op, 𝒜])[⟨⟨c,ξ⟩,(OverBar[m])⟩]={({{⟨⟨(Underscript[to–scal, ℱ])[⟨⟨c,ξ⟩⟩],⟨⟩⟩⟩(Underscript[+, ℳ])(Underscript[fun–to–op, 𝒜])[⟨(OverBar[m])⟩], ⇐, (Underscript[is–scal, 𝒜])[⟨⟨c,ξ⟩⟩]}, {⟨⟨c,⟨⟨"⌈⌉",ξ⟩⟩⟩⟩(Underscript[+, ℳ])(Underscript[fun–to–op, 𝒜])[⟨(OverBar[m])⟩], ⇐, otherwise}})}}, {⟨⟩(Underscript[⋄, 𝒜])f(* the action of int-diff word on function *)=(Underscript[fun–to–op, 𝒜])[f]}, {⟨(OverBar[w]),"∂"⟩(Underscript[⋄, 𝒜])⟨⟨c,f⟩⟩=c(Underscript[·, 𝒜])⟨(OverBar[w])⟩(Underscript[⋄, 𝒜])(Underscript[ew, 𝒜])[(∂_ℱ)f]}, {⟨(OverBar[w]),"∫"⟩(Underscript[⋄, 𝒜])⟨⟨c,f⟩⟩=c(Underscript[·, 𝒜])⟨(OverBar[w])⟩(Underscript[⋄, 𝒜])(Underscript[ew, 𝒜])[(∫_ℱ)f]}, {⟨(OverBar[w]),⟨"⌊⌋",d⟩⟩(Underscript[⋄, 𝒜])⟨⟨c,f⟩⟩=c(Underscript[·, 𝒜])⟨(OverBar[w])⟩(Underscript[⋄, 𝒜])(Underscript[ew, 𝒜])[(Underscript[eval, ℱ])[f,d]]}, {⟨(OverBar[w]),⟨"⌈⌉",b⟩⟩(Underscript[⋄, 𝒜])⟨⟨c,f⟩⟩=c(Underscript[·, 𝒜])⟨(OverBar[w])⟩(Underscript[⋄, 𝒜])(Underscript[ew, 𝒜])[b(Underscript[*, ℱ])f]}, {⟨⟩(Underscript[⊙, 𝒜])f(* the action of int-diff op on function *)=⟨⟩}, {⟨⟨c,ξ⟩,(OverBar[m])⟩(Underscript[⊙, 𝒜])f=c(Underscript[·, 𝒜])ξ(Underscript[⋄, 𝒜])f(Underscript[+, 𝒜])⟨(OverBar[m])⟩(Underscript[⊙, 𝒜])f}, {(Underscript[EvalMat, 𝒜])[ℬ,F]=⟨⟨(Underscript[to–scal, 𝒜])[(Subscript[ℬ, i])(Underscript[⊙, 𝒜])(Underscript[op–to–fun, 𝒜])[(Subscript[F, j])]](Underscript[|, j=1,…,\[LeftBracketingBar]F\[RightBracketingBar]])⟩(Underscript[|, i=1,…,\[LeftBracketingBar]ℬ\[RightBracketingBar]])⟩}})}})]]]

Definition["PrettyPrinting for IntDiffPol",any[ℱ,K],
PrettyPrintingIDP[ℱ,K]=Functor[P,any[b,c,m,n,p,r,w,α,β,λ,γ,η,J,(OverBar[η]),(OverBar[ξ]),(OverBar[J])],
	({{𝕤=⟨⟩}, {({{(Underscript[PrettyPrintW, P])[⟨⟩]=""}, {(Underscript[PrettyPrintW, P])[⟨λ,η,(OverBar[η])⟩]={({{™Times[(λ^2),(Underscript[PrettyPrintW, P])[⟨(OverBar[η])⟩]], ⇐, λ=η}, {mytimes[(Underscript[PrettyPrintL, P])[λ],(Underscript[PrettyPrintW, P])[⟨η,(OverBar[η])⟩]], ⇐, otherwise}})} }, {(Underscript[PrettyPrintW, P])[⟨η⟩]=(Underscript[PrettyPrintL, P])[η]}, {(Underscript[PrettyPrintL, P])[⟨"⌈⌉",⟨⟨⟩,⟨⟩,J⟩⟩]=(Underscript[PrettyPrintJ, P])[J]}, {(Underscript[PrettyPrintL, P])[⟨"⌈⌉",⟨⟨⟩,β,J⟩⟩]=mytimes[™Power[u,β],(Underscript[PrettyPrintJ, P])[J]]}, {(Underscript[PrettyPrintL, P])[⟨"⌈⌉",⟨α,⟨⟩,J⟩⟩]=mytimes[™Power[u[0],α],(Underscript[PrettyPrintJ, P])[J]]}, {(Underscript[PrettyPrintL, P])[⟨"⌈⌉",⟨α,β,J⟩⟩]=mytimes[™Power[u[0],α],™Power[u,β],(Underscript[PrettyPrintJ, P])[J]]}, {(Underscript[PrettyPrintJ, P])[⟨⟩]=""}, {(Underscript[PrettyPrintJ, P])[⟨⟨b,γ⟩,(OverBar[J])⟩]=mytimes[™Times["∫",(Underscript[PrettyPrint, ℱ])[b]],™Power[u,γ],(Underscript[PrettyPrintJ, P])[⟨(OverBar[J])⟩]]}, {(Underscript[PrettyPrintL, P])["∂"]="∂"}, {(Underscript[PrettyPrintL, P])["∫"]="∫"}, {(Underscript[PrettyPrintL, P])[⟨⟩]=""}, {(Underscript[PrettyPrintL, P])[η]=η}, {(Underscript[PrettyPrintM, P])[⟨c,w⟩]=™Times[(Underscript[PrettyPrint, K])[c],(Underscript[PrettyPrintW, P])[w]]}, {(Underscript[PrettyPrint, P])[⟨⟨⟨c,η⟩,(OverBar[ξ])⟩,(OverBar[η])⟩]=⟨(Underscript[PrettyPrint, P])[(Subscript[⟨⟨⟨c,η⟩,(OverBar[ξ])⟩,(OverBar[η])⟩, i])](Underscript[|, i=1,…,\[LeftBracketingBar]⟨⟨⟨c,η⟩,(OverBar[ξ])⟩,(OverBar[η])⟩\[RightBracketingBar]])⟩}, {(Underscript[PrettyPrint, P])[p]=™Plus[(Underscript[PrettyPrintM, P])[(Subscript[p, i])](Underscript[|, i=1,…,\[LeftBracketingBar]p\[RightBracketingBar]])]}, {(Underscript[PrettyPrint, P])[⟨m⟩]=(Underscript[PrettyPrintM, P])[m]}, {(Underscript[PrettyPrint, P])[⟨⟩]=0}})}})]]

Definition["IntDiffOp",any[ℱ,K],
IntDiffOp[ℱ,K]=where[𝒜=FreeIntDiffOp[ℱ,K],
QuotAlg[GBNF[GB[𝒜],(Underscript[𝒢, GreenSystem[ℱ,K]])]]]
]

Integro-Differential Polynomials

Definition["Differential Polynomials",any[ℱ,K],
DiffPolys[ℱ,K]=where[M=MonoidAlgebra[ℱ,TuplesMonoid[ℕ]],
Functor[V,any[c,d,f,k,m,n,w,x,y,λ,ξ,η,A,(OverBar[η]),(OverBar[m]),(OverBar[x]),(OverBar[y])],
	({{𝕤=⟨⟩}, {({{(Underscript[∈, V])[x]⟺((Underscript[∈, M])[x])}, {(Underscript[is–bvec, V])[ξ]⇔(Underscript[is–bvec, M])[ξ]}, {(Underscript[is–coeff, V])[c]⇔(Underscript[is–coeff, M])[c]}, {(Underscript[bvec, V])[ξ]=(Underscript[bvec, M])[ξ]}, {(Underscript[to–exp, V])[⟨⟩]=⟨⟩}, {(Underscript[to–exp, V])[⟨⟨c,ξ⟩,(OverBar[x])⟩]={({{⟨⟨c(Underscript[·, ℱ])(Underscript[1, ℱ]),ξ⟩⟩(Underscript[+, V])(Underscript[to–exp, V])[⟨(OverBar[x])⟩], ⇐, (Underscript[is–coeff, V])[⟨⟨c,⟨0,0⟩⟩⟩]}, {⟨⟨⟨⟨c,⟨0,0⟩⟩⟩(Underscript[·, ℱ])(Underscript[1, ℱ]),ξ⟩⟩(Underscript[+, V])(Underscript[to–exp, V])[⟨(OverBar[x])⟩], ⇐, otherwise}})}}, {(Underscript[0, V])=(Underscript[0, M])}, {(Underscript[1, V])=⟨⟨(Underscript[1, ℱ]),⟨⟩⟩⟩}, {x(Underscript[+, V])y=x(Underscript[+, M])y}, {V[+][x,(OverBar[x])]=x(Underscript[+, M])M[+][(OverBar[x])]}, {(Underscript[-, V])x=(Underscript[-, M])x}, {x(Underscript[-, V])y=x(Underscript[-, M])y}, {c(Underscript[·, V])y(* scalar multiplication *)=c(Underscript[·, M])y}, {x(Underscript[*, V])y=x(Underscript[*, M])y}, {(Underscript[D, V])[⟨⟩]=⟨⟩}, {(Underscript[D, V])[⟨(OverBar[m]),0⟩]=(Underscript[D, V])[⟨(OverBar[m])⟩]}, {(Underscript[D, V])[⟨k⟩]=⟨⟨k,⟨k-1,1⟩⟩⟩}, {(Underscript[D, V])[⟨(OverBar[m]),n⟩]=(Underscript[D, V])[⟨(OverBar[m])⟩](Underscript[*, MonoidAlgebra[K,TuplesMonoid[ℕ]]])⟨⟨(Underscript[1, K]),⟨0(Underscript[|, i=1,…,\[LeftBracketingBar]⟨(OverBar[m])⟩\[RightBracketingBar]]),n⟩⟩⟩(Underscript[+, MonoidAlgebra[K,TuplesMonoid[ℕ]]])⟨⟨n,⟨(OverBar[m]),n-1,1⟩⟩⟩}, {(∂_V)⟨⟩=⟨⟩}, {(∂_V)⟨⟨c,ξ⟩,(OverBar[x])⟩={({{(∂_ℱ)c(Underscript[·, V])⟨⟨(Underscript[1, ℱ]),ξ⟩⟩(Underscript[+, V])c(Underscript[·, V])(Underscript[to–exp, V])[(Underscript[D, V])[ξ]](Underscript[+, V])(∂_V)⟨(OverBar[x])⟩, ⇐, (∂_ℱ)c≠(Underscript[0, ℱ])}, {c(Underscript[·, V])(Underscript[to–exp, V])[(Underscript[D, V])[ξ]](Underscript[+, V])(∂_V)⟨(OverBar[x])⟩, ⇐, otherwise}})}}, {(Underscript[PrettyPrint, V])[x]=™Plus[(Underscript[PrettyPrintM, V])[(Subscript[x, i])](Underscript[|, i=1,…,\[LeftBracketingBar]x\[RightBracketingBar]])]}, {(Underscript[PrettyPrint, V])[⟨m⟩]=(Underscript[PrettyPrintM, V])[m]}, {(Underscript[PrettyPrint, V])[⟨⟩]=0}, {(Underscript[PrettyPrintM, V])[⟨c,w⟩]=tma–trfm[™Times[(Underscript[PrettyPrintC, V])[c],(Underscript[PrettyPrintW, V])[w]]]}, {(Underscript[PrettyPrintC, V])[c]=(Underscript[PrettyPrint, ℱ])[c]}, {(Underscript[PrettyPrintW, V])[⟨⟩]=1}, {(Underscript[PrettyPrintW, V])[⟨η,(OverBar[η])⟩]=™Power[u,⟨η,(OverBar[η])⟩]}})}})]]]

Definition["Term Monoid for IDP",any[N,ℱ],
TermMonoid[ℱ,N]=CartesianProduct[TuplesMonoid[N],TuplesMonoid[N],TuplesMonoid[ℱ\[Cross]TuplesMonoid[N]]]]

Definition["Integro-Differential Polys",any[K,ℱ],
IntDiffPolys[ℱ,K]=where[M=FreeModule[ℱ,TermMonoid[ℱ,ℕ]],
Functor[V,any[a,b,c,f,g,j,k,p,w,α,β,γ,η,(OverBar[η]),A,J,(OverTilde[b]),(OverTilde[α]),(OverTilde[β]),(OverTilde[γ]),(OverTilde[J]),(OverBar[a]),(OverBar[α]),(OverBar[γ]),(OverBar[J]),(OverBar[(OverTilde[J])])],
	({{𝕤=⟨⟩}, {({{(Underscript[∈, V])[⟨⟨f,J⟩,(OverBar[J])⟩]⇔ ((Underscript[∈, M])[⟨⟨f,J⟩,(OverBar[J])⟩])}, {f(Underscript[>, V])g⇔f(Underscript[>, M])g}, {(Underscript[is–bvec, V])[⟨⟨c,f⟩⟩]⇔((Underscript[∈, ℱ])[c]∧(Underscript[is–bvec, M])[f])}, {(Underscript[is–coeff, V])[c]⇔(Underscript[is–coeff, M])[c]}, {(Underscript[ew, V])[f]=(Underscript[bvec, M])[f]}, {(Underscript[lcrd, V])[⟨⟨a,J⟩⟩,⟨⟨b,(OverTilde[J])⟩⟩]=⟨⟨(Underscript[lcrd, ℱ])[a,b],(Underscript[lcm, TermMonoid[ℱ,ℕ]])[J,(OverTilde[J])]⟩⟩}, {(Underscript[is–const, V])[⟨⟨c,⟨α,⟨⟩,J⟩⟩⟩]⇔(α≠(Underscript[⬚, TuplesMonoid[N]])∨J≠(Underscript[⬚, TuplesMonoid[ℱ\[Cross]TuplesMonoid[N]]]))}, {(Underscript[is–const, V])[A]⇔False}, {(Underscript[is–scal, V])[⟨⟨c,(Underscript[⬚, TermMonoid[ℱ,ℕ]])⟩⟩]⇔(Underscript[is–coeff, V])[c]}, {(Underscript[is–scal, V])[⟨⟨c,⟨⟩⟩⟩]⇔(Underscript[is–coeff, V])[c]}, {(Underscript[is–scal, V])[a]⇔False}, {(Underscript[to–scal, V])[⟨⟩]=(Underscript[0, K])}, {(Underscript[to–scal, V])[⟨⟨c,(Underscript[⬚, TermMonoid[ℱ,ℕ]])⟩⟩]=c}, {(Underscript[to–scal, V])[⟨⟨c,⟨⟩⟩⟩]=c}, {(Underscript[0, V])=⟨⟩}, {(Underscript[1, V])=⟨⟨(Underscript[1, ℱ]),⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩}, {(Underscript[-, V])f=(Underscript[-, M])f}, {f(Underscript[+, V])g=f(Underscript[+, M])g}, {f(Underscript[-, V])g=f(Underscript[-, M])g}, {⟨⟩(Underscript[·, V])f=⟨⟩}, {c(Underscript[·, V])f=c(Underscript[·, M])f}, {(Underscript[eval, V])[⟨⟨f,⟨α,β,⟨⟩⟩⟩⟩,0]={({{⟨⟨(Underscript[eval, ℱ])[f,0](Underscript[·, ℱ])(Underscript[1, ℱ]),⟨α(Underscript[*, TuplesMonoid[ℕ]])β,⟨⟩,⟨⟩⟩⟩⟩, ⇐, (Underscript[is–coeff, ℱ])[(Underscript[eval, ℱ])[f,0]]}, {⟨⟨(Underscript[eval, ℱ])[f,0],⟨α(Underscript[*, TuplesMonoid[ℕ]])β,⟨⟩,⟨⟩⟩⟩⟩, ⇐, (Underscript[eval, ℱ])[f,0]≠(Underscript[0, K])}, {⟨⟩, ⇐, otherwise}})}}, {(Underscript[eval, V])[⟨⟨f,⟨α,β,J⟩⟩⟩,0]=⟨⟩}, {(Underscript[to–idp, V])[⟨⟩]=⟨⟩}, {(Underscript[to–idp, V])[⟨⟨c,J⟩,(OverBar[J])⟩]=⟨⟨c,⟨⟨⟩,⟨⟩,J⟩⟩⟩(Underscript[+, V])(Underscript[to–idp, V])[⟨(OverBar[J])⟩]}, {(Underscript[dp–to–idp, V])[⟨⟩]=⟨⟩}, {(Underscript[dp–to–idp, V])[⟨⟨b,γ⟩,(OverBar[J])⟩]=⟨⟨b,⟨⟨⟩,γ,⟨⟩⟩⟩⟩(Underscript[+, V])(Underscript[dp–to–idp, V])[⟨(OverBar[J])⟩]}, {(Underscript[ls–to–idp, V])[⟨⟩]=⟨⟩}, {(Underscript[ls–to–idp, V])[⟨J,(OverBar[J])⟩]=(Underscript[to–idp, V])[J](Underscript[+, V])(Underscript[ls–to–idp, V])[⟨(OverBar[J])⟩]}, {(Underscript[exp, V])[⟨⟩]=⟨⟩}, {(Underscript[exp, V])[a]=⟨⟨(Underscript[1, ℱ]),a⟩⟩}, {a(Underscript[\[Cross], V])⟨⟩=⟨⟩}, {a(Underscript[\[Cross], V])⟨⟨c,⟨α,(OverBar[α])⟩⟩,(OverBar[a])⟩=⟨⟨c,⟨a,α,(OverBar[α])⟩⟩⟩(Underscript[+, FreeModule[ℱ,FreeModule[ℱ,TuplesMonoid[ℕ]]]])a(Underscript[\[Cross], V])⟨(OverBar[a])⟩}, {a(Underscript[∘, V])⟨⟩=⟨⟩}, {⟨a⟩(Underscript[∘, V])⟨⟨c,⟨α,β,⟨⟩⟩⟩,(OverBar[a])⟩=⟨⟨c,⟨α,β,⟨a⟩⟩⟩⟩(Underscript[+, V])⟨a⟩(Underscript[∘, V])⟨(OverBar[a])⟩}, {⟨a⟩(Underscript[∘, V])⟨⟨c,⟨α,β,⟨⟨b,γ⟩,(OverBar[J])⟩⟩⟩,(OverBar[a])⟩=⟨⟨c,⟨α,β,⟨a,⟨b,γ⟩,(OverBar[J])⟩⟩⟩⟩(Underscript[+, V])⟨a⟩(Underscript[∘, V])⟨(OverBar[a])⟩}, {⟨⟩(Underscript[⋄, V])α=(Underscript[exp, V])[α]}, {a(Underscript[⋄, V])⟨⟩=(Underscript[exp, V])[a]}, {⟨a,(OverBar[J])⟩(Underscript[⋄, V])⟨α,(OverBar[(OverTilde[J])])⟩(* shuffle product *)=a(Underscript[\[Cross], V])(⟨(OverBar[J])⟩(Underscript[⋄, V])⟨α,(OverBar[(OverTilde[J])])⟩)(Underscript[+, FreeModule[ℱ,FreeModule[ℱ,TuplesMonoid[ℕ]]]])α(Underscript[\[Cross], V])(⟨(OverBar[(OverTilde[J])])⟩(Underscript[⋄, V])⟨a,(OverBar[J])⟩)}, {⟨⟩(Underscript[*, V])J=⟨⟩}, {J(Underscript[*, V])⟨⟩=⟨⟩}, {⟨⟨b,⟨α,β,⟨⟩⟩⟩,(OverBar[J])⟩(Underscript[*, V])⟨⟨(OverTilde[b]),⟨(OverTilde[α]),(OverTilde[β]),(OverTilde[J])⟩⟩,(OverBar[(OverTilde[J])])⟩=(⟨⟨b(Underscript[*, ℱ])(OverTilde[b]),⟨α(Underscript[*, TuplesMonoid[ℕ]])(OverTilde[α]),β(Underscript[*, TuplesMonoid[ℕ]])(OverTilde[β]),(OverTilde[J])⟩⟩⟩(Underscript[+, V])
⟨⟨b,⟨α,β,⟨⟩⟩⟩⟩(Underscript[*, V])⟨(OverBar[(OverTilde[J])])⟩)(Underscript[+, V])⟨(OverBar[J])⟩(Underscript[*, V])⟨⟨(OverTilde[b]),⟨(OverTilde[α]),(OverTilde[β]),(OverTilde[J])⟩⟩,(OverBar[(OverTilde[J])])⟩}, {⟨⟨b,⟨α,β,J⟩⟩,(OverBar[J])⟩(Underscript[*, V])⟨⟨(OverTilde[b]),⟨(OverTilde[α]),(OverTilde[β]),(OverTilde[J])⟩⟩,(OverBar[(OverTilde[J])])⟩=((⟨⟨b,⟨α,β,⟨⟩⟩⟩⟩(Underscript[*, V])⟨⟨(OverTilde[b]),⟨(OverTilde[α]),(OverTilde[β]),⟨⟩⟩⟩⟩)(Underscript[*, V])(Underscript[to–idp, V])[J(Underscript[⋄, V])(OverTilde[J])](Underscript[+, V])
⟨⟨b,⟨α,β,J⟩⟩⟩(Underscript[*, V])⟨(OverBar[(OverTilde[J])])⟩)(Underscript[+, V])⟨(OverBar[J])⟩(Underscript[*, V])⟨⟨(OverTilde[b]),⟨(OverTilde[α]),(OverTilde[β]),(OverTilde[J])⟩⟩,(OverBar[(OverTilde[J])])⟩}, {(Underscript[exp–basis, V])[⟨⟩]=⟨⟩}, {(Underscript[exp–basis, V])[⟨⟨c,⟨α,β,⟨⟩⟩⟩,(OverBar[J])⟩]=⟨⟨c,⟨α,β,⟨⟩⟩⟩⟩(Underscript[+, V])(Underscript[exp–basis, V])[⟨(OverBar[J])⟩]}, {(Underscript[exp–basis, V])[⟨⟨c,⟨α,β,⟨⟨⟨⟩,γ⟩,(OverBar[J])⟩⟩⟩⟩]=⟨⟩}, {(Underscript[exp–basis, V])[⟨⟨c,⟨α,β,⟨⟨f,⟨0,1⟩⟩,(OverBar[J])⟩⟩⟩⟩]=
c(Underscript[·, V])(Underscript[exp–basis, V])[⟨⟨(Underscript[1, ℱ]),⟨α,β,⟨(OverBar[J])⟩⟩⟩⟩(Underscript[*, V])((⟨⟨f,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩(Underscript[-, V])(∫_V)⟨⟨(∂_ℱ)f,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩)(Underscript[-, V])
(Underscript[eval, V])[⟨⟨f,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩,0])]}, {(Underscript[exp–basis, V])[⟨⟨c,⟨α,β,⟨⟨f,⟨(OverBar[α]),k,1⟩⟩,(OverBar[J])⟩⟩⟩⟩]=
(1(Underscript[/, K])(k+1)(Underscript[·, ℱ])c)(Underscript[·, V])(Underscript[exp–basis, V])[⟨⟨(Underscript[1, ℱ]),⟨α,β,⟨(OverBar[J])⟩⟩⟩⟩(Underscript[*, V])((⟨⟨f,⟨⟨⟩,⟨(OverBar[α]),k+1⟩,⟨⟩⟩⟩⟩(Underscript[-, V])(∫_V)((∂_V)⟨⟨(Underscript[1, ℱ]),⟨⟨⟩,⟨(OverBar[α])⟩,⟨⟩⟩⟩⟩(Underscript[*, V])⟨⟨(Underscript[1, ℱ]),⟨⟨⟩,⟨0(Underscript[|, i=0,…,\[LeftBracketingBar]⟨(OverBar[α])⟩\[RightBracketingBar]-1]),k+1⟩,⟨⟩⟩⟩⟩))
(Underscript[-, V])(Underscript[eval, V])[⟨⟨(Underscript[1, ℱ]),⟨⟨⟩,⟨(OverBar[α]),k+1⟩,⟨⟩⟩⟩⟩,0])]}, {(Underscript[exp–basis, V])[⟨⟨c,⟨α,β,⟨⟨⟨⟨b,a⟩⟩,γ⟩⟩⟩⟩⟩]=⟨⟨c(Underscript[·, ℱ])b,⟨α,β,⟨⟨⟨⟨(Underscript[1, K]),a⟩⟩,γ⟩⟩⟩⟩⟩}, {(Underscript[exp–basis, V])[⟨⟨c,⟨α,β,⟨⟨⟨⟨b,a⟩,(OverBar[a])⟩,γ⟩,(OverBar[J])⟩⟩⟩,(OverBar[(OverTilde[J])])⟩]=(⟨⟨⟨⟨(Underscript[1, K]),a⟩⟩,γ⟩⟩(Underscript[∘, V])(Underscript[exp–basis, V])[⟨⟨c(Underscript[·, ℱ])b,⟨α,β,⟨(OverBar[J])⟩⟩⟩⟩](Underscript[+, V])
(Underscript[exp–basis, V])[⟨⟨c,⟨α,β,⟨⟨⟨(OverBar[a])⟩,γ⟩,(OverBar[J])⟩⟩⟩⟩])(Underscript[+, V])(Underscript[exp–basis, V])[⟨(OverBar[(OverTilde[J])])⟩]}, {(∂_V)⟨⟩=⟨⟩}, {(∂_V)⟨f,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩={({{⟨⟩, ⇐, (Underscript[is–scal, ℱ])[f]}, {(∂_ℱ)f(Underscript[·, V])(Underscript[1, V]), ⇐, otherwise}})}}, {(∂_V)⟨f,⟨α,β,⟨⟩⟩⟩={({{(Underscript[dp–to–idp, V])[(∂_(DiffPolys[ℱ,K]))⟨⟨(Underscript[1, ℱ]),β⟩⟩](Underscript[*, V])⟨⟨f,⟨α,⟨⟩,⟨⟩⟩⟩⟩, ⇐, (Underscript[is–scal, ℱ])[f]}, {(∂_ℱ)f(Underscript[·, V])⟨⟨(Underscript[1, ℱ]),⟨α,β,⟨⟩⟩⟩⟩(Underscript[+, V])(Underscript[dp–to–idp, V])[(∂_(DiffPolys[ℱ,K]))⟨⟨(Underscript[1, ℱ]),β⟩⟩](Underscript[*, V])⟨⟨f,⟨α,⟨⟩,⟨⟩⟩⟩⟩, ⇐, otherwise}})}}, {(∂_V)⟨f,⟨α,β,⟨⟨b,γ⟩,(OverBar[J])⟩⟩⟩={({{(Underscript[dp–to–idp, V])[(∂_(DiffPolys[ℱ,K]))⟨⟨(Underscript[1, ℱ]),β⟩⟩](Underscript[*, V])⟨⟨f,⟨α,⟨⟩,⟨⟨b,γ⟩,(OverBar[J])⟩⟩⟩⟩(Underscript[+, V])
⟨⟨f(Underscript[*, ℱ])b,⟨α,β(Underscript[*, TuplesMonoid[ℕ]])γ,⟨(OverBar[J])⟩⟩⟩⟩, ⇐, (Underscript[is–scal, ℱ])[f]}, {(⟨⟨(∂_ℱ)f,⟨α,β,⟨⟨b,γ⟩,(OverBar[J])⟩⟩⟩⟩(Underscript[+, V])(Underscript[dp–to–idp, V])[(∂_(DiffPolys[ℱ,K]))⟨⟨(Underscript[1, ℱ]),β⟩⟩](Underscript[*, V])
⟨⟨f,⟨α,⟨⟩,⟨⟨b,γ⟩,(OverBar[J])⟩⟩⟩⟩)(Underscript[+, V])⟨⟨f(Underscript[*, ℱ])b,⟨α,β(Underscript[*, TuplesMonoid[ℕ]])γ,⟨(OverBar[J])⟩⟩⟩⟩, ⇐, otherwise}})}}, {(∂_V)⟨⟨f,⟨α,β,J⟩⟩,(OverBar[(OverTilde[J])])⟩=(∂_V)⟨f,⟨α,β,J⟩⟩(Underscript[+, V])(∂_V)⟨(OverBar[(OverTilde[J])])⟩}, {(∫_V)⟨⟩=⟨⟩}, {(∫_V)⟨⟨f,⟨α,⟨⟩,⟨⟩⟩⟩⟩=((∫_ℱ)f)(Underscript[·, V])⟨⟨(Underscript[1, ℱ]),⟨α,⟨⟩,⟨⟩⟩⟩⟩}, {(∫_V)⟨⟨f,⟨α,⟨⟩,⟨⟨b,γ⟩,(OverBar[J])⟩⟩⟩⟩=(* quasiconstant *)((∫_ℱ)f)(Underscript[·, V])⟨⟨(Underscript[1, ℱ]),⟨α,⟨⟩,⟨⟨b,γ⟩,(OverBar[J])⟩⟩⟩⟩(Underscript[-, V])
((∫_V)⟨⟨b(Underscript[*, ℱ])(∫_ℱ)f,⟨α,γ,⟨(OverBar[J])⟩⟩⟩⟩)}, {(∫_V)⟨⟨f,⟨α,⟨0,1⟩,⟨⟩⟩⟩⟩=(* quasilinear base case *)
(⟨⟨f,⟨α,⟨1⟩,⟨⟩⟩⟩⟩(Underscript[-, V])(∫_V)(((∂_ℱ)f)(Underscript[·, V])⟨⟨(Underscript[1, ℱ]),⟨α,⟨1⟩,⟨⟩⟩⟩⟩))(Underscript[-, V])(Underscript[eval, V])[⟨⟨f,⟨α,⟨1⟩,⟨⟩⟩⟩⟩,0]}, {(∫_V)⟨⟨f,⟨α,⟨0,1⟩,⟨⟨b,γ⟩,(OverBar[J])⟩⟩⟩⟩=(* quasilinear base case *)
(⟨⟨f,⟨α,⟨1⟩,⟨⟨b,γ⟩,(OverBar[J])⟩⟩⟩⟩(Underscript[-, V])(∫_V)(((∂_ℱ)f)(Underscript[·, V])⟨⟨(Underscript[1, ℱ]),⟨α,⟨1⟩,⟨⟨b,γ⟩,(OverBar[J])⟩⟩⟩⟩))(Underscript[-, V])(∫_V)⟨⟨f(Underscript[*, ℱ])b,⟨α,⟨1⟩(Underscript[*, TuplesMonoid[ℕ]])γ,⟨(OverBar[J])⟩⟩⟩⟩}, {(∫_V)⟨⟨f,⟨α,⟨(OverBar[α]),k,1⟩,⟨⟩⟩⟩⟩=(* quasilinear *)
(1(Underscript[/, K])(k+1)(Underscript[·, ℱ])(Underscript[1, ℱ]))(Underscript[·, V])((⟨⟨f,⟨α,⟨(OverBar[α]),k+1⟩,⟨⟩⟩⟩⟩(Underscript[-, V])(∫_V)((∂_V)⟨⟨f,⟨α,⟨(OverBar[α])⟩,⟨⟩⟩⟩⟩(Underscript[*, V])⟨⟨(Underscript[1, ℱ]),⟨⟨⟩,⟨0(Underscript[|, i=0,…,\[LeftBracketingBar]⟨(OverBar[α])⟩\[RightBracketingBar]-1]),k+1⟩,⟨⟩⟩⟩⟩))(Underscript[-, V])(Underscript[eval, V])[⟨⟨f,⟨α,⟨(OverBar[α]),k+1⟩,⟨⟩⟩⟩⟩,0])}, {(∫_V)⟨⟨f,⟨α,⟨(OverBar[α]),k,1⟩,J⟩⟩⟩=(* quasilinear *)
(1(Underscript[/, K])(k+1)(Underscript[·, ℱ])(Underscript[1, ℱ]))(Underscript[·, V])(⟨⟨f,⟨α,⟨(OverBar[α]),k+1⟩,J⟩⟩⟩(Underscript[-, V])(∫_V)((∂_V)⟨⟨f,⟨α,⟨(OverBar[α])⟩,J⟩⟩⟩(Underscript[*, V])⟨⟨(Underscript[1, ℱ]),⟨⟨⟩,⟨0(Underscript[|, i=0,…,\[LeftBracketingBar]⟨(OverBar[α])⟩\[RightBracketingBar]-1]),k+1⟩,⟨⟩⟩⟩⟩))}, {(∫_V)⟨⟨f,⟨α,β,⟨(OverBar[J])⟩⟩⟩⟩=(* functional *)⟨⟨(Underscript[1, ℱ]),⟨α,⟨⟩,⟨⟨f,β⟩,(OverBar[J])⟩⟩⟩⟩}, {(∫_V)⟨J,(OverBar[J])⟩=(∫_V)⟨J⟩(Underscript[+, V])(∫_V)⟨(OverBar[J])⟩}, {(Underscript[PrettyPrint, V])[p]=™Plus[(Underscript[PrettyPrintM, V])[(Subscript[p, i])](Underscript[|, i=1,…,\[LeftBracketingBar]p\[RightBracketingBar]])]}, {(Underscript[PrettyPrintV, V])[p]=™Plus[(Underscript[PrettyPrintMV, V])[(Subscript[p, i])](Underscript[|, i=1,…,\[LeftBracketingBar]p\[RightBracketingBar]])]}, {(Underscript[PrettyPrint, V])[⟨p⟩]=(Underscript[PrettyPrintM, V])[p]}, {(Underscript[PrettyPrintV, V])[⟨p⟩]=(Underscript[PrettyPrintMV, V])[p]}, {(Underscript[PrettyPrint, V])[⟨⟩]=0}, {(Underscript[PrettyPrintV, V])[⟨⟩]=0}, {(Underscript[PrettyPrintM, V])[⟨c,w⟩]=tma–trfm[™Times[(Underscript[PrettyPrint, ℱ])[c],(Underscript[PrettyPrintW, V])[w]]]}, {(Underscript[PrettyPrintMV, V])[⟨c,w⟩]=tma–trfm[™Times[(Underscript[PrettyPrint, ℱ])[c],(Underscript[PrettyPrintWV, V])[w]]]}, {(Underscript[PrettyPrintW, V])[⟨⟩]=1}, {(Underscript[PrettyPrintWV, V])[⟨⟩]=1}, {(Underscript[PrettyPrintW, V])[⟨⟨⟩,⟨⟩,J⟩]=(Underscript[PrettyPrintL, V])[J]}, {(Underscript[PrettyPrintWV, V])[⟨⟨⟩,⟨⟩,J⟩]=(Underscript[PrettyPrintLV, V])[J]}, {(Underscript[PrettyPrintW, V])[⟨⟨⟩,β,J⟩]=mytimes[™Power[u,β],(Underscript[PrettyPrintL, V])[J]]}, {(Underscript[PrettyPrintW, V])V[⟨⟨⟩,β,J⟩]=mytimes[™Power[v,β],(Underscript[PrettyPrintLV, V])[J]]}, {(Underscript[PrettyPrintW, V])[⟨α,⟨⟩,J⟩]=mytimes[™Power[u[0],α],(Underscript[PrettyPrintL, V])[J]]}, {(Underscript[PrettyPrintWV, V])[⟨α,⟨⟩,J⟩]=mytimes[™Power[v[0],α],(Underscript[PrettyPrintLV, V])[J]]}, {(Underscript[PrettyPrintW, V])[⟨α,β,J⟩]=mytimes[™Power[u[0],α],™Power[u,β],(Underscript[PrettyPrintL, V])[J]]}, {(Underscript[PrettyPrintWV, V])[⟨α,β,J⟩]=mytimes[™Power[v[0],α],™Power[v,β],(Underscript[PrettyPrintLV, V])[J]]}, {(Underscript[PrettyPrintL, V])[⟨⟩]=""}, {(Underscript[PrettyPrintLV, V])[⟨⟩]=""}, {(Underscript[PrettyPrintL, V])[⟨⟨b,γ⟩,(OverBar[J])⟩]=mytimes[mytimes["∫",(Underscript[PrettyPrint, ℱ])[b]],™Power[u,γ],(Underscript[PrettyPrintL, V])[⟨(OverBar[J])⟩]]}, {(Underscript[PrettyPrintLV, V])[⟨⟨b,γ⟩,(OverBar[J])⟩]=mytimes[mytimes["∫",(Underscript[PrettyPrint, ℱ])[b]],™Power[v,γ],(Underscript[PrettyPrintLV, V])[⟨(OverBar[J])⟩]]}})}})
	]]]

Definition["PrettyPrinting",any[ℱ,K],
PrettyPrinting[ℱ,K]=Functor[P,any[b,c,m,n,p,r,w,α,β,λ,γ,η,J,L,(OverBar[η]),(OverBar[ξ]),(OverBar[J])],
	({{𝕤=⟨⟩}, {({{(Underscript[PrettyPrintW, P])[⟨⟩]=""}, {(Underscript[PrettyPrintW, P])[⟨λ,η,(OverBar[η])⟩]=mytimes[(Underscript[PrettyPrintL, P])[λ],(Underscript[PrettyPrintW, P])[⟨η,(OverBar[η])⟩]] }, {(Underscript[PrettyPrintW, P])[⟨η⟩]=(Underscript[PrettyPrintL, P])[η]}, {(Underscript[PrettyPrintF, P])[⟨⟨⟩,⟨⟩,⟨⟩⟩]=""}, {(Underscript[PrettyPrintF, P])[⟨α,⟨⟩,⟨⟩⟩]=™Power[v[0],α]}, {(Underscript[PrettyPrintF, P])[⟨⟨⟩,β,⟨⟩⟩]=mytimes[™Power[v,β]]}, {(Underscript[PrettyPrintF, P])[⟨α,β,⟨⟩⟩]=mytimes[™Power[v[0],α],™Power[v,β]]}, {(Underscript[PrettyPrintF, P])[⟨⟨⟩,⟨⟩,J⟩]=(Underscript[PrettyPrintJ, P])[J]}, {(Underscript[PrettyPrintF, P])[⟨α,β,J⟩]=mytimes[™Power[v[0],α],™Power[v,β],(Underscript[PrettyPrintJ, P])[J]]}, {(Underscript[PrettyPrintL, P])[⟨"⌈⌉",⟨⟨c,⟨α,β,J⟩⟩⟩⟩]=mytimes[(Underscript[PrettyPrint, IntDiffPolys[𝔼xp,𝕂]])[c],(Underscript[PrettyPrintF, P])[⟨α,β,J⟩]]}, {(Underscript[PrettyPrintL, P])[⟨"⌊⌋",0⟩]="E"}, {(Underscript[PrettyPrintJ, P])[⟨⟩]=""}, {(Underscript[PrettyPrintJ, P])[⟨⟨b,γ⟩,(OverBar[J])⟩]=mytimes[mytimes["∫",(Underscript[PrettyPrintV, IntDiffPolys[𝔼xp,𝕂]])[b]],™Power[v,γ],(Underscript[PrettyPrintJ, P])[⟨(OverBar[J])⟩]]}, {(Underscript[PrettyPrintL, P])["∂"]="∂"}, {(Underscript[PrettyPrintL, P])["∫"]="∫"}, {(Underscript[PrettyPrintL, P])[⟨⟩]=""}, {(Underscript[PrettyPrintL, P])[η]=η}, {(Underscript[PrettyPrintM, P])[⟨⟩]=0}, {(Underscript[PrettyPrintM, P])[⟨c,⟨⟩⟩]=c}, {(Underscript[PrettyPrintM, P])[⟨c,w⟩]=mytimes[(Underscript[PrettyPrint, K])[c],(Underscript[PrettyPrintW, P])[w]]}, {(Underscript[PrettyPrintRule, P])[⟨m,n⟩]=(Underscript[PrettyPrint, P])[m]->(Underscript[PrettyPrint, P])[n]}, {(Underscript[PrettyPrintRules, P])[L]=⟨(Underscript[PrettyPrintRule, P])[(Subscript[L, i])](Underscript[|, i=1,…,\[LeftBracketingBar]L\[RightBracketingBar]])⟩}, {(Underscript[PrettyPrint, P])[⟨⟨⟨c,η⟩,(OverBar[ξ])⟩,(OverBar[η])⟩]=⟨(Underscript[PrettyPrint, P])[(Subscript[⟨⟨⟨c,η⟩,(OverBar[ξ])⟩,(OverBar[η])⟩, i])](Underscript[|, i=1,…,\[LeftBracketingBar]⟨⟨⟨c,η⟩,(OverBar[ξ])⟩,(OverBar[η])⟩\[RightBracketingBar]])⟩}, {(Underscript[PrettyPrint, P])[p]=™Plus[(Underscript[PrettyPrintM, P])[(Subscript[p, i])](Underscript[|, i=1,…,\[LeftBracketingBar]p\[RightBracketingBar]])]}, {(Underscript[PrettyPrint, P])[⟨m⟩]=(Underscript[PrettyPrintM, P])[m]}, {(Underscript[PrettyPrint, P])[⟨⟩]=0}})}})]]

Translator IDP

Translator Exponential Polynomials

Use[⟨Built–in["Tuples"],Built–in["Quantifiers"],Built–in["Connectives"],Built–in["Mult"],Built–in["Minus"],Built–in["IsNumber"]⟩]

Definition["Parsing Exp",any[ℱ],
Parsing[ℱ]=Functor[P,any[c,m,n,r,λ,(OverBar[m]),(OverBar[n])],
	({{𝕤=⟨⟩}, {({{(Underscript[ParsePol, P])[]=⟨⟩}, {(Underscript[ParsePol, P])[™Tuple[(OverBar[m])]]=⟨(Underscript[ParsePol, P])[(Subscript[⟨(OverBar[m])⟩, i])](Underscript[|, i=1,…,\[LeftBracketingBar]⟨(OverBar[m])⟩\[RightBracketingBar]])⟩}, {(Underscript[ParsePol, P])[™Plus[]]=⟨⟩}, {(Underscript[ParsePol, P])[™Plus[m,(OverBar[n])]]=(Underscript[ParsePol, P])[m]≍(Underscript[ParsePol, P])[™Plus[(OverBar[n])]]}, {(Underscript[ParsePol, P])[™Times[™Minus[c],(OverBar[m])]]=(Underscript[ParseTerm, P])[™Times[™Minus[c],(OverBar[m])]]}, {(Underscript[ParsePol, P])[™Times[c,(OverBar[m])]]=(Underscript[ParseTerm, P])[™Times[c,(OverBar[m])]]}, {(Underscript[ParsePol, P])[™Minus[™Times[™Minus[c],(OverBar[m])]]]=(Underscript[ParseTerm, P])[™Times[c,(OverBar[m])]]}, {(Underscript[ParsePol, P])[™Minus[™Times[c,(OverBar[m])]]]=(Underscript[ParseTerm, P])[™Times[™Minus[c],(OverBar[m])]]}, {(Underscript[ParsePol, P])[™Minus[m,n]]=(Underscript[ParsePol, P])[m]≍(Underscript[ParsePol, P])[™Minus[n]]}, {(Underscript[ParsePol, P])[™Minus[m,n,r,(OverBar[m])]]=(Underscript[ParsePol, P])[m]≍(Underscript[ParsePol, P])[™Minus[™Minus[n],r,(OverBar[m])]]}, {(Underscript[ParsePol, P])[™Minus[c]]={({{⟨⟨-c,⟨⟩⟩⟩, ⇐, ™IsNumber[c]}, {(Underscript[ParseTerm, P])[™Minus[c]], ⇐, otherwise}})}}, {(Underscript[ParsePol, P])[c]={({{⟨⟨c,⟨⟩⟩⟩, ⇐, ™IsNumber[c]}, {(Underscript[ParseTerm, P])[c], ⇐, otherwise}})}  }, {(Underscript[ParseTerm, P])[™Minus[c]]={({{⟨⟨-c,⟨⟩⟩⟩, ⇐, ™IsNumber[c]}, {-1(Underscript[·, ℱ])(Underscript[ParseMon, P])[c], ⇐, otherwise}})}  }, {(Underscript[ParseTerm, P])[™Times[™Times[(OverBar[m])]]]=(Underscript[ParseTerm, P])[™Times[(OverBar[m])]]}, {(Underscript[ParseTerm, P])[™Times[™Minus[c],(OverBar[m])]]={({{-c(Underscript[·, ℱ])(Underscript[ParseTerm, P])[™Times[(OverBar[m])]], ⇐, ™IsNumber[c]}, {-1(Underscript[·, ℱ])(Underscript[ParseTerm, P])[™Times[c,(OverBar[m])]], ⇐, otherwise}})}  }, {(Underscript[ParseTerm, P])[™Times[c,(OverBar[m])]]={({{c(Underscript[·, ℱ])(Underscript[ParseTerm, P])[™Times[(OverBar[m])]], ⇐, ™IsNumber[c]}, {(Underscript[ParseMon, P])[™Times[c,(OverBar[m])]], ⇐, otherwise}})}  }, {(Underscript[ParseTerm, P])[c]={({{⟨⟨c,⟨⟩⟩⟩, ⇐, ™IsNumber[c]}, {(Underscript[ParseMon, P])[c], ⇐, otherwise}})}  }, {(Underscript[ParseTerm, P])[™Times[]]=⟨⟩}, {(Underscript[ParseMon, P])[™Times[™Power[x,n],™Power[E,™Times[λ,x]]]]=⟨⟨1,⟨⟨"⌈⌉",⟨n,λ⟩⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[™Times[™Power[x,n],™Power[E,™Times[λ,x]]]]]=⟨⟨1,⟨⟨"⌈⌉",⟨n,λ⟩⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[™Power[x,n],™Power[E,x]]]=⟨⟨1,⟨⟨"⌈⌉",⟨n,1⟩⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[™Times[™Power[x,n],™Power[E,x]]]]=⟨⟨1,⟨⟨"⌈⌉",⟨n,1⟩⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[x,™Power[E,™Times[λ,x]]]]=⟨⟨1,⟨⟨"⌈⌉",⟨1,λ⟩⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[™Times[x,™Power[E,™Times[λ,x]]]]]=⟨⟨1,⟨⟨"⌈⌉",⟨1,λ⟩⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™Power[E,™Times[λ,x]]]=⟨⟨1,⟨⟨"⌈⌉",⟨0,λ⟩⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[™Power[E,™Times[λ,x]]]]=⟨⟨1,⟨⟨"⌈⌉",⟨0,λ⟩⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™Power[x,n]]=⟨⟨1,⟨⟨"⌈⌉",⟨n,0⟩⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[™Power[x,n]]]=⟨⟨1,⟨⟨"⌈⌉",⟨n,0⟩⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™Power[E,x]]=⟨⟨1,⟨⟨"⌈⌉",⟨0,1⟩⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[™Power[E,x]]]=⟨⟨1,⟨⟨"⌈⌉",⟨0,1⟩⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™Power[E,™Minus[x]]]=⟨⟨1,⟨⟨"⌈⌉",⟨0,-1⟩⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[™Power[E,™Minus[x]]]]=⟨⟨1,⟨⟨"⌈⌉",⟨0,-1⟩⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[x]=⟨⟨1,⟨⟨"⌈⌉",⟨1,0⟩⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[x]]=⟨⟨1,⟨⟨"⌈⌉",⟨1,0⟩⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™Floor[c]]=⟨⟨1,⟨⟨"⌊⌋",c⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[™Floor[c]]]=⟨⟨1,⟨⟨"⌊⌋",c⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™D]=⟨⟨1,⟨"∂"⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[™D]]=⟨⟨1,⟨"∂"⟩⟩⟩}, {(Underscript[ParseMon, P])[™Power[m,0]]=⟨⟩}, {(Underscript[ParseMon, P])[™Power[m,1]]=(Underscript[ParseMon, P])[m]}, {(Underscript[ParseMon, P])[™Power[m,n]]=(Underscript[ParseMon, P])[m](Underscript[*, ℱ])(Underscript[ParseMon, P])[™Power[m,n(Underscript[-, MmaAuxF[]])1]]}, {(Underscript[ParseMon, P])[™Times[™Power[m,n]]]=(Underscript[ParseMon, P])[™Power[m,n]]}, {(Underscript[ParseMon, P])[™Times[™Times[(OverBar[m])]]]=(Underscript[ParseMon, P])[™Times[(OverBar[m])]]}, {(Underscript[ParseMon, P])[™Times[m,n,(OverBar[n])]]=(Underscript[ParseMon, P])[m](Underscript[*, ℱ])(Underscript[ParseMon, P])[™Times[n,(OverBar[n])]]}, {(Underscript[ParseMon, P])[c]=⟨⟨c,⟨⟩⟩⟩}, {(Underscript[ParseMon, P])[]=⟨⟩}})}})]]

Definition["Parsing",any[ℱ],
Parsing[ℱ]=Functor[P,any[c,m,n,r,λ,(OverBar[m]),(OverBar[n])],
	({{𝕤=⟨⟩}, {({{(Underscript[ParsePol, P])[]=⟨⟩}, {(Underscript[ParsePol, P])[™Tuple[(OverBar[m])]]=⟨(Underscript[ParsePol, P])[(Subscript[⟨(OverBar[m])⟩, i])](Underscript[|, i=1,…,\[LeftBracketingBar]⟨(OverBar[m])⟩\[RightBracketingBar]])⟩}, {(Underscript[ParsePol, P])[™Plus[]]=⟨⟩}, {(Underscript[ParsePol, P])[™Plus[m,(OverBar[n])]]=(Underscript[ParsePol, P])[m]≍(Underscript[ParsePol, P])[™Plus[(OverBar[n])]]}, {(Underscript[ParsePol, P])[™Times[™Minus[c],(OverBar[m])]]=(Underscript[ParseTerm, P])[™Times[™Minus[c],(OverBar[m])]]}, {(Underscript[ParsePol, P])[™Times[c,(OverBar[m])]]=(Underscript[ParseTerm, P])[™Times[c,(OverBar[m])]]}, {(Underscript[ParsePol, P])[™Minus[™Times[™Minus[c],(OverBar[m])]]]=(Underscript[ParseTerm, P])[™Times[c,(OverBar[m])]]}, {(Underscript[ParsePol, P])[™Minus[™Times[c,(OverBar[m])]]]=(Underscript[ParseTerm, P])[™Times[™Minus[c],(OverBar[m])]]}, {(Underscript[ParsePol, P])[™Minus[m,n]]=(Underscript[ParsePol, P])[m]≍(Underscript[ParsePol, P])[™Minus[n]]}, {(Underscript[ParsePol, P])[™Minus[m,n,r,(OverBar[m])]]=(Underscript[ParsePol, P])[m]≍(Underscript[ParsePol, P])[™Minus[™Minus[n],r,(OverBar[m])]]}, {(Underscript[ParsePol, P])[™Minus[c]]={({{⟨⟨-c,⟨⟩⟩⟩, ⇐, ™IsNumber[c]}, {(Underscript[ParseTerm, P])[™Minus[c]], ⇐, otherwise}})}}, {(Underscript[ParsePol, P])[c]={({{⟨⟨c,⟨⟩⟩⟩, ⇐, ™IsNumber[c]}, {(Underscript[ParseTerm, P])[c], ⇐, otherwise}})}  }, {(Underscript[ParseTerm, P])[™Minus[c]]={({{⟨⟨-c,⟨⟩⟩⟩, ⇐, ™IsNumber[c]}, {-1(Underscript[·, ℱ])(Underscript[ParseMon, P])[c], ⇐, otherwise}})}  }, {(Underscript[ParseTerm, P])[™Times[™Times[(OverBar[m])]]]=(Underscript[ParseTerm, P])[™Times[(OverBar[m])]]}, {(Underscript[ParseTerm, P])[™Times[™Minus[c],(OverBar[m])]]={({{-c(Underscript[·, ℱ])(Underscript[ParseTerm, P])[™Times[(OverBar[m])]], ⇐, ™IsNumber[c]}, {-1(Underscript[·, ℱ])(Underscript[ParseTerm, P])[™Times[c,(OverBar[m])]], ⇐, otherwise}})}  }, {(Underscript[ParseTerm, P])[™Times[c,(OverBar[m])]]={({{c(Underscript[·, ℱ])(Underscript[ParseTerm, P])[™Times[(OverBar[m])]], ⇐, ™IsNumber[c]}, {(Underscript[ParseMon, P])[™Times[c,(OverBar[m])]], ⇐, otherwise}})}  }, {(Underscript[ParseTerm, P])[c]={({{⟨⟨c,⟨⟩⟩⟩, ⇐, ™IsNumber[c]}, {(Underscript[ParseMon, P])[c], ⇐, otherwise}})}  }, {(Underscript[ParseTerm, P])[™Times[]]=⟨⟩}, {(Underscript[ParseMon, P])[™Times[™Power[x,n],™Power[E,™Times[λ,x]]]]=⟨⟨1,⟨n,λ⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[™Times[™Power[x,n],™Power[E,™Times[λ,x]]]]]=⟨⟨1,⟨n,λ⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[™Power[x,n],™Power[E,x]]]=⟨⟨1,⟨n,1⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[™Times[™Power[x,n],™Power[E,x]]]]=⟨⟨1,⟨n,1⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[x,™Power[E,™Times[λ,x]]]]=⟨⟨1,⟨1,λ⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[™Times[x,™Power[E,™Times[λ,x]]]]]=⟨⟨1,⟨1,λ⟩⟩⟩}, {(Underscript[ParseMon, P])[™Power[E,™Times[λ,x]]]=⟨⟨1,⟨0,λ⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[™Power[E,™Times[λ,x]]]]=⟨⟨1,⟨0,λ⟩⟩⟩}, {(Underscript[ParseMon, P])[™Power[x,n]]=⟨⟨1,⟨n,0⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[™Power[x,n]]]=⟨⟨1,⟨n,0⟩⟩⟩}, {(Underscript[ParseMon, P])[™Power[E,x]]=⟨⟨1,⟨0,1⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[™Power[E,x]]]=⟨⟨1,⟨0,1⟩⟩⟩}, {(Underscript[ParseMon, P])[™Power[E,™Minus[x]]]=⟨⟨1,⟨0,-1⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[™Power[E,™Minus[x]]]]=⟨⟨1,⟨0,-1⟩⟩⟩}, {(Underscript[ParseMon, P])[x]=⟨⟨1,⟨1,0⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[x]]=⟨⟨1,⟨1,0⟩⟩⟩}, {(Underscript[ParseMon, P])[™Power[m,0]]=⟨⟩}, {(Underscript[ParseMon, P])[™Power[m,1]]=(Underscript[ParseMon, P])[m]}, {(Underscript[ParseMon, P])[™Power[m,n]]=(Underscript[ParseMon, P])[m](Underscript[*, ℱ])(Underscript[ParseMon, P])[™Power[m,n(Underscript[-, MmaAuxF[]])1]]}, {(Underscript[ParseMon, P])[™Times[™Power[m,n]]]=(Underscript[ParseMon, P])[™Power[m,n]]}, {(Underscript[ParseMon, P])[™Times[™Times[(OverBar[m])]]]=(Underscript[ParseMon, P])[™Times[(OverBar[m])]]}, {(Underscript[ParseMon, P])[™Times[m,n,(OverBar[n])]]=(Underscript[ParseMon, P])[m](Underscript[*, ℱ])(Underscript[ParseMon, P])[™Times[n,(OverBar[n])]]}, {(Underscript[ParseMon, P])[c]=⟨⟨c,⟨⟩⟩⟩}, {(Underscript[ParseMon, P])[]=⟨⟩}})}})]]

Definition["ParsingF",any[ℱ],
ParsingF[ℱ]=Functor[P,any[c,m,n,r,λ,(OverBar[m]),(OverBar[n])],
	({{𝕤=⟨⟩}, {({{(Underscript[ParsePolF, P])[]=⟨⟩}, {(Underscript[ParsePolF, P])[0]=⟨⟩}, {(Underscript[ParsePolF, P])[™Tuple[(OverBar[m])]]=⟨(Underscript[ParsePolF, P])[(Subscript[⟨(OverBar[m])⟩, i])](Underscript[|, i=1,…,\[LeftBracketingBar]⟨(OverBar[m])⟩\[RightBracketingBar]])⟩}, {(Underscript[ParsePolF, P])[™Plus[]]=⟨⟩}, {(Underscript[ParsePolF, P])[™Plus[m,(OverBar[n])]]=(Underscript[ParsePolF, P])[m]≍(Underscript[ParsePolF, P])[™Plus[(OverBar[n])]]}, {(Underscript[ParsePolF, P])[™Times[™Minus[c],(OverBar[m])]]=(Underscript[ParseTermF, P])[™Times[™Minus[c],(OverBar[m])]]}, {(Underscript[ParsePolF, P])[™Times[c,(OverBar[m])]]=(Underscript[ParseTermF, P])[™Times[c,(OverBar[m])]]}, {(Underscript[ParsePolF, P])[™Minus[™Times[™Minus[c],(OverBar[m])]]]=(Underscript[ParseTermF, P])[™Times[c,(OverBar[m])]]}, {(Underscript[ParsePolF, P])[™Minus[™Times[c,(OverBar[m])]]]=(Underscript[ParseTermF, P])[™Times[™Minus[c],(OverBar[m])]]}, {(Underscript[ParsePolF, P])[™Minus[m,n]]=(Underscript[ParsePolF, P])[m]≍(Underscript[ParsePolF, P])[™Minus[n]]}, {(Underscript[ParsePolF, P])[™Minus[m,n,r,(OverBar[m])]]=(Underscript[ParsePolF, P])[m]≍(Underscript[ParsePolF, P])[™Minus[™Minus[n],r,(OverBar[m])]]}, {(Underscript[ParsePolF, P])[™Minus[c]]={({{⟨⟨-c,⟨⟩⟩⟩, ⇐, ™IsNumber[c]}, {(Underscript[ParseTermF, P])[™Minus[c]], ⇐, otherwise}})}}, {(Underscript[ParsePolF, P])[c]={({{⟨⟨c,⟨⟩⟩⟩, ⇐, ™IsNumber[c]}, {(Underscript[ParseTermF, P])[c], ⇐, otherwise}})}  }, {(Underscript[ParseTermF, P])[™Minus[c]]={({{⟨⟨-c,⟨⟩⟩⟩, ⇐, ™IsNumber[c]}, {-1(Underscript[·, ℱ])(Underscript[ParseMonF, P])[c], ⇐, otherwise}})}  }, {(Underscript[ParseTermF, P])[™Times[™Times[(OverBar[m])]]]=(Underscript[ParseTermF, P])[™Times[(OverBar[m])]]}, {(Underscript[ParseTermF, P])[™Times[™Minus[c],(OverBar[m])]]={({{-c(Underscript[·, ℱ])(Underscript[ParseTermF, P])[™Times[(OverBar[m])]], ⇐, ™IsNumber[c]}, {-1(Underscript[·, ℱ])(Underscript[ParseTermF, P])[™Times[c,(OverBar[m])]], ⇐, otherwise}})}  }, {(Underscript[ParseTermF, P])[™Times[c,(OverBar[m])]]={({{c(Underscript[·, ℱ])(Underscript[ParseTermF, P])[™Times[(OverBar[m])]], ⇐, ™IsNumber[c]}, {(Underscript[ParseMonF, P])[™Times[c,(OverBar[m])]], ⇐, otherwise}})}  }, {(Underscript[ParseTermF, P])[c]={({{⟨⟨c,⟨⟩⟩⟩, ⇐, ™IsNumber[c]}, {(Underscript[ParseMonF, P])[c], ⇐, otherwise}})}  }, {(Underscript[ParseTermF, P])[™Times[]]=⟨⟩}, {(Underscript[ParseMonF, P])[™Times[™Power[x,m],™Power[E,™Times[λ,x]]]]=⟨⟨1,⟨m,λ⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[™Power[E,™Times[λ,x]],™Power[x,m]]]=⟨⟨1,⟨m,λ⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[™Power[x,m],™Power[E,x]]]=⟨⟨1,⟨m,1⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[x,™Power[E,™Times[λ,x]]]]=⟨⟨1,⟨1,λ⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[™Times[™Power[x,m],™Power[E,™Times[λ,x]]]]]=⟨⟨1,⟨m,λ⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[™Times[™Power[E,™Times[λ,x]],™Power[x,m]]]]=⟨⟨1,⟨m,λ⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[™Times[™Power[x,m],™Power[E,x]]]]=⟨⟨1,⟨m,1⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[™Times[x,™Power[E,™Times[λ,x]]]]]=⟨⟨1,⟨1,λ⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Power[x,m]]=⟨⟨1,⟨m,0⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[™Power[x,m]]]=⟨⟨1,⟨m,0⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Power[E,™Times[λ,x]]]=⟨⟨1,⟨0,λ⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[™Power[E,™Times[λ,x]]]]=⟨⟨1,⟨0,λ⟩⟩⟩}, {(Underscript[ParseMonF, P])[x]=⟨⟨1,⟨1,0⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[x]]=⟨⟨1,⟨1,0⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Power[E,x]]=⟨⟨1,⟨0,1⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[™Power[E,x]]]=⟨⟨1,⟨0,1⟩⟩⟩}, {(Underscript[ParseMonF, P])[]=⟨⟩}})}})]]

Definition["Parsing Diff Polys",any[ℱ],
ParsingDP[ℱ]=Functor[P,any[c,k,l,m,n,r,λ,(OverBar[c]),(OverBar[d]),(OverBar[m]),(OverBar[n])],
	({{𝕤=⟨⟩}, {({{(Underscript[ParsePolF, P])[]=⟨⟩}, {(Underscript[ParsePolF, P])[0]=⟨⟩}, {(Underscript[ParsePolF, P])[™Tuple[(OverBar[m])]]=⟨(Underscript[ParsePolF, P])[(Subscript[⟨(OverBar[m])⟩, i])](Underscript[|, i=1,…,\[LeftBracketingBar]⟨(OverBar[m])⟩\[RightBracketingBar]])⟩}, {(Underscript[ParsePolF, P])[™Plus[]]=⟨⟩}, {(Underscript[ParsePolF, P])[™Plus[m,(OverBar[n])]]=(Underscript[ParsePolF, P])[m]≍(Underscript[ParsePolF, P])[™Plus[(OverBar[n])]]}, {(Underscript[ParsePolF, P])[™Times[™Minus[c],(OverBar[m])]]=(Underscript[ParseTermF, P])[™Times[™Minus[c],(OverBar[m])]]}, {(Underscript[ParsePolF, P])[™Times[c,(OverBar[m])]]=(Underscript[ParseTermF, P])[™Times[c,(OverBar[m])]]}, {(Underscript[ParsePolF, P])[™Minus[™Times[™Minus[c],(OverBar[m])]]]=(Underscript[ParseTermF, P])[™Times[c,(OverBar[m])]]}, {(Underscript[ParsePolF, P])[™Minus[™Times[c,(OverBar[m])]]]=(Underscript[ParseTermF, P])[™Times[™Minus[c],(OverBar[m])]]}, {(Underscript[ParsePolF, P])[™Minus[m,n]]=(Underscript[ParsePolF, P])[m]≍(Underscript[ParsePolF, P])[™Minus[n]]}, {(Underscript[ParsePolF, P])[™Minus[m,n,r,(OverBar[m])]]=(Underscript[ParsePolF, P])[m]≍(Underscript[ParsePolF, P])[™Minus[™Minus[n],r,(OverBar[m])]]}, {(Underscript[ParsePolF, P])[™Minus[c]]={({{⟨⟨-c,⟨0,0⟩⟩⟩, ⇐, ™IsNumber[c]}, {(Underscript[ParseTermF, P])[™Minus[c]], ⇐, otherwise}})}}, {(Underscript[ParsePolF, P])[c]={({{⟨⟨c,⟨0,0⟩⟩⟩, ⇐, ™IsNumber[c]}, {(Underscript[ParseTermF, P])[c], ⇐, otherwise}})}  }, {(Underscript[ParseTermF, P])[™Minus[c]]={({{⟨⟨-c,⟨0,0⟩⟩⟩, ⇐, ™IsNumber[c]}, {-1(Underscript[·, ℱ])(Underscript[ParseMonF, P])[c], ⇐, otherwise}})}  }, {(Underscript[ParseTermF, P])[™Times[™Times[(OverBar[m])]]]=(Underscript[ParseTermF, P])[™Times[(OverBar[m])]]}, {(Underscript[ParseTermF, P])[™Times[™Minus[c],(OverBar[m])]]={({{-c(Underscript[·, ℱ])(Underscript[ParseTermF, P])[™Times[(OverBar[m])]], ⇐, ™IsNumber[c]}, {-1(Underscript[·, ℱ])(Underscript[ParseTermF, P])[™Times[c,(OverBar[m])]], ⇐, otherwise}})}  }, {(Underscript[ParseTermF, P])[™Times[c,(OverBar[m])]]={({{c(Underscript[·, ℱ])(Underscript[ParseTermF, P])[™Times[(OverBar[m])]], ⇐, ™IsNumber[c]}, {(Underscript[ParseMonF, P])[™Times[c,(OverBar[m])]], ⇐, otherwise}})}  }, {(Underscript[ParseTermF, P])[c]={({{⟨⟨c,⟨0,0⟩⟩⟩, ⇐, ™IsNumber[c]}, {(Underscript[ParseMonF, P])[c], ⇐, otherwise}})}  }, {(Underscript[ParseTermF, P])[™Times[]]=⟨⟩}, {(Underscript[ParseMonF, P])[™Times[™Power[x,m],™Power[E,™Times[λ,x]]]]=⟨⟨1,⟨m,λ⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[™Power[E,™Times[λ,x]],™Power[x,m]]]=⟨⟨1,⟨m,λ⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[™Power[x,m],™Power[E,x]]]=⟨⟨1,⟨m,1⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[x,™Power[E,x]]]=⟨⟨1,⟨1,1⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[x,™Power[E,™Times[λ,x]]]]=⟨⟨1,⟨1,λ⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[™Times[™Power[x,m],™Power[E,™Times[λ,x]]]]]=⟨⟨1,⟨m,λ⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[™Times[™Power[E,™Times[λ,x]],™Power[x,m]]]]=⟨⟨1,⟨m,λ⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[™Times[™Power[x,m],™Power[E,x]]]]=⟨⟨1,⟨m,1⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[™Times[x,™Power[E,™Times[λ,x]]]]]=⟨⟨1,⟨1,λ⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Power[x,m]]=⟨⟨1,⟨m,0⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[™Power[x,m]]]=⟨⟨1,⟨m,0⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[c,™Power[x,m]]]=⟨⟨c,⟨m,0⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Power[E,™Times[λ,x]]]=⟨⟨1,⟨0,λ⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[™Power[E,™Times[λ,x]]]]=⟨⟨1,⟨0,λ⟩⟩⟩}, {(Underscript[ParseMonF, P])[x]=⟨⟨1,⟨1,0⟩⟩⟩}, {(Underscript[ParseMonF, P])[E]=⟨⟨1,⟨0,1⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[x]]=⟨⟨1,⟨1,0⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Power[E,x]]=⟨⟨1,⟨0,1⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[™Power[E,x]]]=⟨⟨1,⟨0,1⟩⟩⟩}, {(Underscript[ParseMonF, P])[™Times[c]]=(Underscript[ParsePolF, P])[c]}, {(Underscript[ParseMonF, P])[c]=⟨⟨c,⟨0,0⟩⟩⟩}, {(Underscript[ParseMonF, P])[]=⟨⟩}, {(Underscript[ParseDP, P])[]=⟨⟩}, {(Underscript[ParseDP, P])[™Plus[]]=⟨⟩}, {(Underscript[ParseDP, P])[™Plus[m,(OverBar[n])]]=(Underscript[ParseMonDP, P])[m]≍(Underscript[ParseDP, P])[™Plus[(OverBar[n])]]}, {(Underscript[ParseDP, P])[™Power[u,k]]=⟨⟨(Underscript[1, ℱ]),k⟩⟩}, {(Underscript[ParseDP, P])[™Times[(OverBar[c]),™Power[u,k]]]=(Underscript[ParseMonDP, P])[™Times[(OverBar[c]),™Power[u,k]]]}, {(Underscript[ParseMonDP, P])[™Times[(OverBar[c]),™Power[u,k]]]=where[p=(Underscript[ParsePolF, P])[™Times[(OverBar[c])]],
⟨⟨p,k⟩⟩]}, {(Underscript[ParseMonDP, P])[™Power[u,k]]=⟨⟨(Underscript[1, ℱ]),k⟩⟩}, {(Underscript[ParseIDP, P])[]=⟨⟩}, {(Underscript[ParseIDP, P])[™Plus[]]=⟨⟩}, {(Underscript[ParseIDP, P])[™Plus[m,(OverBar[n])]]=(Underscript[ParseIDP, P])[m]≍(Underscript[ParseIDP, P])[™Plus[(OverBar[n])]]}, {(Underscript[ParseIDP, P])[™Times[™Minus[c],(OverBar[m])]]=(Underscript[ParseMonIDP, P])[™Times[™Minus[c],(OverBar[m])]]}, {(Underscript[ParseIDP, P])[™Minus[™Times[™Minus[c],(OverBar[m])]]]=(Underscript[ParseMonIDP, P])[™Times[c,(OverBar[m])]]}, {(Underscript[ParseIDP, P])[™Minus[™Times[c,(OverBar[m])]]]=(Underscript[ParseMonIDP, P])[™Times[™Minus[c],(OverBar[m])]]}, {(Underscript[ParseIDP, P])[™Minus[m,n]]=(Underscript[ParseIDP, P])[m]≍(Underscript[ParseIDP, P])[™Minus[n]]}, {(Underscript[ParseIDP, P])[™Minus[m,n,r,(OverBar[m])]]=(Underscript[ParseIDP, P])[m]≍(Underscript[ParseIDP, P])[™Minus[™Minus[n],r,(OverBar[m])]]}, {(Underscript[ParseIDP, P])[™Minus[c]]={({{⟨⟨(Underscript[ParsePolF, P])[-c],⟨0,0⟩⟩⟩, ⇐, (Underscript[∈, ℱ])[c]}, {(Underscript[ParseMonIDP, P])[™Minus[c]], ⇐, otherwise}})}}, {(Underscript[ParseMonIDP, P])[™Minus[c]]={({{⟨⟨(Underscript[ParsePolF, P])[-c],⟨0,0⟩⟩⟩, ⇐, (Underscript[∈, ℱ])[c]}, {(-(Underscript[1, IntDiffPolys[ℱ,𝕂]]))(Underscript[·, IntDiffPolys[ℱ,𝕂]])(Underscript[ParseMonIDP, P])[c], ⇐, otherwise}})}  }, {(Underscript[ParseIDP, P])[™Times[c,(OverBar[d])]]=(Underscript[ParseMonIDP, P])[™Times[c,(OverBar[d])]]}, {(Underscript[ParseIDP, P])[™Power[u,k]]=⟨⟨(Underscript[1, ℱ]),⟨⟨⟩,k,⟨⟩⟩⟩⟩}, {(Underscript[ParseIDP, P])[u]=⟨⟨(Underscript[1, ℱ]),⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩}, {(Underscript[ParseIDP, P])[™Power[u[0],k]]=⟨⟨(Underscript[1, ℱ]),⟨k,⟨⟩,⟨⟩⟩⟩⟩}, {(Underscript[ParseIDP, P])[u[0]]=⟨⟨(Underscript[1, ℱ]),⟨⟨1⟩,⟨⟩,⟨⟩⟩⟩⟩}, {(Underscript[ParseIDP, P])[™Times[c,™Power[u,k]]]=(Underscript[ParseMonIDP, P])[™Times[c,™Power[u,k]]]}, {(Underscript[ParseIDP, P])[c]=⟨⟨(Underscript[ParsePolF, P])[c],⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩}, {(Underscript[ParseMonIDP, P])[™Minus[c]]={({{⟨⟨(Underscript[ParsePolF, P])[-c],⟨0,0⟩⟩⟩, ⇐, (Underscript[∈, ℱ])[c]}, {(Underscript[-, IntDiffPolys[ℱ,𝕂]])(Underscript[ParseMonIDP, P])[c], ⇐, otherwise}})}  }, {(Underscript[ParseMonIDP, P])[™Times[™Minus[c],(OverBar[m])]]={({{(Underscript[ParsePolF, P])[-c](Underscript[·, IntDiffPolys[ℱ,𝕂]])(Underscript[ParseMonIDP, P])[™Times[(OverBar[m])]], ⇐, (Underscript[∈, ℱ])[c]}, {(Underscript[-, IntDiffPolys[ℱ,𝕂]])(Underscript[ParseMonIDP, P])[™Times[c,(OverBar[m])]], ⇐, otherwise}})}  }, {(Underscript[ParseMonIDP, P])[™Power[u,k]]=⟨⟨(Underscript[1, ℱ]),k⟩⟩}, {(Underscript[ParseMonIDP, P])[™Times[c,™Power[u[0],k],™Power[u,l],(OverBar[d])]]=where[p=(Underscript[ParsePolF, P])[c],
⟨⟨p,⟨k,l,(Underscript[ParseFunc, P])[™Times[(OverBar[d])]]⟩⟩⟩]}, {(Underscript[ParseMonIDP, P])[™Times[™Power[u[0],k],™Power[u,l],(OverBar[d])]]=⟨⟨(Underscript[1, ℱ]),⟨k,l,(Underscript[ParseFunc, P])[™Times[(OverBar[d])]]⟩⟩⟩}, {(Underscript[ParseMonIDP, P])[™Times[c,™Power[u[0],k],"∫",(OverBar[d])]]=where[p=(Underscript[ParsePolF, P])[c],
⟨⟨p,⟨k,⟨⟩,(Underscript[ParseFunc, P])[™Times["∫",(OverBar[d])]]⟩⟩⟩]}, {(Underscript[ParseMonIDP, P])[™Times[™Power[u[0],k],"∫",(OverBar[d])]]=⟨⟨(Underscript[1, ℱ]),⟨k,⟨⟩,(Underscript[ParseFunc, P])[™Times["∫",(OverBar[d])]]⟩⟩⟩}, {(Underscript[ParseMonIDP, P])[™Times[c,™Power[u,l],"∫",(OverBar[d])]]=where[p=(Underscript[ParsePolF, P])[c],
⟨⟨p,⟨⟨⟩,l,(Underscript[ParseFunc, P])[™Times["∫",(OverBar[d])]]⟩⟩⟩]}, {(Underscript[ParseMonIDP, P])[™Times[™Power[u,l],"∫",(OverBar[d])]]=⟨⟨(Underscript[1, ℱ]),⟨⟨⟩,l,(Underscript[ParseFunc, P])[™Times["∫",(OverBar[d])]]⟩⟩⟩}, {(Underscript[ParseMonIDP, P])[™Times[c,™Power[u[0],k]]]=where[p=(Underscript[ParsePolF, P])[c],
⟨⟨p,⟨k,⟨⟩,⟨⟩⟩⟩⟩]}, {(Underscript[ParseMonIDP, P])[™Times[™Power[u[0],k],(OverBar[c])]]=⟨⟨(Underscript[1, ℱ]),⟨k,⟨⟩,(Underscript[ParseFunc, P])[™Times[(OverBar[c])]]⟩⟩⟩}, {(Underscript[ParseMonIDP, P])[™Times[c,u[0]]]=where[p=(Underscript[ParsePolF, P])[c],
⟨⟨p,⟨⟨1⟩,⟨⟩,⟨⟩⟩⟩⟩]}, {(Underscript[ParseMonIDP, P])[u[0]]=⟨⟨(Underscript[1, ℱ]),⟨⟨1⟩,⟨⟩,⟨⟩⟩⟩⟩}, {(Underscript[ParseMonIDP, P])[™Times[c,™Power[u,k]]]=where[p=(Underscript[ParsePolF, P])[c],
⟨⟨p,⟨⟨⟩,k,⟨⟩⟩⟩⟩]}, {(Underscript[ParseMonIDP, P])[™Times[c,u]]=where[p=(Underscript[ParsePolF, P])[c],
⟨⟨p,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩]}, {(Underscript[ParseMonIDP, P])[u]=⟨⟨(Underscript[1, ℱ]),⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩}, {(Underscript[ParseMonIDP, P])[™Times[c,"∫",(OverBar[d])]]=where[p=(Underscript[ParsePolF, P])[c],
⟨⟨p,⟨⟨⟩,⟨⟩,(Underscript[ParseFunc, P])[™Times["∫",(OverBar[d])]]⟩⟩⟩]}, {(Underscript[ParseMonIDP, P])[c]=⟨⟨(Underscript[ParsePolF, P])[c],⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩}, {(Underscript[ParseFunc, P])[]=⟨⟩}, {(Underscript[ParseFunc, P])[™Times[]]=⟨⟩}, {(Underscript[ParseFunc, P])[™Times["∫",™Power[u,k],(OverBar[d])]]=⟨⟨(Underscript[1, ℱ]),k⟩⟩≍(Underscript[ParseFunc, P])[™Times[(OverBar[d])]]}, {(Underscript[ParseFunc, P])[™Times["∫",c,™Power[u,k],(OverBar[d])]]=⟨⟨(Underscript[ParsePolF, P])[c],k⟩⟩≍(Underscript[ParseFunc, P])[™Times[(OverBar[d])]]}})}})]]

Definition["ParsingIDO",any[ℱ],
ParsingIDO[ℱ]=Functor[P,any[c,m,n,r,λ,(OverBar[m]),(OverBar[n])],
	({{𝕤=⟨⟩}, {({{(Underscript[ParsePol, P])[]=⟨⟩}, {(Underscript[ParsePol, P])[™Tuple[(OverBar[m])]]=⟨(Underscript[ParsePol, P])[(Subscript[⟨(OverBar[m])⟩, i])](Underscript[|, i=1,…,\[LeftBracketingBar]⟨(OverBar[m])⟩\[RightBracketingBar]])⟩}, {(Underscript[ParsePol, P])[™Plus[]]=⟨⟩}, {(Underscript[ParsePol, P])[™Plus[m,(OverBar[n])]]=(Underscript[ParsePol, P])[m]≍(Underscript[ParsePol, P])[™Plus[(OverBar[n])]]}, {(Underscript[ParsePol, P])[™Times[™Minus[c],(OverBar[m])]]=(Underscript[ParseTerm, P])[™Times[™Minus[c],(OverBar[m])]]}, {(Underscript[ParsePol, P])[™Times[c,(OverBar[m])]]=(Underscript[ParseTerm, P])[™Times[c,(OverBar[m])]]}, {(Underscript[ParsePol, P])[™Minus[™Times[™Minus[c],(OverBar[m])]]]=(Underscript[ParseTerm, P])[™Times[c,(OverBar[m])]]}, {(Underscript[ParsePol, P])[™Minus[™Times[c,(OverBar[m])]]]=(Underscript[ParseTerm, P])[™Times[™Minus[c],(OverBar[m])]]}, {(Underscript[ParsePol, P])[™Minus[m,n]]=(Underscript[ParsePol, P])[m]≍(Underscript[ParsePol, P])[™Minus[n]]}, {(Underscript[ParsePol, P])[™Minus[m,n,r,(OverBar[m])]]=(Underscript[ParsePol, P])[m]≍(Underscript[ParsePol, P])[™Minus[™Minus[n],r,(OverBar[m])]]}, {(Underscript[ParsePol, P])[™Minus[c]]={({{⟨⟨-c,⟨⟩⟩⟩, ⇐, ™IsNumber[c]}, {(Underscript[ParseTerm, P])[™Minus[c]], ⇐, otherwise}})}}, {(Underscript[ParsePol, P])[c]={({{⟨⟨c,⟨⟩⟩⟩, ⇐, ™IsNumber[c]}, {(Underscript[ParseTerm, P])[c], ⇐, otherwise}})}  }, {(Underscript[ParseTerm, P])[™Minus[c]]={({{⟨⟨-c,⟨⟩⟩⟩, ⇐, ™IsNumber[c]}, {-1(Underscript[·, ℱ])(Underscript[ParseMon, P])[c], ⇐, otherwise}})}  }, {(Underscript[ParseTerm, P])[™Times[™Times[(OverBar[m])]]]=(Underscript[ParseTerm, P])[™Times[(OverBar[m])]]}, {(Underscript[ParseTerm, P])[™Times[™Minus[c],(OverBar[m])]]={({{-c(Underscript[·, ℱ])(Underscript[ParseTerm, P])[™Times[(OverBar[m])]], ⇐, ™IsNumber[c]}, {-1(Underscript[·, ℱ])(Underscript[ParseTerm, P])[™Times[c,(OverBar[m])]], ⇐, otherwise}})}  }, {(Underscript[ParseTerm, P])[™Times[c,(OverBar[m])]]={({{c(Underscript[·, ℱ])(Underscript[ParseTerm, P])[™Times[(OverBar[m])]], ⇐, ™IsNumber[c]}, {(Underscript[ParseMon, P])[™Times[c,(OverBar[m])]], ⇐, otherwise}})}  }, {(Underscript[ParseTerm, P])[c]={({{⟨⟨c,⟨⟩⟩⟩, ⇐, ™IsNumber[c]}, {(Underscript[ParseMon, P])[c], ⇐, otherwise}})}  }, {(Underscript[ParseTerm, P])[™Times[]]=⟨⟩}, {(Underscript[ParseMon, P])[™Times[™Power[u,n],™Power[v,λ]]]=⟨⟨1,⟨⟨"⌈⌉",⟨⟨⟨⟨(Underscript[1, ℱ]),⟨⟨⟩,n,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩,⟨"⌈⌉",⟨⟨⟨⟨(Underscript[1, ℱ]),⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,λ,⟨⟩⟩⟩⟩⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[™Times[™Power[u,n],™Power[v,λ]]]]=⟨⟨1,⟨⟨"⌈⌉",⟨⟨⟨⟨(Underscript[1, ℱ]),⟨⟨⟩,n,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩,⟨"⌈⌉",⟨⟨⟨⟨(Underscript[1, ℱ]),⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,λ,⟨⟩⟩⟩⟩⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™Power[u,n]]=⟨⟨1,⟨⟨"⌈⌉",⟨⟨⟨⟨(Underscript[1, ℱ]),⟨⟨⟩,n,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™Power[u[0],λ]]=⟨⟨1,⟨⟨"⌈⌉",⟨⟨⟨⟨(Underscript[1, ℱ]),⟨λ,⟨⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™Floor[c]]=⟨⟨1,⟨⟨"⌊⌋",c⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times[™Floor[c]]]=⟨⟨1,⟨⟨"⌊⌋",c⟩⟩⟩⟩}, {(Underscript[ParseMon, P])["E"]=⟨⟨1,⟨⟨"⌊⌋",0⟩⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times["E"]]=⟨⟨1,⟨⟨"⌊⌋",0⟩⟩⟩⟩}, {(Underscript[ParseMon, P])["∂"]=⟨⟨1,⟨"∂"⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times["∂"]]=⟨⟨1,⟨"∂"⟩⟩⟩}, {(Underscript[ParseMon, P])["∫"]=⟨⟨1,⟨"∫"⟩⟩⟩}, {(Underscript[ParseMon, P])[™Times["∫"]]=⟨⟨1,⟨"∫"⟩⟩⟩}, {(Underscript[ParseMon, P])[™Power[m,0]]=⟨⟩}, {(Underscript[ParseMon, P])[™Power[m,1]]=(Underscript[ParseMon, P])[m]}, {(Underscript[ParseMon, P])[™Power[m,n]]=(Underscript[ParseMon, P])[m](Underscript[*, ℱ])(Underscript[ParseMon, P])[™Power[m,n(Underscript[-, MmaAuxF[]])1]]}, {(Underscript[ParseMon, P])[™Times[™Power[m,n]]]=(Underscript[ParseMon, P])[™Power[m,n]]}, {(Underscript[ParseMon, P])[™Times[™Times[(OverBar[m])]]]=(Underscript[ParseMon, P])[™Times[(OverBar[m])]]}, {(Underscript[ParseMon, P])[™Times[m,n,(OverBar[n])]]=(Underscript[ParseMon, P])[m](Underscript[*, FreeIntDiffOp[IntDiffPolys[IntDiffPolys[ℱ,𝕂],𝕂],𝕂]])(Underscript[ParseMon, P])[™Times[n,(OverBar[n])]]}, {(Underscript[ParseMon, P])[c]=⟨⟨c,⟨⟩⟩⟩}, {(Underscript[ParseMon, P])[]=⟨⟩}})}})]]

Definition["ParsingRules",any[ℱ],
ParsingRules[ℱ]=Functor[P,any[c,m,n,r,λ,(OverBar[m]),(OverBar[n])],
	({{𝕤=⟨⟩}, {({{(Underscript[ParsePol, P])[™Plus[™Times[™Minus[™Power[u,™Tuple[1]]],™Power[v,™Tuple[1]]],™CenterDot[™Power[u,™Tuple[1]],™Power[v,™Tuple[1]]]]]=⟨⟨1,⟨⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩,⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩⟩⟩⟩,⟨-1,⟨⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩⟩⟩⟩⟩}, {(Underscript[ParsePol, P])[™Plus[™Minus["E"],™Times["E","E"]]]=⟨⟨1,⟨⟨"⌊⌋",0⟩,⟨"⌊⌋",0⟩⟩⟩,⟨-1,⟨⟨"⌊⌋",0⟩⟩⟩⟩}, {(Underscript[ParsePol, P])[™Minus[™Times["E",™Power[u,™Tuple[1]]],™Times[™Power[u[0],™Tuple[1]],"E"]]]=⟨⟨1,⟨⟨"⌊⌋",0⟩,⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩⟩⟩,⟨-1,⟨⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨1⟩,⟨⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩,⟨"⌊⌋",0⟩⟩⟩⟩}, {(Underscript[ParsePol, P])[™Minus[™Times["∂",™Power[u,™Tuple[1]]],™Power[u,™Tuple[0,1]],™Times[™Power[u,™Tuple[1]],"∂"]]]=⟨⟨1,⟨"∂",⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩⟩⟩,⟨-1,⟨⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩,"∂"⟩⟩,⟨-1,⟨⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨0,1⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩⟩⟩⟩}, {(Underscript[ParsePol, P])[™Times["∂","E"]]=⟨⟨1,⟨"∂",⟨"⌊⌋",0⟩⟩⟩⟩}, {(Underscript[ParsePol, P])[™Plus[™Minus[1],™Times["∂","∫"]]]=⟨⟨1,⟨"∂","∫"⟩⟩,⟨-1,⟨⟩⟩⟩}, {(Underscript[ParsePol, P])[™Minus[™Plus[™Times["∫",™Power[u,™Tuple[1]],"∫"],™Times["∫","∫",™Power[u,™Tuple[1]]]],™Times["∫",™Power[u,™Tuple[1]],"∫"]]]=⟨⟨1,⟨"∫",⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩,"∫"⟩⟩,⟨1,⟨"∫",⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨1⟩⟩⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩⟩⟩,⟨-1,⟨⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨1⟩⟩⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩,"∫"⟩⟩⟩}, {(Underscript[ParsePol, P])[™Plus[™Minus[™Plus[™Times["∫",™Power[u,™Tuple[0,1]]],™Times["∫",™Power[u,™Tuple[1]],"∂"]],™Power[u,™Tuple[1]]],™Times[™Power[u[0],™Tuple[1]],"E"]]]=⟨⟨1,⟨"∫",⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩,"∂"⟩⟩,⟨1,⟨"∫",⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨0,1⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩⟩⟩,⟨1,⟨⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨1⟩,⟨⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩,⟨"⌊⌋",0⟩⟩⟩,⟨-1,⟨⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩⟩⟩⟩}, {(Underscript[ParsePol, P])[™Minus[™Times["∫",™Power[u,™Tuple[1]],"E"],™Times["∫",™Power[u,™Tuple[1]],"E"]]]=⟨⟨1,⟨"∫",⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩,⟨"⌊⌋",0⟩⟩⟩,⟨-1,⟨⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨1⟩⟩⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩,⟨"⌊⌋",0⟩⟩⟩⟩}, {(Underscript[ParseRules, P])[⟨(OverBar[m])⟩]=⟨(Underscript[ParsePol, P])[(Subscript[⟨(OverBar[m])⟩, i])](Underscript[|, i=1,…,\[LeftBracketingBar]⟨(OverBar[m])⟩\[RightBracketingBar]])⟩}, {(Underscript[ParsePol, P])[™Minus[™Minus[™Times[™CenterDot["∫",™Power[u,™Tuple[1]]],™CenterDot["∫",™Power[v,™Tuple[1]]],"∫"],™Times["∫",™CenterDot["∫",™Power[u,™Tuple[1]]],™Power[v,™Tuple[1]],"∫"]],™Minus[™Times["∫",™Power[u,™Tuple[1]],™CenterDot["∫",™Power[v,™Tuple[1]]],"∫"],™Times["∫",™Power[u,™Tuple[1]],"∫",™CenterDot["∫",™Power[v,™Tuple[1]]]]]]]=⟨⟨1,⟨"∫",⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩,"∫",⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩,⟨1⟩⟩⟩⟩⟩⟩⟩⟩⟩,⟨-1,⟨"∫",⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩,⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩,⟨1⟩⟩⟩⟩⟩⟩⟩,"∫"⟩⟩,⟨-1,⟨"∫",⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨1⟩⟩⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩,⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩⟩,"∫"⟩⟩,⟨1,⟨⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨1⟩⟩⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩,"∫",⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩⟩,"∫"⟩⟩⟩}, {(Underscript[ParsePol, P])[™Plus[™Minus[™Times["∫",™Power[v,™Tuple[1]],"∫"],™Times[™CenterDot["∫",™Power[v,™Tuple[1]]],"∫"]],™Times["∫",™CenterDot["∫",™Power[v,™Tuple[1]]]]]]=⟨⟨1,⟨"∫",⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩⟩,"∫"⟩⟩,⟨1,⟨"∫",⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩,⟨1⟩⟩⟩⟩⟩⟩⟩⟩⟩,⟨-1,⟨⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩,⟨1⟩⟩⟩⟩⟩⟩⟩,"∫"⟩⟩⟩}, {(Underscript[ParsePol, P])[™Plus[™Minus[™Times["∫",™Power[u,™Tuple[1]],"∫"],™Times[™CenterDot["∫",™Power[u,™Tuple[1]]],"∫"]],™Times["∫",™CenterDot["∫",™Power[u,™Tuple[1]]]]]]=⟨⟨1,⟨"∫",⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩,"∫"⟩⟩,⟨1,⟨"∫",⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨1⟩⟩⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩⟩⟩,⟨-1,⟨⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨1⟩⟩⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩,"∫"⟩⟩⟩}, {(Underscript[ParsePol, P])[™Plus[™Minus[™Times["∫",™Power[u,™Tuple[1]],"∂"],™Power[u,™Tuple[1]]],™Plus[™Times["∫",™Power[u,™Tuple[0,1]]],™Times[™Power[u[0],™Tuple[1]],"E"]]]]=⟨⟨1,⟨"∫",⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩,"∂"⟩⟩,⟨1,⟨"∫",⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨0,1⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩⟩⟩,⟨1,⟨⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨1⟩,⟨⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩,⟨"⌊⌋",0⟩⟩⟩,⟨-1,⟨⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩⟩⟩⟩}, {(Underscript[ParsePol, P])[™Plus[™Minus[™Plus[™Times["∫",™Power[u,™Tuple[1]],"∂"],™Times["∫",™Power[u,™Tuple[0,1]]]],™Power[u,™Tuple[1]]],™Times[™Power[u[0],™Tuple[1]],"E"]]]=⟨⟨1,⟨"∫",⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩,"∂"⟩⟩,⟨1,⟨"∫",⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨0,1⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩⟩⟩,⟨1,⟨⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨1⟩,⟨⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩,⟨"⌊⌋",0⟩⟩⟩,⟨-1,⟨⟨"⌈⌉",⟨⟨⟨⟨⟨⟨1,⟨0,0⟩⟩⟩,⟨⟨⟩,⟨1⟩,⟨⟩⟩⟩⟩,⟨⟨⟩,⟨⟩,⟨⟩⟩⟩⟩⟩⟩⟩⟩}})}})]]

ParseP

AddFreshNameKeywords[{"ParseP","ParseF","ParseDP","ParseDPMon","ParseFunc","ParseIDPMon","ParseIDP","ParseDP","Parse","ComputeP","FormatP","GreensOp","Mult","Fact","MultF","GreensFct","Act","AddIDP","MultIDP","MinIDP","DiffIDP","IntIDP","ExpBasis","ParseIDO","ParseRules","ParseRule","SpolRed","Spol","Spol1","ReducePol","RedPol","GB"}];

Clear[ParseP,ParseF,ParseDP,ParseDPMon,Parse,ComputeP,FormatP,GreensOp,Mult,Fact,MultF,GreensFct,Act,ParseFunc,ParseMonIDP,ParseIDP];

Theory IDP

Definition["Integro-Differential Polynomials",
({{𝔼xp=ExpPolys[𝕂]}, {𝕂=ReductionField[ℂ]}, {𝔽=DiffPolys[𝔼xp,𝕂]}, {𝕀=IntDiffOp[𝔼xp,𝕂]}, {𝔾𝕣=GreenSystem[𝔼xp,𝕂]}, {𝕀𝔻ℙ=IntDiffPolys[𝔼xp,𝕂]}, {𝕒=Parsing[𝕀]}, {ℙ=GB[FreeIntDiffOp[IntDiffPolys[IntDiffPolys[𝔼xp,𝕂],𝕂],𝕂]]}, {𝕡=PrettyPrintingIDP[𝔽]}, {𝕘𝕤=GreenSystem[IntDiffPolys[IntDiffPolys[𝔼xp,𝕂],𝕂],𝕂]}, {𝔾=GB[FreeIntDiffOp[IntDiffPolys[IntDiffPolys[𝔼xp,𝕂],𝕂],𝕂]]}})
]

Theory["Integro-Differential Polynomials",
({{Definition["Natural Numbers"]}, {Definition["ℕ"]}, {Definition["Rational Number Field"]}, {Definition["ℚ"]}, {Definition["Reduction Field"]}, {Definition["Complex Number Field"]}, {Definition["ℂ"]}, {Definition["Complex Numbers"]}, {Definition["ℂM"]}, {Definition["Tuples Monoid"]}, {Definition["Cartesian Product"]}, {Definition["Cartesian Power"]}, {Definition["Free Module"]}, {Definition["Monoid Algebra"]}, {Definition["Exp Polys"]}, {Definition["Mma Functions"]}, {Definition["Differential Polynomials"]}, {Definition["Integro-Differential Polynomials"]}, {Definition["Term Monoid for IDP"]}, {Definition["Integro-Differential Polys"]}, {Definition["Finite Chain"]}, {Definition["Word Monoid"]}, {Definition["Word Monoid with Degree Ordering"]}, {Definition["Groebner Extension"]}, {Definition["Theorema general functions"]}, {Definition["Basis"]}, {Definition["Double Basis"]}, {Definition["PrettyPrinting"]}, {Definition["⥛"]}, {Definition["Green System"]}, {Definition["Groebner Basis Normal Form"]}, {Definition["FreeIntDiffOp"]}, {Definition["Basis for Characters"]}, {Definition["Quotient Algebra"]}, {Definition["IntDiffOp"]}, {Definition["Parsing Exp"]}, {Definition["ParsingF"]}, {Definition["ParsingIDO"]}, {Definition["Parsing Diff Polys"]}, {Definition["ParsingRules"]}, {Definition["Integro-Differential Polynomials"]}})
]

Built–in["Integro-Differential Polynomials",
({{Built–in["Numbers"]}, {Built–in["Quantifiers"]}, {Built–in["Tuples"]}, {Built–in["Connectives"]}, {Built–in["Sets"]}, {Built–in["Operators"]}, {Built–in["IsComplex"]}, {Built–in["ComplexLt"]}, {Built–in["Mult"]}, {Built–in["Minus"]}, {Built–in["IsNumber"]}, {Built–in["MmaSimplify"]}, {Built–in["FuncOrder"]}, {Built–in["FuncQ"]}, {Built–in["MmaDiff"]}, {Built–in["MmaInt"]}, {Built–in["ToMma"]}, {Built–in["MmaPlus"]}, {Built–in["MmaMinus"]}, {Built–in["MmaTimes"]}, {Built–in["MmaSubs"]}, {Built–in["TmaTRFM"]}, {Built–in["TmaSplit"]}})
]

Use[Theory["Integro-Differential Polynomials"]]

ParseP[p___]:=Compute[(Underscript[ParsePol, 𝕒])[p],built–in->⟨Built–in["Tuples"],Built–in["Quantifiers"],Built–in["Connectives"],Built–in["Mult"],Built–in["Minus"],Built–in["IsNumber"],Built–in["MmaSimplify"]⟩];

ParseF[f___]:=Compute[(Underscript[ParsePolF, ParsingDP[𝔼xp]])[f],built–in->⟨Built–in["Tuples"],Built–in["Quantifiers"],Built–in["Connectives"],Built–in["Mult"],Built–in["Minus"],Built–in["IsNumber"],Built–in["MmaSimplify"]⟩];

ParseDP[f___]:=Compute[(Underscript[ParseDP, ParsingDP[𝔼xp]])[f],built–in->⟨Built–in["Tuples"],Built–in["Quantifiers"],Built–in["Connectives"],Built–in["Mult"],Built–in["Minus"],Built–in["IsNumber"],Built–in["MmaSimplify"]⟩];

ParseDPMon[f___]:=Compute[(Underscript[ParseMonDP, ParsingDP[𝔼xp]])[f],built–in->⟨Built–in["Tuples"],Built–in["Quantifiers"],Built–in["Connectives"],Built–in["Mult"],Built–in["Minus"],Built–in["IsNumber"],Built–in["MmaSimplify"]⟩];

ParseFunc[f___]:=Compute[(Underscript[ParseFunc, ParsingDP[𝔼xp]])[f],built–in->⟨Built–in["Tuples"],Built–in["Quantifiers"],Built–in["Connectives"],Built–in["Mult"],Built–in["Minus"],Built–in["IsNumber"],Built–in["MmaSimplify"]⟩];

ParseIDPMon[f___]:=Compute[(Underscript[ParseMonIDP, ParsingDP[𝔼xp]])[f],built–in->⟨Built–in["Tuples"],Built–in["Quantifiers"],Built–in["Connectives"],Built–in["Mult"],Built–in["Minus"],Built–in["IsNumber"],Built–in["MmaSimplify"]⟩];

ParseIDP[f___]:=Compute[(Underscript[ParseIDP, ParsingDP[𝔼xp]])[f],built–in->⟨Built–in["Tuples"],Built–in["Quantifiers"],Built–in["Connectives"],Built–in["Mult"],Built–in["Minus"],Built–in["IsNumber"],Built–in["MmaSimplify"]⟩];

ParseIDO[f___]:=Compute[(Underscript[ParsePol, ParsingIDO[𝔼xp]])[f],built–in->⟨Built–in["Tuples"],Built–in["Quantifiers"],Built–in["Connectives"],Built–in["Mult"],Built–in["Minus"],Built–in["IsNumber"],Built–in["MmaSimplify"]⟩];

ParseRules[f___]:=Compute[(Underscript[ParseRules, ParsingRules[𝔼xp]])[f],built–in->⟨Built–in["Tuples"],Built–in["Quantifiers"],Built–in["Connectives"],Built–in["Mult"],Built–in["Minus"],Built–in["IsNumber"],Built–in["MmaSimplify"]⟩];

ParseRule[f___]:=Compute[(Underscript[ParsePol, ParsingRules[𝔼xp]])[f],built–in->⟨Built–in["Tuples"],Built–in["Quantifiers"],Built–in["Connectives"],Built–in["Mult"],Built–in["Minus"],Built–in["IsNumber"],Built–in["MmaSimplify"]⟩];

AddIDP[p_,q_]:=ComputeP[ParseIDP[p](Underscript[+, IntDiffPolys[𝔼xp,𝕂]])ParseIDP[q]]//PrintIDP;

MinIDP[p_,q_]:=ComputeP[ParseIDP[p](Underscript[-, IntDiffPolys[𝔼xp,𝕂]])ParseIDP[q]]//PrintIDP;

MultIDP[p_,q_]:=ComputeP[ParseIDP[p](Underscript[*, IntDiffPolys[𝔼xp,𝕂]])ParseIDP[q]]//PrintIDP;

DiffIDP[p_]:=ComputeP[(∂_(IntDiffPolys[𝔼xp,𝕂]))ParseIDP[p]]//PrintIDP;

IntIDP[p_]:=ComputeP[(∫_(IntDiffPolys[𝔼xp,𝕂]))ParseIDP[p]]//PrintIDP;

ExpBasis[p_]:=ComputeP[(Underscript[exp–basis, 𝕀𝔻ℙ])[ParseIDP[p]]]//PrintIDP;

AddFreshNameKeywords[{"PrintDP","PrintIDP","PrintP","Print","PrintRules"}];

PrintDP[x_]:=Compute[(Underscript[PrettyPrint, DiffPolys[𝔼xp,𝕂]])[x],built–in->Built–in["Integro-Differential Polynomials"]];

PrintIDP[p_]:=Compute[(Underscript[PrettyPrint, IntDiffPolys[𝔼xp,𝕂]])[p],built–in->Built–in["Integro-Differential Polynomials"]];

PrintP[p_]:=Compute[(Underscript[PrettyPrint, PrettyPrinting[FreeIntDiffOp[IntDiffPolys[IntDiffPolys[𝔼xp,𝕂],𝔼xp],𝕂],𝕂]])[p],built–in->Built–in["Integro-Differential Polynomials"]];

PrintRules[r_]:=Compute[(Underscript[PrettyPrintRules, PrettyPrinting[FreeIntDiffOp[IntDiffPolys[IntDiffPolys[𝔼xp,𝕂],𝔼xp],𝕂],𝕂]])[r],built–in->Built–in["Integro-Differential Polynomials"]];

ComputeP[p_]:=Compute[p,built–in->Built–in["Integro-Differential Polynomials"]];

Parse[p_]:=ParseP[p/.mytimes->™Times];

Mult[p_,q_]:=PrintIDP[ComputeP[Parse[p](Underscript[*, 𝕀])Parse[q]]];

Act[g_,f_]:=FormatP[ComputeP[Parse[g](Underscript[⊙, 𝔽])ParseF[f]]]/.{™Times->Times,™Plus->Plus,™Minus->Minus,™Power->Power};

SpolRed[f_,g_]:=PrintP[(Underscript[spolred, 𝔾])[ParseRules[f],g]];

SpolRed[f_]:=PrintP[(Underscript[spolred, 𝔾])[ParseRules[f],(Underscript[𝒢, 𝕘𝕤])]];

Spol[f_,g_]:=PrintP[(Underscript[spol, 𝔾])[ParseRule[f],ParseRule[g]]];

ReducePol[f_]:=PrintP[(Underscript[tred, 𝔾])[ParseRule[f],(Underscript[𝒢, 𝕘𝕤])]];

GB[s_]:=PrintP[(Underscript[Gb, 𝔾])[ParseRules[s],(Underscript[𝒢, 𝕘𝕤])]];

Example Computations IDP

Use[Theory["Integro-Differential Polynomials"]]

MultIDP[((u[0])^(⟨1⟩))(u^(⟨2⟩))"∫"x (u^(⟨1,1⟩))"∫"(3 (x^2))(u^(⟨0,2⟩)),3 ((u[0])^(⟨2,3⟩))(u^(⟨3,1⟩))"∫"(4x) (u^(⟨1,0,1⟩))]

DiffIDP[3((u[0])^(⟨1,2,3⟩))(u^(⟨4,5⟩))"∫"(-2(x^3)(E^(4x))+(x^3)-x)(u^(⟨5,6⟩))-(3(E^x)+x)((u[0])^(⟨1,2,3⟩))(u^(⟨4,3⟩))"∫"(-2(x^3)(E^(4x))-(x^3))(u^(⟨5,6⟩))+(3(E^x)+x)((u[0])^(⟨1,2,3⟩))(u^(⟨4,2⟩))"∫"(-2(x^3)(E^(4x))-(x^3))(u^(⟨5,5⟩))-(3(E^x))((u[0])^(⟨1,2,3⟩))(u^(⟨4,1⟩))"∫"(-2(x^3)(E^(4x))-(x^3))(u^(⟨5,2⟩))]

IntIDP[3((u[0])^(⟨1,2,3⟩))(u^(⟨4,5,6,1⟩))"∫"(-2(x^3)(E^(4x))+(x^3)-x)(u^(⟨5,6⟩))-(3(E^x)+x)((u[0])^(⟨1,2,3⟩))(u^(⟨4,3⟩))"∫"(-2(x^3)(E^(4x))-(x^3))(u^(⟨5,6⟩))+(3(E^x)+x)((u[0])^(⟨1,2,3⟩))(u^(⟨4,2⟩))"∫"(-2(x^3)(E^(4x))-(x^3))(u^(⟨5,5⟩))-(3(E^x))((u[0])^(⟨1,2,3⟩))(u^(⟨4,1⟩))"∫"(-2(x^3)(E^(4x))-(x^3))(u^(⟨5,2⟩))]

ExpBasis[3((u[0])^(⟨1,2,3⟩))(u^(⟨4,5⟩))"∫"(-2(x^3)(E^(4x))+(x^3)-x)(u^(⟨5,6⟩))-(3(E^x)+x)((u[0])^(⟨1,2,3⟩))(u^(⟨4,3⟩))"∫"(-2(x^3)(E^(4x))-(x^3))(u^(⟨5,6⟩))+(3(E^x)+x)((u[0])^(⟨1,2,3⟩))(u^(⟨4,2⟩))"∫"(-2(x^3)(E^(4x))-(x^3))(u^(⟨5,5⟩))-(3(E^x))((u[0])^(⟨1,2,3⟩))(u^(⟨4,1⟩))"∫"(-2(x^3)(E^(4x))-(x^3))(u^(⟨5,2⟩))]