folds.txt

    rule Foldl-0 {
      foldl $f $init ∅ = $init
    }

    rule Foldl-N {
      $init $f $head = $init' / foldl $f $init' $tail = $res
      ------------------------------------------------------
                foldl $f $init ($head $tail) = $res
    }

    rule Foldr-0 {
      foldr $f $init ∅ = $init
    }

    rule Foldr-N {
      foldr $f $init $tail = $init' / $head $f $init' = $res
      ------------------------------------------------------
                foldr $f $init ($head $tail) = $res
    }

    rule Cons {
      $head : $tail = ($head $tail)
    }

    rule Concat {
      foldr : $b $a = $c
      ------------------
         $a ++ $b = $c
    }

    prove { (a (b ∅)) ++ (c (d (e ∅))) = $x }

    prove { foldl ++ ∅ ((a ∅)
                       ((b (c ∅))
                       ((d (e (f ∅)))
                       ∅)))
                       = $x }

output.txt

prove { (a (b ∅)) ++ (c (d (e ∅))) = $x }

    ─────────────────────────────────────── Foldr-0   ───────────────────────────────────── Cons
    foldr : (c (d (e ∅))) ∅ = (c (d (e ∅)))           b : (c (d (e ∅))) = (b (c (d (e ∅))))
    ─────────────────────────────────────────────────────────────────────────────────────── Foldr-N   ───────────────────────────────────────────── Cons
                        foldr : (c (d (e ∅))) (b ∅) = (b (c (d (e ∅))))                               a : (b (c (d (e ∅)))) = (a (b (c (d (e ∅)))))
                        ─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── Foldr-N
                                                          foldr : (c (d (e ∅))) (a (b ∅)) = (a (b (c (d (e ∅)))))
                                                          ─────────────────────────────────────────────────────── Concat
                                                            (a (b ∅)) ++ (c (d (e ∅))) = (a (b (c (d (e ∅)))))


prove { foldl ++ ∅ ((a ∅)
                       ((b (c ∅))
                       ((d (e (f ∅)))
                       ∅)))
                       = $x }

                                                                                                                        ─────────────────────────────────────── Foldr-0   ───────────────────────────────────── Cons
                                                                                                                        foldr : (d (e (f ∅))) ∅ = (d (e (f ∅)))           c : (d (e (f ∅))) = (c (d (e (f ∅))))
                                                                                                                        ─────────────────────────────────────────────────────────────────────────────────────── Foldr-N   ───────────────────────────────────────────── Cons
                                                                                                                                            foldr : (d (e (f ∅))) (c ∅) = (c (d (e (f ∅))))                               b : (c (d (e (f ∅)))) = (b (c (d (e (f ∅)))))
                                                                                                                                            ─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── Foldr-N   ───────────────────────────────────────────────────── Cons
                                                                                                                                                                              foldr : (d (e (f ∅))) (b (c ∅)) = (b (c (d (e (f ∅)))))                                             a : (b (c (d (e (f ∅))))) = (a (b (c (d (e (f ∅))))))
                                      ─────────────────────────────── Foldr-0   ───────────────────────────── Cons                                                            ───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── Foldr-N
                                      foldr : (b (c ∅)) ∅ = (b (c ∅))           a : (b (c ∅)) = (a (b (c ∅)))                                                                                                              foldr : (d (e (f ∅))) (a (b (c ∅))) = (a (b (c (d (e (f ∅))))))
                                      ─────────────────────────────────────────────────────────────────────── Foldr-N                                                                                                      ─────────────────────────────────────────────────────────────── Concat                                                 ──────────────────────────────────────────────────────────────── Foldl-0
                                                      foldr : (b (c ∅)) (a ∅) = (a (b (c ∅)))                                                                                                                                (a (b (c ∅))) ++ (d (e (f ∅))) = (a (b (c (d (e (f ∅))))))                                                           foldl ++ (a (b (c (d (e (f ∅)))))) ∅ = (a (b (c (d (e (f ∅))))))
    ─────────────────────── Foldr-0                   ─────────────────────────────────────── Concat                                                                                                                         ───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── Foldl-N
    foldr : (a ∅) ∅ = (a ∅)                             (a ∅) ++ (b (c ∅)) = (a (b (c ∅)))                                                                                                                                                                                           foldl ++ (a (b (c ∅))) ((d (e (f ∅))) ∅) = (a (b (c (d (e (f ∅))))))
    ─────────────────────── Concat                      ───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── Foldl-N
      ∅ ++ (a ∅) = (a ∅)                                                                                                                                            foldl ++ (a ∅) ((b (c ∅)) ((d (e (f ∅))) ∅)) = (a (b (c (d (e (f ∅))))))
      ────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────── Foldl-N
                                                                                   foldl ++ ∅ ((a ∅) ((b (c ∅)) ((d (e (f ∅))) ∅))) = (a (b (c (d (e (f ∅))))))