+ opt_map ?? (preast_to_ast_expr subExpr1 d e)
+ (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
+ (λsigmaRes2:(Σt.ast_expr d e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
+ (λres2.Some ? ≪?,(AST_EXPR_SHL d e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
+ | PREAST_EXPR_AND subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 d e)
+ (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
+ (λsigmaRes2:(Σt.ast_expr d e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_AND d e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
+ | PREAST_EXPR_OR subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 d e)
+ (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
+ (λsigmaRes2:(Σt.ast_expr d e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_OR d e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
+ | PREAST_EXPR_XOR subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 d e)
+ (λsigmaRes1:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr subExpr2 d e)
+ (λsigmaRes2:(Σt.ast_expr d e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check d e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check d e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_XOR d e ? res1 res2)≫))
+ | _ ⇒ None ? ]))