+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_ADD e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
+ | PREAST_EXPR_SUB subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 e)
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_SUB e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
+ | PREAST_EXPR_MUL subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 e)
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_MUL e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
+ | PREAST_EXPR_DIV subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 e)
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_DIV e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
+
+ | PREAST_EXPR_SHR subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 e)
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
+ (λres2.Some ? ≪?,(AST_EXPR_SHR e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
+ | PREAST_EXPR_SHL subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 e)
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
+ (λres2.Some ? ≪?,(AST_EXPR_SHL e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
+
+ | PREAST_EXPR_GT subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 e)
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_GT e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
+ | PREAST_EXPR_GTE subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 e)
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_GTE e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
+ | PREAST_EXPR_LT subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 e)
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_LT e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
+ | PREAST_EXPR_LTE subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 e)
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_LTE e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
+ | PREAST_EXPR_EQ subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 e)
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_EQ e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
+ | PREAST_EXPR_NEQ subExpr1 subExpr2 ⇒
+ opt_map ?? (preast_to_ast_expr subExpr1 e)
+ (λsigmaRes1:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr subExpr2 e)
+ (λsigmaRes2:(Σt.ast_expr e t).
+ match (sigmaFst ?? sigmaRes1) with
+ [ AST_TYPE_BASE bType ⇒
+ opt_map ?? (preast_to_ast_expr_check e sigmaRes1 (AST_TYPE_BASE bType))
+ (λres1.opt_map ?? (preast_to_ast_expr_check e sigmaRes2 (AST_TYPE_BASE bType))
+ (λres2.Some ? ≪?,(AST_EXPR_NEQ e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
+
+ | PREAST_EXPR_B8toW16 subExpr ⇒
+ opt_map ?? (preast_to_ast_expr subExpr e)
+ (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
+ (λres.Some ? ≪?,(AST_EXPR_B8toW16 e res)≫))
+ | PREAST_EXPR_B8toW32 subExpr ⇒
+ opt_map ?? (preast_to_ast_expr subExpr e)
+ (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
+ (λres.Some ? ≪?,(AST_EXPR_B8toW32 e res)≫))
+ | PREAST_EXPR_W16toB8 subExpr ⇒
+ opt_map ?? (preast_to_ast_expr subExpr e)
+ (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD16))
+ (λres.Some ? ≪?,(AST_EXPR_W16toB8 e res)≫))
+ | PREAST_EXPR_W16toW32 subExpr ⇒
+ opt_map ?? (preast_to_ast_expr subExpr e)
+ (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD16))
+ (λres.Some ? ≪?,(AST_EXPR_W16toW32 e res)≫))
+ | PREAST_EXPR_W32toB8 subExpr ⇒
+ opt_map ?? (preast_to_ast_expr subExpr e)
+ (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD32))
+ (λres.Some ? ≪?,(AST_EXPR_W32toB8 e res)≫))
+ | PREAST_EXPR_W32toW16 subExpr ⇒
+ opt_map ?? (preast_to_ast_expr subExpr e)
+ (λsigmaRes:(Σt.ast_expr e t).opt_map ?? (preast_to_ast_expr_check e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD32))
+ (λres.Some ? ≪?,(AST_EXPR_W32toW16 e res)≫))