+ | PREAST_EXPR_GT 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_GT d e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
+ | PREAST_EXPR_GTE 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_GTE d e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
+ | PREAST_EXPR_LT 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_LT d e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
+ | PREAST_EXPR_LTE 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_LTE d e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
+ | PREAST_EXPR_EQ 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_EQ d e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
+ | PREAST_EXPR_NEQ 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_NEQ d e ? res1 res2)≫))
+ | _ ⇒ None ? ]))
+
+ | PREAST_EXPR_B8toW16 subExpr ⇒
+ opt_map ?? (preast_to_ast_expr subExpr d e)
+ (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
+ (λres.Some ? ≪?,(AST_EXPR_B8toW16 d e res)≫))
+ | PREAST_EXPR_B8toW32 subExpr ⇒
+ opt_map ?? (preast_to_ast_expr subExpr d e)
+ (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_BYTE8))
+ (λres.Some ? ≪?,(AST_EXPR_B8toW32 d e res)≫))
+ | PREAST_EXPR_W16toB8 subExpr ⇒
+ opt_map ?? (preast_to_ast_expr subExpr d e)
+ (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD16))
+ (λres.Some ? ≪?,(AST_EXPR_W16toB8 d e res)≫))
+ | PREAST_EXPR_W16toW32 subExpr ⇒
+ opt_map ?? (preast_to_ast_expr subExpr d e)
+ (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD16))
+ (λres.Some ? ≪?,(AST_EXPR_W16toW32 d e res)≫))
+ | PREAST_EXPR_W32toB8 subExpr ⇒
+ opt_map ?? (preast_to_ast_expr subExpr d e)
+ (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD32))
+ (λres.Some ? ≪?,(AST_EXPR_W32toB8 d e res)≫))
+ | PREAST_EXPR_W32toW16 subExpr ⇒
+ opt_map ?? (preast_to_ast_expr subExpr d e)
+ (λsigmaRes:(Σt.ast_expr d e t).opt_map ?? (preast_to_ast_expr_check d e sigmaRes (AST_TYPE_BASE AST_BASE_TYPE_WORD32))
+ (λres.Some ? ≪?,(AST_EXPR_W32toW16 d e res)≫))
+
+ | PREAST_EXPR_ID var ⇒
+ opt_map ?? (preast_to_ast_var var d e)
+ (λsigmaRes:(Σb.(Σt.ast_var d e b t)).
+ match sigmaRes with [ sigma_intro b sigmaRes' ⇒
+ match sigmaRes' with [ sigma_intro t _ ⇒
+ opt_map ?? (preast_to_ast_var_check d e sigmaRes b t)
+ (λres.Some ? ≪?,(AST_EXPR_ID d e ?? res)≫)]])
+ ]