def number_prefix_reversed

qasim-bend-kit@0.1.0.2 · proof/JSON_NumberLexProof.bend:164

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

164def number_prefix_reversed(+text: String,
165                           +state: J.NumberState,
166                           +reversed: String,
167                           +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}:
168    match text:
169        case SNil{}: {==}
170        case SCon{+head, +tail}:
171            Equal.trans(String, W.prefix_reversed(SCon{head, tail}, J.Outside{}, reversed),
172                W.prefix_reversed(tail, J.Outside{}, SCon{head, reversed}),
173                String.reverse(SCon{head, tail}) ++ reversed,
174                Equal.trans(String,
175                    W.prefix_reversed(SCon{head, tail}, J.Outside{}, reversed),
176                    W.prefix_reversed(tail, W.after_mode(J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.Outside{}),
177                        W.after_reversed(J.lex_seed_action(SCon{head, tail}, J.Outside{}), head, reversed)),
178                    W.prefix_reversed(tail, J.Outside{}, SCon{head, reversed}),
179                    {==},
180                    Equal.cong(J.LexAction, String, action => W.prefix_reversed(tail, W.after_mode(action, J.Outside{}),
181                        W.after_reversed(action, head, reversed)),
182                        J.lex_seed_action(SCon{head, tail}, J.Outside{}), J.LexRaw{},
183                        number_char_action(head, J.number_char(head), {==}, tail, state, evidence))),
184                Equal.trans(String,
185                    W.prefix_reversed(tail, J.Outside{}, SCon{head, reversed}),
186                    String.reverse(tail) ++ SCon{head, reversed},
187                    String.reverse(SCon{head, tail}) ++ reversed,
188                    number_prefix_reversed(tail, J.number_next(state, head), SCon{head, reversed},
189                        number_valid_cons(head, tail, state, evidence)),
190                    Equal.trans(String,
191                        String.reverse(tail) ++ SCon{head, reversed},
192                        (String.reverse(tail) ++ SCon{head, SNil{}}) ++ reversed,
193                        String.reverse(SCon{head, tail}) ++ reversed,
194                        Equal.sym(String, (String.reverse(tail) ++ SCon{head, SNil{}}) ++ reversed,
195                            String.reverse(tail) ++ SCon{head, reversed},
196                            S.append_assoc(String.reverse(tail), SCon{head, SNil{}}, reversed)),
197                        Equal.cong(String, String, value => value ++ reversed,
198                            String.reverse(tail) ++ SCon{head, SNil{}}, String.reverse(SCon{head, tail}),
199                            Equal.sym(String, String.reverse(SCon{head, tail}), String.reverse(tail) ++ SCon{head, SNil{}},
200                                S.reverse_cons(head, tail))))))