Solution in Maude for https://adventofcode.com/2021/day/12

aoc2021d12.maude

fmod PATH is
    protecting STRING .
    protecting BOOL .
    sorts Path Node .
    subsort String < Node .
    op _-_ : Node Node -> Path [ctor comm] .
    op small : Node -> Bool .
    var s : Node .
    eq small(s) = ascii(substr(s, 0, 1)) > 90 .
    
endfm

view Path from TRIV to PATH is
  sort Elt to Path .
endv

fmod DATA is
    protecting SET{Path} .
    op data : -> Set{Path} .
    eq data =
        "GC" - "zi",
        "end" - "zv",
        "lk" - "ca",
        "lk" - "zi",
        "GC" - "ky",
        "zi" - "ca",
        "end" - "FU",
        "iv" - "FU",
        "lk" - "iv",
        "lk" - "FU",
        "GC" - "end",
        "ca" - "zv",
        "lk" - "GC",
        "GC" - "zv",
        "start" - "iv",
        "zv" - "QQ",
        "ca" - "GC",
        "ca" - "FU",
        "iv" - "ca",
        "start" - "lk",
        "zv" - "FU",
        "start" - "zi" .
endfm

mod AOC1 is
    including DATA .
    sorts State Nodes .
    subsort Node < Nodes .
    ops start A b c d end : -> Node [ctor] .
    op <_>[_] : Set{Path} Nodes -> State [ctor] .
    op __ : Nodes Nodes -> Nodes [ctor assoc] .
    op member : Node Nodes -> Bool .
    vars xs : Nodes .
    vars X Y : Node .
    var S : Set{Path} .
    eq member(X , X) = true .
    eq member(X , Y) = false .
    eq member(X , X xs) = true .
    eq member(X , Y xs) = member(X , xs) [owise] .
    rl [first] : < (X - Y) , S >[ X ] => < (X - Y) , S >[ X Y ] .
    crl [next] : < (X - Y) , S >[ xs X ] => < (X - Y) , S >[ xs X Y ]
      if not(small(Y)) .
    crl [next-s] : < (X - Y) , S >[ xs X ] => < (X - Y) , S >[ xs X Y ]
      if small(Y) and not(member(Y,xs)) .
endm

mod AOC2 is
    including DATA .
    sorts State Nodes .
    subsort Node < Nodes .
    ops start A b c d end : -> Node [ctor] .
    op [_]<_>[_] : Bool Set{Path} Nodes -> State [ctor] .
    op __ : Nodes Nodes -> Nodes [ctor assoc] .
    op count : Node Nodes -> Nat .
    vars xs : Nodes .
    vars X Y : Node .
    var S : Set{Path} .
    var B : Bool .
    eq count(X , X) = 1 .
    eq count(X , Y) = 0 .
    eq count(X , X xs) = 1 + count(X , xs) .
    eq count(X , Y xs) = count(X , xs) [owise] .
    rl [first] : [ B ]< (X - Y) , S >[ X ] => [ B ]< (X - Y) , S >[ X Y ] .
    crl [next] : [ B ]< (X - Y) , S >[ xs X ] => [ B ]< (X - Y) , S >[ xs X Y ]
      if not(small(Y)) and not(X == "end") .
    crl [next-s] : [ false ]< (X - Y) , S >[ xs X ] => [ count(Y,xs) > 0 ]< (X - Y) , S >[ xs X Y ]
      if small(Y) and (count(Y,xs) < 2) and not(Y == "start") and not(X == "end") .
    crl [next-b] : [ true ]< (X - Y) , S >[ xs X ] => [ true ]< (X - Y) , S >[ xs X Y ]
      if small(Y) and (count(Y,xs) < 1) and not(Y == "start") and not(X == "end") .
endm

*** search [ false ]<  >["start"] =>+ [ B:Bool ]< S:Set{Path} > [ "start" xs:Nodes "end" ] .
*** search [ false ]< "start" - "A" , "start" - "b", "A" - "c", "A" - "b", "b" - "d", "A" - "end", "b" - "end" >["start"] =>+ [ B:Bool ]< S:Set{Path} >[ "start" xs:Nodes "end" ] .

search in AOC2 : [ false ]< data >["start"] =>+
  [ B:Bool ]< S:Set{Path} >[ "start" xs:Nodes "end" ] .

quit

$ time { maude -batch foo.maude > z }
1m8.325152312s