JSONRenderLexProof.number_tail_acc: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend as JSONRenderLexProof
Lines 90-145 of qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend&start_line=90&end_line=145

import Base
import qasim-bend-kit@0.1.0.2/libs/JSON.bend as J
import qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend as Num
import qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend as S

def number_tail_acc(+text: String,
                    +state: J.NumberState,
                    +rev_head: Char,
                    +rev_tail: String,
                    +first: Char,
                    +prefix_tail: String,
                    +acc: List<&2, J.Lexeme>,
                    +reverse_prefix: {String.reverse(SCon{rev_head, rev_tail}) == SCon{first, prefix_tail} : String},
                    +evidence: {J.number_valid_end(J.number_valid_step(text, state)) == True{} : Bool}) -> {J.lex_scan(text, J.Outside{}, SCon{rev_head, rev_tail}, acc) == (List.reverse(&2, J.Lexeme, J.Payload{SCon{first, prefix_tail} ++ text} <> acc)) : List<&2, J.Lexeme>}:
    match text:
        case SNil{}:
            Equal.trans(List<&2, J.Lexeme>,
                J.lex_scan(SNil{}, J.Outside{}, SCon{rev_head, rev_tail}, acc),
                List.reverse(&2, J.Lexeme, J.Payload{String.reverse(SCon{rev_head, rev_tail})} <> acc),
                List.reverse(&2, J.Lexeme, J.Payload{SCon{first, prefix_tail} ++ SNil{}} <> acc),
                {==},
                Equal.trans(List<&2, J.Lexeme>,
                    List.reverse(&2, J.Lexeme, J.Payload{String.reverse(SCon{rev_head, rev_tail})} <> acc),
                    List.reverse(&2, J.Lexeme, J.Payload{SCon{first, prefix_tail}} <> acc),
                    List.reverse(&2, J.Lexeme, J.Payload{SCon{first, prefix_tail} ++ SNil{}} <> acc),
                    Equal.cong(String, List<&2, J.Lexeme>, s => List.reverse(&2, J.Lexeme, J.Payload{s} <> acc),
                        String.reverse(SCon{rev_head, rev_tail}), SCon{first, prefix_tail}, reverse_prefix),
                    Equal.cong(String, List<&2, J.Lexeme>, s => List.reverse(&2, J.Lexeme, J.Payload{s} <> acc),
                        SCon{first, prefix_tail}, SCon{first, prefix_tail} ++ SNil{},
                        Equal.sym(String, SCon{first, prefix_tail} ++ SNil{}, SCon{first, prefix_tail}, S.append_nil(SCon{first, prefix_tail})))))
        case SCon{+head, +tail}:
            Equal.trans(List<&2, J.Lexeme>,
                J.lex_scan(text, J.Outside{}, SCon{rev_head, rev_tail}, acc),
                J.lexemes(text, J.Outside{}, SCon{rev_head, rev_tail}, acc, J.LexRaw{}),
                List.reverse(&2, J.Lexeme, J.Payload{SCon{first, prefix_tail} ++ text} <> acc),
                Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => J.lexemes(text, J.Outside{}, SCon{rev_head, rev_tail}, acc, action),
                    J.lex_seed_action(text, J.Outside{}), J.LexRaw{},
                    Num.number_char_action(head, J.number_char(head), {==}, tail, state, evidence)),
                Equal.trans(List<&2, J.Lexeme>,
                    J.lexemes(text, J.Outside{}, SCon{rev_head, rev_tail}, acc, J.LexRaw{}),
                    J.lex_scan(tail, J.Outside{}, SCon{head, SCon{rev_head, rev_tail}}, acc),
                    List.reverse(&2, J.Lexeme, J.Payload{SCon{first, prefix_tail} ++ text} <> acc),
                    {==},
                    Equal.trans(List<&2, J.Lexeme>,
                        J.lex_scan(tail, J.Outside{}, SCon{head, SCon{rev_head, rev_tail}}, acc),
                        List.reverse(&2, J.Lexeme, J.Payload{(SCon{first, prefix_tail} ++ SCon{head, SNil{}}) ++ tail} <> acc),
                        List.reverse(&2, J.Lexeme, J.Payload{SCon{first, prefix_tail} ++ text} <> acc),
                        number_tail_acc(tail, J.number_next(state, head), head, SCon{rev_head, rev_tail}, first,
                            prefix_tail ++ SCon{head, SNil{}}, acc,
                            Equal.trans(String,
                                String.reverse(SCon{head, SCon{rev_head, rev_tail}}),
                                String.reverse(SCon{rev_head, rev_tail}) ++ SCon{head, SNil{}},
                                SCon{first, prefix_tail} ++ SCon{head, SNil{}},
                                S.reverse_cons(head, SCon{rev_head, rev_tail}),
                                Equal.cong(String, String, x => x ++ SCon{head, SNil{}},
                                    String.reverse(SCon{rev_head, rev_tail}), SCon{first, prefix_tail}, reverse_prefix)),
                            Num.number_valid_cons(head, tail, state, evidence)),
                        Equal.cong(String, List<&2, J.Lexeme>, s => List.reverse(&2, J.Lexeme, J.Payload{s} <> acc),
                            (SCon{first, prefix_tail} ++ SCon{head, SNil{}}) ++ tail,
                            SCon{first, prefix_tail} ++ text,
                            S.append_assoc(SCon{first, prefix_tail}, SCon{head, SNil{}}, tail)))))

Uses (26):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Char
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.reverse
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.reverse
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=LexAction
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=LexMode
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Lexeme
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=NumberState
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=lex_scan
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=lex_seed_action
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=lexemes
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=number_char
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=number_next
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=number_valid_end
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=number_valid_step
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend&name=number_char_action
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend&name=number_valid_cons
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend&name=append_assoc
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend&name=append_nil
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend&name=reverse_cons