JSONNumberLexProof.number_prefix_reversed: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend as JSONNumberLexProof
Lines 164-200 of qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend&start_line=164&end_line=200

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_StringProof.bend as S
import qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend as W

def number_prefix_reversed(+text: String,
                           +state: J.NumberState,
                           +reversed: String,
                           +evidence: {J.number_valid_end(J.number_valid_step(text, state)) == True{} : Bool}) -> {W.prefix_reversed(text, J.Outside{}, reversed) == String.reverse(text) ++ reversed : String}:
    match text:
        case SNil{}: {==}
        case SCon{+head, +tail}:
            Equal.trans(String, W.prefix_reversed(SCon{head, tail}, J.Outside{}, reversed),
                W.prefix_reversed(tail, J.Outside{}, SCon{head, reversed}),
                String.reverse(SCon{head, tail}) ++ reversed,
                Equal.trans(String,
                    W.prefix_reversed(SCon{head, tail}, J.Outside{}, reversed),
                    W.prefix_reversed(tail, W.after_mode(J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.Outside{}),
                        W.after_reversed(J.lex_seed_action(SCon{head, tail}, J.Outside{}), head, reversed)),
                    W.prefix_reversed(tail, J.Outside{}, SCon{head, reversed}),
                    {==},
                    Equal.cong(J.LexAction, String, action => W.prefix_reversed(tail, W.after_mode(action, J.Outside{}),
                        W.after_reversed(action, head, reversed)),
                        J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.LexRaw{},
                        number_char_action(head, J.number_char(head), {==}, tail, state, evidence))),
                Equal.trans(String,
                    W.prefix_reversed(tail, J.Outside{}, SCon{head, reversed}),
                    String.reverse(tail) ++ SCon{head, reversed},
                    String.reverse(SCon{head, tail}) ++ reversed,
                    number_prefix_reversed(tail, J.number_next(state, head), SCon{head, reversed},
                        number_valid_cons(head, tail, state, evidence)),
                    Equal.trans(String,
                        String.reverse(tail) ++ SCon{head, reversed},
                        (String.reverse(tail) ++ SCon{head, SNil{}}) ++ reversed,
                        String.reverse(SCon{head, tail}) ++ reversed,
                        Equal.sym(String, (String.reverse(tail) ++ SCon{head, SNil{}}) ++ reversed,
                            String.reverse(tail) ++ SCon{head, reversed},
                            S.append_assoc(String.reverse(tail), SCon{head, SNil{}}, reversed)),
                        Equal.cong(String, String, value => value ++ reversed,
                            String.reverse(tail) ++ SCon{head, SNil{}}, String.reverse(SCon{head, tail}),
                            Equal.sym(String, String.reverse(SCon{head, tail}), String.reverse(tail) ++ SCon{head, SNil{}},
                                S.reverse_cons(head, tail))))))

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=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=NumberState
  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=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_LexWhitespaceProof.bend&name=after_mode
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend&name=after_reversed
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend&name=prefix_reversed
  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=reverse_cons