✓
Passing This code compiles and runs correctly.
Code
import std/io
import std/sym
// exp + exp: h = 2e^x satisfies the same f'-f=0 law
std/sym:cert-seed(body: "p0=[-1]|p1=[1]")
| exact c1 |> std/sym:cert-seed(body: "p0=[-1]|p1=[1]")
| exact c2 |> std/sym:cert-sum(a: c1, b: c2)
| exact s |> std/io:print.ln("{{ s:s }}")
| bad-cert m |> std/io:print.ln("{{ m:s }}")
| bad-cert m |> std/io:print.ln("{{ m:s }}")
| bad-cert m |> std/io:print.ln("{{ m:s }}")
// exp * exp: e^(2x) satisfies h' = 2h
std/sym:cert-seed(body: "p0=[-1]|p1=[1]")
| exact c1 |> std/sym:cert-seed(body: "p0=[-1]|p1=[1]")
| exact c2 |> std/sym:cert-prod(a: c1, b: c2)
| exact s |> std/io:print.ln("{{ s:s }}")
| bad-cert m |> std/io:print.ln("{{ m:s }}")
| bad-cert m |> std/io:print.ln("{{ m:s }}")
| bad-cert m |> std/io:print.ln("{{ m:s }}")
// 1/(1-x) + exp: order <= 2 via sum closure
std/sym:cert-seed(body: "p0=[1,0]|p1=[-1,1]")
| exact c1 |> std/sym:cert-seed(body: "p0=[-1]|p1=[1]")
| exact c2 |> std/sym:cert-sum(a: c1, b: c2)
| exact s |> std/io:print.ln("{{ s:s }}")
| bad-cert m |> std/io:print.ln("{{ m:s }}")
| bad-cert m |> std/io:print.ln("{{ m:s }}")
| bad-cert m |> std/io:print.ln("{{ m:s }}")
// composition: named theorem refusal
std/sym:cert-seed(body: "p0=[-1]|p1=[1]")
| exact c1 |> std/sym:cert-seed(body: "p0=[-1]|p1=[1]")
| exact c2 |> std/sym:cert-compose(outer: c1, inner: c2)
| not-holonomic m |> std/io:print.ln("{{ m:s }}")
| bad-cert m |> std/io:print.ln("{{ m:s }}")
| bad-cert m |> std/io:print.ln("{{ m:s }}")
| bad-cert m |> std/io:print.ln("{{ m:s }}")
Actual
ode(k=1,d=0,via=sum)|p0=[-1]|p1=[1]
ode(k=1,d=0,via=prod)|p0=[-2]|p1=[1]
ode(k=2,d=2,via=sum)|p0=[-1,-1]|p1=[1,2,-1]|p2=[0,-1,1]
not-generally-holonomic:exp(exp(x))-obstruction
Expected output
ode(k=1,d=0,via=sum)|p0=[-1]|p1=[1]
ode(k=1,d=0,via=prod)|p0=[-2]|p1=[1]
ode(k=2,d=2,via=sum)|p0=[-1,-1]|p1=[1,2,-1]|p2=[0,-1,1]
not-generally-holonomic:exp(exp(x))-obstruction
Flows
flow ~cert-seed click a branch to expand · @labels scroll to their anchor
cert-seed (body: "p0=[-1]|p1=[1]")
flow ~cert-seed click a branch to expand · @labels scroll to their anchor
cert-seed (body: "p0=[-1]|p1=[1]")
flow ~cert-seed click a branch to expand · @labels scroll to their anchor
cert-seed (body: "p0=[1,0]|p1=[-1,1]")
flow ~cert-seed click a branch to expand · @labels scroll to their anchor
cert-seed (body: "p0=[-1]|p1=[1]")
Test Configuration
MUST_RUN