+ (λres2.Some ? ≪(sigmaFst ?? sigmaRes1),(AST_EXPR_ADD e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+ | PREAST_EXPR_SUB subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 e)
+ (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
+ (λres2.Some ? ≪(sigmaFst ?? sigmaRes1),(AST_EXPR_SUB e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+ | PREAST_EXPR_MUL subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 e)
+ (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
+ (λres2.Some ? ≪(sigmaFst ?? sigmaRes1),(AST_EXPR_MUL e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+ | PREAST_EXPR_DIV subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 e)
+ (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
+ (λres2.Some ? ≪(sigmaFst ?? sigmaRes1),(AST_EXPR_DIV e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+
+ | PREAST_EXPR_SHR subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 e)
+ (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 AST_BASE_TYPE_BYTE8)
+ (λres2.Some ? ≪(sigmaFst ?? sigmaRes1),(AST_EXPR_SHR e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+ | PREAST_EXPR_SHL subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 e)
+ (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 AST_BASE_TYPE_BYTE8)
+ (λres2.Some ? ≪(sigmaFst ?? sigmaRes1),(AST_EXPR_SHL e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+
+ | PREAST_EXPR_GT subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 e)
+ (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
+ (λres2.Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_GT e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+ | PREAST_EXPR_GTE subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 e)
+ (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
+ (λres2.Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_GTE e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+ | PREAST_EXPR_LT subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 e)
+ (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
+ (λres2.Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_LT e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+ | PREAST_EXPR_LTE subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 e)
+ (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
+ (λres2.Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_LTE e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+ | PREAST_EXPR_EQ subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 e)
+ (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
+ (λres2.Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_EQ e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))
+ | PREAST_EXPR_NEQ subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 e)
+ (λsigmaRes1:Σt:ast_base_type.ast_expr e t.opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (sigmaFst ?? sigmaRes1))
+ (λres2.Some ? ≪AST_BASE_TYPE_BYTE8,(AST_EXPR_NEQ e (sigmaFst ?? sigmaRes1) (sigmaSnd ?? sigmaRes1) res2)≫)))