FStar build with configurable Z3 inputs — 2026-06-09

[github-actions[bot]]

Build status

• ✅ Z3 build completed
• ⚠️ FStar build failure (pipeline continued)

Inputs used

• z3_ref: master
• z3_cmake_args: ``
• z3_runtime_args: smt.ho_matching=true
• fstar_ref: _nik_higher_order_smt
• fstar_opam_switch: 4.14.2
• fstar_otherflags: --split_queries on_failure --log_failing_queries --ext higher_order_smt --proof_recovery

Produced versions

• Z3: Z3 version 4.17.0 - 64 bit - build hashcode e093be8b607d255373402bd8f52554cd0dd504ba
• FStar: unknown
• FStar commit: b2f48b84ce63139b95d6548587e8835bc03c8392

Generated SMT2 files

• Artifact: https://github.com/Z3Prover/z3/actions/runs/27239186162/artifacts/7522060340

First 1000 lines per generated .smt2 file:

failedQueries-FStar.Algebra.Monoid-1.smt2

; Z3 invocation started by F*
; F* version: 2026.06.07~dev -- commit hash: b2f48b84ce63139b95d6548587e8835bc03c8392
; Z3 version (according to F*): 4.17.0

(set-option :global-decls false)
(set-option :smt.mbqi false)
(set-option :auto_config false)
(set-option :produce-unsat-cores true)
(set-option :model true)
(set-option :smt.case_split 3)
(set-option :smt.relevancy 2)
(set-option :rewriter.enable_der false)
(set-option :rewriter.sort_disjunctions false)
(set-option :pi.decompose_patterns false)
(set-option :smt.arith.solver 6)
(set-option :smt.random-seed 0)


(declare-sort FString)
(declare-fun FString_constr_id (FString) Int)

(declare-sort Term)
(declare-sort Universe)
(declare-fun U_zero () Universe)
(declare-fun U_succ (Universe) Universe)
(declare-fun ulevel ((Universe)) Int)
(declare-fun Univ (Int) Universe)
(assert (= (ulevel U_zero) 0))
(assert (forall ((u Universe)) (! (= (ulevel (U_succ u)) (+ 1 (ulevel u))) :pattern ((ulevel (U_succ u))))))
(assert (forall ((u Universe)) (! (>= (ulevel u) 0) :pattern ((ulevel u)))))
(assert (forall ((u Universe)) (! (= (Univ (ulevel u)) u) :pattern ((ulevel u)))))
(assert (forall ((i Int)) (! (implies (>= i 0) (= (ulevel (Univ i)) i)) :pattern ((Univ i)))))
(declare-fun U_max (Universe Universe) Universe)
(assert (forall ((u1 Universe) (u2 Universe))
(! (= (U_max u1 u2)
(ite (<= (ulevel u1) (ulevel u2)) u2 u1))
:pattern ((U_max u1 u2)))))
(declare-fun U_unif (Int) Universe)
(declare-fun U_unknown () Universe)
(declare-fun Term_constr_id (Term) Int)
(declare-sort Dummy_sort)
(declare-fun Dummy_value () Dummy_sort)
(declare-datatypes () ((Fuel 
(ZFuel) 
(SFuel (prec Fuel)))))
(declare-fun MaxIFuel () Fuel)
(declare-fun MaxFuel () Fuel)
(declare-fun PreType (Term) Term)
(declare-fun Valid (Term) Bool)
(declare-fun HasTypeFuel (Fuel Term Term) Bool)
(define-fun HasTypeZ ((x Term) (t Term)) Bool
(HasTypeFuel ZFuel x t))
(define-fun HasType ((x Term) (t Term)) Bool
(HasTypeFuel MaxIFuel x t))
(declare-fun IsTotFun (Term) Bool)

                ;;fuel irrelevance
(assert (forall ((f Fuel) (x Term) (t Term))
(! (= (HasTypeFuel (SFuel f) x t)
(HasTypeZ x t))
:pattern ((HasTypeFuel (SFuel f) x t)))))
(declare-fun NoHoist (Term Bool) Bool)
;;no-hoist
(assert (forall ((dummy Term) (b Bool))
(! (= (NoHoist dummy b) b)
:pattern ((NoHoist dummy b)))))
(define-fun  IsTyped ((x Term)) Bool
(exists ((t Term)) (HasTypeZ x t)))
(declare-fun ApplyTF (Term Fuel) Term)
(declare-fun ApplyTT (Term Term) Term)
(declare-fun Prec (Term Term) Bool)
(assert (forall ((x Term) (y Term) (z Term))
(! (implies (and (Prec x y) (Prec y z)) (Prec x z))
:pattern ((Prec x z) (Prec x y)))))
(assert (forall ((x Term) (y Term))
(implies (Prec x y)
(not (Prec y x)))))
(declare-fun Closure (Term) Term)
(declare-fun ConsTerm (Term Term) Term)
(declare-fun ConsFuel (Fuel Term) Term)
(declare-fun Tm_uvar (Int) Term)
(define-fun Reify ((x Term)) Term x)
(declare-fun Prims.precedes (Universe Universe Term Term Term Term) Term)
(declare-fun Range_const (Int) Term)
(declare-fun _mul (Int Int) Int)
(declare-fun _div (Int Int) Int)
(declare-fun _mod (Int Int) Int)
(declare-fun __uu__PartialApp () Term)
(assert (forall ((x Int) (y Int)) (! (= (_mul x y) (* x y)) :pattern ((_mul x y)))))
(assert (forall ((x Int) (y Int)) (! (= (_div x y) (div x y)) :pattern ((_div x y)))))
(assert (forall ((x Int) (y Int)) (! (= (_mod x y) (mod x y)) :pattern ((_mod x y)))))
(declare-fun _rmul (Real Real) Real)
(declare-fun _rdiv (Real Real) Real)
(assert (forall ((x Real) (y Real)) (! (= (_rmul x y) (* x y)) :pattern ((_rmul x y)))))
(assert (forall ((x Real) (y Real)) (! (= (_rdiv x y) (/ x y)) :pattern ((_rdiv x y)))))
(define-fun Unreachable () Bool false)
(declare-fun Tm_refinement (Term (=> Term Bool)) Term)
(assert (forall ((x Term) (base Term) (f (=> Term Bool)))
                  (! (iff (and (HasType x base) (select f x))
                          (HasType x (Tm_refinement base f)))
                  :pattern ((HasType x (Tm_refinement base f)))
                  :qid refine_interpretation)))
(assert (forall ((t Term) (base Term) (f (=> Term Bool)))
                  (! (iff (HasType base t)
                          (HasType (Tm_refinement base f) t))
                  :pattern ((HasType (Tm_refinement base f) t))
                  :qid refine_typing)))
(declare-fun Tm_lambda (Term (=> Term Term)) Term)
(assert (forall ((t Term) (f (=> Term Term)) (x Term))
                  (! (implies (HasTypeFuel ZFuel x t)
                              (= (ApplyTT (Tm_lambda t f) x)
                                 (select f x)))
                  :pattern ((ApplyTT (Tm_lambda t f) x))
                  :qid beta_reduction)))
(declare-fun WithType (Term Term) Term)
(assert (forall ((t Term) (ty Term))
                        (! (and (HasType (WithType t ty) ty)
                                (= (WithType t ty) t))
                          :pattern ((WithType t ty)))))
(declare-fun WithInterp (Term Bool) Term)
(assert (forall ((t Term) (interp Bool))
                        (! (and (= (Valid t) interp)
                                (= (WithInterp t interp) t))
                          :pattern ((WithInterp t interp)))))
; <start constructor FString_const>
; Constructor
(declare-fun FString_const (Int) FString)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= 0 (FString_constr_id (FString_const @u0)))
    :pattern ((FString_const @u0))
    :qid constructor_distinct_FString_const))
  :named constructor_distinct_FString_const))
; Projector
(declare-fun FString_const_proj_0 (FString) Int)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= (FString_const_proj_0 (FString_const @u0)) @u0)
    :pattern ((FString_const @u0))
    :qid projection_inverse_FString_const_proj_0))
  :named projection_inverse_FString_const_proj_0))
; Discriminator definition
(define-fun is-FString_const ((__@u0 FString)) Bool
 (and (= (FString_constr_id __@u0) 0) (= __@u0 (FString_const (FString_const_proj_0 __@u0)))))
; </end constructor FString_const>
; <start constructor Tm_type>
; Constructor
(declare-fun Tm_type (Universe) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Universe))
   (! (= 2 (Term_constr_id (Tm_type @u0)))
    :pattern ((Tm_type @u0))
    :qid constructor_distinct_Tm_type))
  :named constructor_distinct_Tm_type))
; Projector
(declare-fun Tm_type_0 (Term) Universe)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Universe))
   (! (= (Tm_type_0 (Tm_type @u0)) @u0) :pattern ((Tm_type @u0)) :qid projection_inverse_Tm_type_0))
  :named projection_inverse_Tm_type_0))
; Discriminator definition
(define-fun is-Tm_type ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 2) (= __@x0 (Tm_type (Tm_type_0 __@x0)))))
; </end constructor Tm_type>
; <start constructor Tm_arrow>
; Constructor
(declare-fun Tm_arrow (Int) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= 3 (Term_constr_id (Tm_arrow @u0)))
    :pattern ((Tm_arrow @u0))
    :qid constructor_distinct_Tm_arrow))
  :named constructor_distinct_Tm_arrow))
; Projector
(declare-fun Tm_arrow_id (Term) Int)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= (Tm_arrow_id (Tm_arrow @u0)) @u0)
    :pattern ((Tm_arrow @u0))
    :qid projection_inverse_Tm_arrow_id))
  :named projection_inverse_Tm_arrow_id))
; Discriminator definition
(define-fun is-Tm_arrow ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 3) (= __@x0 (Tm_arrow (Tm_arrow_id __@x0)))))
; </end constructor Tm_arrow>
; <start constructor Tm_unit>
; Constructor
(declare-fun Tm_unit () Term)
; Constructor distinct
;;; Fact-ids: 
(assert (! (= 6 (Term_constr_id Tm_unit)) :named constructor_distinct_Tm_unit))
; Discriminator definition
(define-fun is-Tm_unit ((__@x0 Term)) Bool (and (= (Term_constr_id __@x0) 6) (= __@x0 Tm_unit)))
; </end constructor Tm_unit>
; <start constructor BoxInt>
; Constructor
(declare-fun BoxInt (Int) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= 7 (Term_constr_id (BoxInt @u0))) :pattern ((BoxInt @u0)) :qid constructor_distinct_BoxInt))
  :named constructor_distinct_BoxInt))
; Projector
(declare-fun BoxInt_proj_0 (Term) Int)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= (BoxInt_proj_0 (BoxInt @u0)) @u0)
    :pattern ((BoxInt @u0))
    :qid projection_inverse_BoxInt_proj_0))
  :named projection_inverse_BoxInt_proj_0))
; Discriminator definition
(define-fun is-BoxInt ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 7) (= __@x0 (BoxInt (BoxInt_proj_0 __@x0)))))
; </end constructor BoxInt>
; <start constructor BoxBool>
; Constructor
(declare-fun BoxBool (Bool) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Bool))
   (! (= 8 (Term_constr_id (BoxBool @u0)))
    :pattern ((BoxBool @u0))
    :qid constructor_distinct_BoxBool))
  :named constructor_distinct_BoxBool))
; Projector
(declare-fun BoxBool_proj_0 (Term) Bool)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Bool))
   (! (= (BoxBool_proj_0 (BoxBool @u0)) @u0)
    :pattern ((BoxBool @u0))
    :qid projection_inverse_BoxBool_proj_0))
  :named projection_inverse_BoxBool_proj_0))
; Discriminator definition
(define-fun is-BoxBool ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 8) (= __@x0 (BoxBool (BoxBool_proj_0 __@x0)))))
; </end constructor BoxBool>
; <start constructor BoxString>
; Constructor
(declare-fun BoxString (FString) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 FString))
   (! (= 9 (Term_constr_id (BoxString @u0)))
    :pattern ((BoxString @u0))
    :qid constructor_distinct_BoxString))
  :named constructor_distinct_BoxString))
; Projector
(declare-fun BoxString_proj_0 (Term) FString)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 FString))
   (! (= (BoxString_proj_0 (BoxString @u0)) @u0)
    :pattern ((BoxString @u0))
    :qid projection_inverse_BoxString_proj_0))
  :named projection_inverse_BoxString_proj_0))
; Discriminator definition
(define-fun is-BoxString ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 9) (= __@x0 (BoxString (BoxString_proj_0 __@x0)))))
; </end constructor BoxString>
; <start constructor BoxReal>
; Constructor
(declare-fun BoxReal (Real) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Real))
   (! (= 10 (Term_constr_id (BoxReal @u0)))
    :pattern ((BoxReal @u0))
    :qid constructor_distinct_BoxReal))
  :named constructor_distinct_BoxReal))
; Projector
(declare-fun BoxReal_proj_0 (Term) Real)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Real))
   (! (= (BoxReal_proj_0 (BoxReal @u0)) @u0)
    :pattern ((BoxReal @u0))
    :qid projection_inverse_BoxReal_proj_0))
  :named projection_inverse_BoxReal_proj_0))
; Discriminator definition
(define-fun is-BoxReal ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 10) (= __@x0 (BoxReal (BoxReal_proj_0 __@x0)))))
; </end constructor BoxReal>
; <start constructor LexCons>
; Constructor
(declare-fun LexCons (Term Term Term) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@x0 Term) (@x1 Term) (@x2 Term))
   (! (= 11 (Term_constr_id (LexCons @x0 @x1 @x2)))
    :pattern ((LexCons @x0 @x1 @x2))
    :qid constructor_distinct_LexCons))
  :named constructor_distinct_LexCons))
; Projector
(declare-fun LexCons_0 (Term) Term)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@x0 Term) (@x1 Term) (@x2 Term))
   (! (= (LexCons_0 (LexCons @x0 @x1 @x2)) @x0)
    :pattern ((LexCons @x0 @x1 @x2))
    :qid projection_inverse_LexCons_0))
  :named projection_inverse_LexCons_0))
; Projector
(declare-fun LexCons_1 (Term) Term)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@x0 Term) (@x1 Term) (@x2 Term))
   (! (= (LexCons_1 (LexCons @x0 @x1 @x2)) @x1)
    :pattern ((LexCons @x0 @x1 @x2))
    :qid projection_inverse_LexCons_1))
  :named projection_inverse_LexCons_1))
; Projector
(declare-fun LexCons_2 (Term) Term)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@x0 Term) (@x1 Term) (@x2 Term))
   (! (= (LexCons_2 (LexCons @x0 @x1 @x2)) @x2)
    :pattern ((LexCons @x0 @x1 @x2))
    :qid projection_inverse_LexCons_2))
  :named projection_inverse_LexCons_2))
; Discriminator definition
(define-fun is-LexCons ((__@x0 Term)) Bool
 (and
  (= (Term_constr_id __@x0) 11)
  (= __@x0 (LexCons (LexCons_0 __@x0) (LexCons_1 __@x0) (LexCons_2 __@x0)))))
; </end constructor LexCons>
(declare-fun Prims.precedes@tok (Universe Universe) Term)
(assert
(forall ((u0 Universe) (u1 Universe) (@x0 Term) (@x1 Term) (@x2 Term) (@x3 Term))
(! (= (ApplyTT (ApplyTT (ApplyTT (ApplyTT (Prims.precedes@tok u0 u1) @x0) @x1) @x2) @x3)
(Prims.precedes u0 u1 @x0 @x1 @x2 @x3))
:pattern ((ApplyTT (ApplyTT (ApplyTT (ApplyTT (Prims.precedes@tok u0 u1) @x0) @x1) @x2) @x3)))))

(define-fun is-Prims.LexCons ((t Term)) Bool 
(is-LexCons t))
(declare-fun Prims.lex_t () Term)
(declare-fun LexTop () Term)
(assert (forall ((u0 Universe) (u1 Universe) (t1 Term) (t2 Term) (x1 Term) (x2 Term) (y1 Term) (y2 Term))
(iff (Valid (Prims.precedes u0 u1 Prims.lex_t Prims.lex_t (LexCons t1 x1 x2) (LexCons t2 y1 y2)))
(or (Valid (Prims.precedes u0 u1 t1 t2 x1 y1))
(and (= x1 y1)
(Valid (Prims.precedes u0 u1 Prims.lex_t Prims.lex_t x2 y2)))))))
(assert (forall ((u0 Universe) (u1 Universe) (t1 Term) (t2 Term) (e1 Term) (e2 Term))
(! (iff (Valid (Prims.precedes u0 u1 t1 t2 e1 e2))
(Valid (Prims.precedes U_zero U_zero Prims.lex_t Prims.lex_t e1 e2)))
:pattern (Prims.precedes u0 u1 t1 t2 e1 e2))))
(assert (forall ((u0 Universe) (u1 Universe) (t1 Term) (t2 Term))
(! (iff (Valid (Prims.precedes u0 u1 Prims.lex_t Prims.lex_t t1 t2)) 
(Prec t1 t2))
:pattern ((Prims.precedes u0 u1 Prims.lex_t Prims.lex_t t1 t2)))))
(assert (forall ((u Universe) (t Term))
(! (iff (HasType (Tm_type u) t)
(= t (Tm_type (U_succ u))))
:pattern ((HasType (Tm_type u) t)))))

(declare-fun FStar.Algebra.Monoid.associativity_lemma (Universe Term Term) Term)
(declare-fun FStar.Algebra.Monoid.left_unitality_lemma (Universe Term Term Term) Term)
(declare-fun FStar.Algebra.Monoid.right_unitality_lemma (Universe Term Term Term) Term)
(declare-fun Prims.eq2 (Universe Term Term Term) Term)
(declare-fun Prims.eqtype () Term)
(declare-fun Prims.hasEq (Universe Term) Term)
(declare-fun Prims.int () Term)
(declare-fun Prims.l_Forall (Universe Term Term) Term)
(declare-fun Prims.nat () Term)
(declare-fun Prims.op_Addition (Term Term) Term)
(declare-fun Prims.prop () Term)
(declare-fun Tm_arrow_d64d4275ed8e577d65d5c1671754751b (Term Universe) Term)
(declare-fun Tm_arrow_eb6b0d19c4d8aa97d1954ddb31b16d45 (Term Universe) Term)
; interpretation_Tm_arrow_d64d4275ed8e577d65d5c1671754751b
;;; Fact-ids: Name FStar.Algebra.Monoid.right_unitality_lemma; Namespace FStar.Algebra.Monoid
(assert
 (! ;; def=FStar.Algebra.Monoid.fst(29,27-29,28); use=FStar.Algebra.Monoid.fst(29,47-29,58)
  (forall ((@x0 Term) (@x1 Term) (@u2 Universe))
   (! (iff
     (HasTypeZ @x0 (Tm_arrow_d64d4275ed8e577d65d5c1671754751b @x1 @u2))
     (and
      ;; def=FStar.Algebra.Monoid.fst(29,27-29,28); use=FStar.Algebra.Monoid.fst(29,47-29,58)
      (forall ((@x3 Term) (@x4 Term))
       (! (implies
         (and (HasType @x3 @x1) (HasType @x4 @x1))
         (HasType (ApplyTT (ApplyTT @x0 @x3) @x4) @x1))
        :pattern ((ApplyTT (ApplyTT @x0 @x3) @x4))
        :qid FStar.Algebra.Monoid_interpretation_Tm_arrow_d64d4275ed8e577d65d5c1671754751b.1))
      (IsTotFun @x0)
      ;; def=FStar.Algebra.Monoid.fst(29,27-29,28); use=FStar.Algebra.Monoid.fst(29,47-29,58)
      (forall ((@x3 Term))
       (! (implies (HasType @x3 @x1) (IsTotFun (ApplyTT @x0 @x3)))
        :pattern ((ApplyTT @x0 @x3))
        :qid FStar.Algebra.Monoid_interpretation_Tm_arrow_d64d4275ed8e577d65d5c1671754751b.2))))
    :pattern ((HasTypeZ @x0 (Tm_arrow_d64d4275ed8e577d65d5c1671754751b @x1 @u2)))
    :qid FStar.Algebra.Monoid_interpretation_Tm_arrow_d64d4275ed8e577d65d5c1671754751b))
  :named FStar.Algebra.Monoid_interpretation_Tm_arrow_d64d4275ed8e577d65d5c1671754751b))
; interpretation_Tm_arrow_eb6b0d19c4d8aa97d1954ddb31b16d45
;;; Fact-ids: Name Prims.l_Forall; Namespace Prims
(assert
 (! ;; def=Prims.fst(264,22-264,73); use=Prims.fst(264,59-264,73)
  (forall ((@x0 Term) (@x1 Term) (@u2 Universe))
   (! (iff
     (HasTypeZ @x0 (Tm_arrow_eb6b0d19c4d8aa97d1954ddb31b16d45 @x1 @u2))
     (and
      ;; def=Prims.fst(264,22-264,73); use=Prims.fst(264,59-264,73)
      (forall ((@x3 Term))
       (! (implies (HasType @x3 @x1) (HasType (ApplyTT @x0 @x3) Prims.prop))
        :pattern ((ApplyTT @x0 @x3))
        :qid Prims_interpretation_Tm_arrow_eb6b0d19c4d8aa97d1954ddb31b16d45.1))
      (IsTotFun @x0)))
    :pattern ((HasTypeZ @x0 (Tm_arrow_eb6b0d19c4d8aa97d1954ddb31b16d45 @x1 @u2)))
    :qid Prims_interpretation_Tm_arrow_eb6b0d19c4d8aa97d1954ddb31b16d45))
  :named Prims_interpretation_Tm_arrow_eb6b0d19c4d8aa97d1954ddb31b16d45))
; Constructor distinct
;;; Fact-ids: Name Prims.int; Namespace Prims
(assert
 (! (= 290 (Term_constr_id Prims.int)) :named constructor_distinct_Prims.int))
; Equation for FStar.Algebra.Monoid.associativity_lemma
;;; Fact-ids: Name FStar.Algebra.Monoid.associativity_lemma; Namespace FStar.Algebra.Monoid
(assert
 (! ;; def=FStar.Algebra.Monoid.fst(35,4-35,23); use=FStar.Algebra.Monoid.fst(35,4-35,23)
  (forall ((@u0 Universe) (@x1 Term) (@x2 Term))
   (! (=
     (FStar.Algebra.Monoid.associativity_lemma @u0 @x1 @x2)
     (WithInterp
      (Prims.l_Forall
       @u0
       @x1
       (WithType
        ;; def=FStar.Algebra.Monoid.fst(36,9-36,64); use=FStar.Algebra.Monoid.fst(36,9-36,64)
        (Tm_lambda
         @x1
         ;; def=FStar.Algebra.Monoid.fst(36,9-36,64); use=FStar.Algebra.Monoid.fst(36,9-36,64)
         (lambda ((@x3 Term))
          (Prims.l_Forall
           @u0
           @x1
           (WithType
            ;; def=FStar.Algebra.Monoid.fst(36,9-36,64); use=FStar.Algebra.Monoid.fst(36,9-36,64)
            (Tm_lambda
             @x1
             ;; def=FStar.Algebra.Monoid.fst(36,9-36,64); use=FStar.Algebra.Monoid.fst(36,9-36,64)
             (lambda ((@x4 Term))
              (Prims.l_Forall
               @u0
               @x1
               (WithType
                ;; def=FStar.Algebra.Monoid.fst(36,9-36,64); use=FStar.Algebra.Monoid.fst(36,9-36,64)
                (Tm_lambda
                 @x1
                 ;; def=FStar.Algebra.Monoid.fst(36,9-36,64); use=FStar.Algebra.Monoid.fst(36,9-36,64)
                 (lambda ((@x5 Term))
                  (Prims.eq2
                   @u0
                   @x1
                   (ApplyTT (ApplyTT @x2 (ApplyTT (ApplyTT @x2 @x3) @x4)) @x5)
                   (ApplyTT (ApplyTT @x2 @x3) (ApplyTT (ApplyTT @x2 @x4) @x5)))))
                (Tm_arrow_eb6b0d19c4d8aa97d1954ddb31b16d45 @x1 @u0)))))
            (Tm_arrow_eb6b0d19c4d8aa97d1954ddb31b16d45 @x1 @u0)))))
        (Tm_arrow_eb6b0d19c4d8aa97d1954ddb31b16d45 @x1 @u0)))
      ;; def=FStar.Algebra.Monoid.fst(36,2-36,64); use=FStar.Algebra.Monoid.fst(36,2-36,64)
      (forall ((@x3 Term) (@x4 Term) (@x5 Term))
       (! (implies
         (and (HasType @x3 @x1) (HasType @x4 @x1) (HasType @x5 @x1))
         ;; def=FStar.Algebra.Monoid.fst(36,20-36,64); use=FStar.Algebra.Monoid.fst(36,20-36,64)
         (=
          (ApplyTT (ApplyTT @x2 (ApplyTT (ApplyTT @x2 @x3) @x4)) @x5)
          (ApplyTT (ApplyTT @x2 @x3) (ApplyTT (ApplyTT @x2 @x4) @x5))))
        :qid defn_equation_FStar.Algebra.Monoid.associativity_lemma.1))))
    :pattern ((FStar.Algebra.Monoid.associativity_lemma @u0 @x1 @x2))
    :qid defn_equation_FStar.Algebra.Monoid.associativity_lemma))
  :named defn_equation_FStar.Algebra.Monoid.associativity_lemma))
; Equation for FStar.Algebra.Monoid.left_unitality_lemma
;;; Fact-ids: Name FStar.Algebra.Monoid.left_unitality_lemma; Namespace FStar.Algebra.Monoid
(assert
 (! ;; def=FStar.Algebra.Monoid.fst(32,4-32,24); use=FStar.Algebra.Monoid.fst(32,4-32,24)
  (forall ((@u0 Universe) (@x1 Term) (@x2 Term) (@x3 Term))
   (! (=
     (FStar.Algebra.Monoid.left_unitality_lemma @u0 @x1 @x2 @x3)
     (WithInterp
      (Prims.l_Forall
       @u0
       @x1
       (WithType
        ;; def=FStar.Algebra.Monoid.fst(33,2-33,31); use=FStar.Algebra.Monoid.fst(33,2-33,31)
        (Tm_lambda
         @x1
         ;; def=FStar.Algebra.Monoid.fst(33,2-33,31); use=FStar.Algebra.Monoid.fst(33,2-33,31)
         (lambda ((@x4 Term)) (Prims.eq2 @u0 @x1 (ApplyTT (ApplyTT @x3 @x2) @x4) @x4)))
        (Tm_arrow_eb6b0d19c4d8aa97d1954ddb31b16d45 @x1 @u0)))
      ;; def=FStar.Algebra.Monoid.fst(33,2-33,31); use=FStar.Algebra.Monoid.fst(33,2-33,31)
      (forall ((@x4 Term))
       (! (implies
         (HasType @x4 @x1)
         ;; def=FStar.Algebra.Monoid.fst(33,16-33,31); use=FStar.Algebra.Monoid.fst(33,16-33,31)
         (= (ApplyTT (ApplyTT @x3 @x2) @x4) @x4))
        :qid defn_equation_FStar.Algebra.Monoid.left_unitality_lemma.1))))
    :pattern ((FStar.Algebra.Monoid.left_unitality_lemma @u0 @x1 @x2 @x3))
    :qid defn_equation_FStar.Algebra.Monoid.left_unitality_lemma))
  :named defn_equation_FStar.Algebra.Monoid.left_unitality_lemma))
; Equation for FStar.Algebra.Monoid.right_unitality_lemma
;;; Fact-ids: Name FStar.Algebra.Monoid.right_unitality_lemma; Namespace FStar.Algebra.Monoid
(assert
 (! ;; def=FStar.Algebra.Monoid.fst(29,4-29,25); use=FStar.Algebra.Monoid.fst(29,4-29,25)
  (forall ((@u0 Universe) (@x1 Term) (@x2 Term) (@x3 Term))
   (! (=
     (FStar.Algebra.Monoid.right_unitality_lemma @u0 @x1 @x2 @x3)
     (WithInterp
      (Prims.l_Forall
       @u0
       @x1
       (WithType
        ;; def=FStar.Algebra.Monoid.fst(30,2-30,31); use=FStar.Algebra.Monoid.fst(30,2-30,31)
        (Tm_lambda
         @x1
         ;; def=FStar.Algebra.Monoid.fst(30,2-30,31); use=FStar.Algebra.Monoid.fst(30,2-30,31)
         (lambda ((@x4 Term)) (Prims.eq2 @u0 @x1 (ApplyTT (ApplyTT @x3 @x4) @x2) @x4)))
        (Tm_arrow_eb6b0d19c4d8aa97d1954ddb31b16d45 @x1 @u0)))
      ;; def=FStar.Algebra.Monoid.fst(30,2-30,31); use=FStar.Algebra.Monoid.fst(30,2-30,31)
      (forall ((@x4 Term))
       (! (implies
         (HasType @x4 @x1)
         ;; def=FStar.Algebra.Monoid.fst(30,16-30,31); use=FStar.Algebra.Monoid.fst(30,16-30,31)
         (= (ApplyTT (ApplyTT @x3 @x4) @x2) @x4))
        :qid defn_equation_FStar.Algebra.Monoid.right_unitality_lemma.1))))
    :pattern ((FStar.Algebra.Monoid.right_unitality_lemma @u0 @x1 @x2 @x3))
    :qid defn_equation_FStar.Algebra.Monoid.right_unitality_lemma))
  :named defn_equation_FStar.Algebra.Monoid.right_unitality_lemma))
; Eq2 interpretation
;;; Fact-ids: Name Prims.eq2; Namespace Prims
(assert
 (! (forall ((@u0 Universe) (@x1 Term) (@x2 Term) (@x3 Term))
   (! (iff (= @x2 @x3) (Valid (Prims.eq2 @u0 @x1 @x2 @x3)))
    :pattern ((Prims.eq2 @u0 @x1 @x2 @x3))
    :qid eq2-interp))
  :named eq2-interp))
; Equation for FStar.Algebra.Monoid.associativity_lemma
;;; Fact-ids: Name FStar.Algebra.Monoid.associativity_lemma; Namespace FStar.Algebra.Monoid
(assert
 (! ;; def=FStar.Algebra.Monoid.fst(35,4-35,23); use=FStar.Algebra.Monoid.fst(35,4-35,23)
  (forall ((@u0 Universe) (@x1 Term) (@x2 Term))
   (! (=
     (Valid (FStar.Algebra.Monoid.associativity_lemma @u0 @x1 @x2))
     ;; def=FStar.Algebra.Monoid.fst(36,2-36,64); use=FStar.Algebra.Monoid.fst(36,2-36,64)
     (forall ((@x3 Term) (@x4 Term) (@x5 Term))
      (! (implies
        (and (HasType @x3 @x1) (HasType @x4 @x1) (HasType @x5 @x1))
        ;; def=FStar.Algebra.Monoid.fst(36,20-36,64); use=FStar.Algebra.Monoid.fst(36,20-36,64)
        (=
         (ApplyTT (ApplyTT @x2 (ApplyTT (ApplyTT @x2 @x3) @x4)) @x5)
         (ApplyTT (ApplyTT @x2 @x3) (ApplyTT (ApplyTT @x2 @x4) @x5))))
       :qid equation_FStar.Algebra.Monoid.associativity_lemma.1)))
    :pattern ((FStar.Algebra.Monoid.associativity_lemma @u0 @x1 @x2))
    :qid equation_FStar.Algebra.Monoid.associativity_lemma))
  :named equation_FStar.Algebra.Monoid.associativity_lemma))
; Equation for FStar.Algebra.Monoid.left_unitality_lemma
;;; Fact-ids: Name FStar.Algebra.Monoid.left_unitality_lemma; Namespace FStar.Algebra.Monoid
(assert
 (! ;; def=FStar.Algebra.Monoid.fst(32,4-32,24); use=FStar.Algebra.Monoid.fst(32,4-32,24)
  (forall ((@u0 Universe) (@x1 Term) (@x2 Term) (@x3 Term))
   (! (=
     (Valid (FStar.Algebra.Monoid.left_unitality_lemma @u0 @x1 @x2 @x3))
     ;; def=FStar.Algebra.Monoid.fst(33,2-33,31); use=FStar.Algebra.Monoid.fst(33,2-33,31)
     (forall ((@x4 Term))
      (! (implies
        (HasType @x4 @x1)
        ;; def=FStar.Algebra.Monoid.fst(33,16-33,31); use=FStar.Algebra.Monoid.fst(33,16-33,31)
        (= (ApplyTT (ApplyTT @x3 @x2) @x4) @x4))
       :qid equation_FStar.Algebra.Monoid.left_unitality_lemma.1)))
    :pattern ((FStar.Algebra.Monoid.left_unitality_lemma @u0 @x1 @x2 @x3))
    :qid equation_FStar.Algebra.Monoid.left_unitality_lemma))
  :named equation_FStar.Algebra.Monoid.left_unitality_lemma))
; Equation for FStar.Algebra.Monoid.right_unitality_lemma
;;; Fact-ids: Name FStar.Algebra.Monoid.right_unitality_lemma; Namespace FStar.Algebra.Monoid
(assert
 (! ;; def=FStar.Algebra.Monoid.fst(29,4-29,25); use=FStar.Algebra.Monoid.fst(29,4-29,25)
  (forall ((@u0 Universe) (@x1 Term) (@x2 Term) (@x3 Term))
   (! (=
     (Valid (FStar.Algebra.Monoid.right_unitality_lemma @u0 @x1 @x2 @x3))
     ;; def=FStar.Algebra.Monoid.fst(30,2-30,31); use=FStar.Algebra.Monoid.fst(30,2-30,31)
     (forall ((@x4 Term))
      (! (implies
        (HasType @x4 @x1)
        ;; def=FStar.Algebra.Monoid.fst(30,16-30,31); use=FStar.Algebra.Monoid.fst(30,16-30,31)
        (= (ApplyTT (ApplyTT @x3 @x4) @x2) @x4))
       :qid equation_FStar.Algebra.Monoid.right_unitality_lemma.1)))
    :pattern ((FStar.Algebra.Monoid.right_unitality_lemma @u0 @x1 @x2 @x3))
    :qid equation_FStar.Algebra.Monoid.right_unitality_lemma))
  :named equation_FStar.Algebra.Monoid.right_unitality_lemma))
; Equation for Prims.eqtype
;;; Fact-ids: Name Prims.eqtype; Namespace Prims
(assert
 (! (=
   Prims.eqtype
   ;; def=Prims.fst(90,14-90,31); use=Prims.fst(90,14-90,31)
   (Tm_refinement
    (Tm_type U_zero)
    ;; def=Prims.fst(90,14-90,31); use=Prims.fst(90,14-90,31)
    (lambda ((@x0 Term))
     ;; def=Prims.fst(90,23-90,30); use=Prims.fst(90,23-90,30)
     (Valid
      ;; def=Prims.fst(90,23-90,30); use=Prims.fst(90,23-90,30)
      (Prims.hasEq U_zero @x0)))))
  :named equation_Prims.eqtype))
; Equation for Prims.nat
;;; Fact-ids: Name Prims.nat; Namespace Prims
(assert
 (! (=
   Prims.nat
   ;; def=Prims.fst(642,11-642,25); use=Prims.fst(642,11-642,25)
   (Tm_refinement
    Prims.int
    ;; def=Prims.fst(642,11-642,25); use=Prims.fst(642,11-642,25)
    (lambda ((@x0 Term))
     ;; def=Prims.fst(642,18-642,24); use=Prims.fst(642,18-642,24)
     (>= (BoxInt_proj_0 @x0) (BoxInt_proj_0 (BoxInt 0))))))
  :named equation_Prims.nat))
; function token typing
;;; Fact-ids: Name Prims.eqtype; Namespace Prims
(assert
 (! (HasType Prims.eqtype (Tm_type (U_succ U_zero))) :named function_token_typing_Prims.eqtype))
; function token typing
;;; Fact-ids: Name Prims.int; Namespace Prims
(assert
 (! (HasType Prims.int Prims.eqtype) :named function_token_typing_Prims.int))
; function token typing
;;; Fact-ids: Name Prims.nat; Namespace Prims
(assert
 (! (HasType Prims.nat (Tm_type U_zero)) :named function_token_typing_Prims.nat))
; function token typing
;;; Fact-ids: Name Prims.prop; Namespace Prims
(assert
 (! (HasType Prims.prop (Tm_type U_zero)) :named function_token_typing_Prims.prop))
; int inversion
;;; Fact-ids: Name Prims.int; Namespace Prims
(assert
 (! (forall ((@u0 Fuel) (@x1 Term))
   (! (implies (HasTypeFuel @u0 @x1 Prims.int) (is-BoxInt @x1))
    :pattern ((HasTypeFuel @u0 @x1 Prims.int))
    :qid int_inversion))
  :named int_inversion))
; int typing
;;; Fact-ids: Name Prims.int; Namespace Prims
(assert
 (! (forall ((@u0 Int)) (! (HasType (BoxInt @u0) Prims.int) :pattern ((BoxInt @u0)) :qid int_typing))
  :named int_typing))
; kinding_Tm_arrow_d64d4275ed8e577d65d5c1671754751b
;;; Fact-ids: Name FStar.Algebra.Monoid.right_unitality_lemma; Namespace FStar.Algebra.Monoid
(assert
 (! ;; def=FStar.Algebra.Monoid.fst(29,27-29,28); use=FStar.Algebra.Monoid.fst(29,47-29,58)
  (forall ((@x0 Term) (@u1 Universe))
   (! (HasType (Tm_arrow_d64d4275ed8e577d65d5c1671754751b @x0 @u1) (Tm_type @u1))
    :pattern ((HasType (Tm_arrow_d64d4275ed8e577d65d5c1671754751b @x0 @u1) (Tm_type @u1)))
    :qid kinding_Tm_arrow_d64d4275ed8e577d65d5c1671754751b))
  :named kinding_Tm_arrow_d64d4275ed8e577d65d5c1671754751b))
; kinding_Tm_arrow_eb6b0d19c4d8aa97d1954ddb31b16d45
;;; Fact-ids: Name Prims.l_Forall; Namespace Prims
(assert
 (! ;; def=Prims.fst(264,22-264,73); use=Prims.fst(264,59-264,73)
  (forall ((@x0 Term) (@u1 Universe))
   (! (HasType (Tm_arrow_eb6b0d19c4d8aa97d1954ddb31b16d45 @x0 @u1) (Tm_type @u1))
    :pattern ((HasType (Tm_arrow_eb6b0d19c4d8aa97d1954ddb31b16d45 @x0 @u1) (Tm_type @u1)))
    :qid kinding_Tm_arrow_eb6b0d19c4d8aa97d1954ddb31b16d45))
  :named kinding_Tm_arrow_eb6b0d19c4d8aa97d1954ddb31b16d45))
;;; Fact-ids: Name Prims.op_Addition; Namespace Prims
(assert
 (! ;; def=Prims.fst(520,4-520,15); use=Prims.fst(520,4-520,15)
  (forall ((@x0 Term) (@x1 Term))
   (! (= (Prims.op_Addition @x0 @x1) (BoxInt (+ (BoxInt_proj_0 @x0) (BoxInt_proj_0 @x1))))
    :pattern ((Prims.op_Addition @x0 @x1))
    :qid primitive_Prims.op_Addition))
  :named primitive_Prims.op_Addition))
; free var typing
;;; Fact-ids: Name FStar.Algebra.Monoid.associativity_lemma; Namespace FStar.Algebra.Monoid
(assert
 (! ;; def=FStar.Algebra.Monoid.fst(35,4-35,23); use=FStar.Algebra.Monoid.fst(35,4-35,23)
  (forall ((@u0 Universe) (@x1 Term) (@x2 Term))
   (! (implies
     (and
      (HasType @x1 (Tm_type @u0))
      (HasType @x2 (Tm_arrow_d64d4275ed8e577d65d5c1671754751b @x1 @u0)))
     (HasType (FStar.Algebra.Monoid.associativity_lemma @u0 @x1 @x2) Prims.prop))
    :pattern ((FStar.Algebra.Monoid.associativity_lemma @u0 @x1 @x2))
    :qid typing_FStar.Algebra.Monoid.associativity_lemma))
  :named typing_FStar.Algebra.Monoid.associativity_lemma))
; free var typing
;;; Fact-ids: Name FStar.Algebra.Monoid.left_unitality_lemma; Namespace FStar.Algebra.Monoid
(assert
 (! ;; def=FStar.Algebra.Monoid.fst(32,4-32,24); use=FStar.Algebra.Monoid.fst(32,4-32,24)
  (forall ((@u0 Universe) (@x1 Term) (@x2 Term) (@x3 Term))
   (! (implies
     (and
      (HasType @x1 (Tm_type @u0))
      (HasType @x2 @x1)
      (HasType @x3 (Tm_arrow_d64d4275ed8e577d65d5c1671754751b @x1 @u0)))
     (HasType (FStar.Algebra.Monoid.left_unitality_lemma @u0 @x1 @x2 @x3) Prims.prop))
    :pattern ((FStar.Algebra.Monoid.left_unitality_lemma @u0 @x1 @x2 @x3))
    :qid typing_FStar.Algebra.Monoid.left_unitality_lemma))
  :named typing_FStar.Algebra.Monoid.left_unitality_lemma))
; free var typing
;;; Fact-ids: Name FStar.Algebra.Monoid.right_unitality_lemma; Namespace FStar.Algebra.Monoid
(assert
 (! ;; def=FStar.Algebra.Monoid.fst(29,4-29,25); use=FStar.Algebra.Monoid.fst(29,4-29,25)
  (forall ((@u0 Universe) (@x1 Term) (@x2 Term) (@x3 Term))
   (! (implies
     (and
      (HasType @x1 (Tm_type @u0))
      (HasType @x2 @x1)
      (HasType @x3 (Tm_arrow_d64d4275ed8e577d65d5c1671754751b @x1 @u0)))
     (HasType (FStar.Algebra.Monoid.right_unitality_lemma @u0 @x1 @x2 @x3) Prims.prop))
    :pattern ((FStar.Algebra.Monoid.right_unitality_lemma @u0 @x1 @x2 @x3))
    :qid typing_FStar.Algebra.Monoid.right_unitality_lemma))
  :named typing_FStar.Algebra.Monoid.right_unitality_lemma))
; free var typing
;;; Fact-ids: Name Prims.eq2; Namespace Prims
(assert
 (! ;; def=Prims.fst(160,11-160,14); use=Prims.fst(160,11-160,14)
  (forall ((@u0 Universe) (@x1 Term) (@x2 Term) (@x3 Term))
   (! (implies
     (and (HasType @x1 (Tm_type @u0)) (HasType @x2 @x1) (HasType @x3 @x1))
     (HasType (Prims.eq2 @u0 @x1 @x2 @x3) Prims.prop))
    :pattern ((Prims.eq2 @u0 @x1 @x2 @x3))
    :qid typing_Prims.eq2))
  :named typing_Prims.eq2))
; free var typing
;;; Fact-ids: Name Prims.eqtype; Namespace Prims
(assert
 (! (HasType Prims.eqtype (Tm_type (U_succ U_zero))) :named typing_Prims.eqtype))
; free var typing
;;; Fact-ids: Name Prims.hasEq; Namespace Prims
(assert
 (! ;; def=Prims.fst(86,5-86,10); use=Prims.fst(86,5-86,10)
  (forall ((@u0 Universe) (@x1 Term))
   (! (implies (HasType @x1 (Tm_type @u0)) (HasType (Prims.hasEq @u0 @x1) Prims.prop))
    :pattern ((Prims.hasEq @u0 @x1))
    :qid typing_Prims.hasEq))
  :named typing_Prims.hasEq))
; free var typing
;;; Fact-ids: Name Prims.int; Namespace Prims
(assert
 (! (HasType Prims.int Prims.eqtype) :named typing_Prims.int))
; free var typing
;;; Fact-ids: Name Prims.l_Forall; Namespace Prims
(assert
 (! ;; def=Prims.fst(264,11-264,19); use=Prims.fst(264,11-264,19)
  (forall ((@u0 Universe) (@x1 Term) (@x2 Term))
   (! (implies
     (and
      (HasType @x1 (Tm_type @u0))
      (HasType @x2 (Tm_arrow_eb6b0d19c4d8aa97d1954ddb31b16d45 @x1 @u0)))
     (HasType (Prims.l_Forall @u0 @x1 @x2) Prims.prop))
    :pattern ((Prims.l_Forall @u0 @x1 @x2))
    :qid typing_Prims.l_Forall))
  :named typing_Prims.l_Forall))
; free var typing
;;; Fact-ids: Name Prims.nat; Namespace Prims
(assert
 (! (HasType Prims.nat (Tm_type U_zero)) :named typing_Prims.nat))
; free var typing
;;; Fact-ids: Name Prims.op_Addition; Namespace Prims
(assert
 (! ;; def=Prims.fst(520,4-520,15); use=Prims.fst(520,4-520,15)
  (forall ((@x0 Term) (@x1 Term))
   (! (implies
     (and (HasType @x0 Prims.int) (HasType @x1 Prims.int))
     (HasType (Prims.op_Addition @x0 @x1) Prims.int))
    :pattern ((Prims.op_Addition @x0 @x1))
    :qid typing_Prims.op_Addition))
  :named typing_Prims.op_Addition))
; free var typing
;;; Fact-ids: Name Prims.prop; Namespace Prims
(assert
 (! (HasType Prims.prop (Tm_type U_zero)) :named typing_Prims.prop))
(push) ;; push{1
; Starting query at FStar.Algebra.Monoid.fst(59,0-61,24)
(declare-fun label_4 () Bool)
(declare-fun label_3 () Bool)
(declare-fun label_2 () Bool)
(declare-fun label_1 () Bool)
(declare-fun Tm_arrow_2bb228db8432d0cdc106cb64c22e55ba () Term)
; kinding_Tm_arrow_2bb228db8432d0cdc106cb64c22e55ba
;;; Fact-ids: 
(assert
 (! (HasType Tm_arrow_2bb228db8432d0cdc106cb64c22e55ba (Tm_type U_zero))
  :named kinding_Tm_arrow_2bb228db8432d0cdc106cb64c22e55ba))
; pretyping
;;; Fact-ids: 
(assert
 (! ;; def=FStar.Algebra.Monoid.fst(60,17-60,27); use=Prims.fst(422,7-422,10)
  (forall ((@u0 Fuel) (@x1 Term))
   (! (implies
     (HasTypeFuel @u0 @x1 Tm_arrow_2bb228db8432d0cdc106cb64c22e55ba)
     (is-Tm_arrow (PreType @x1)))
    :pattern ((HasTypeFuel @u0 @x1 Tm_arrow_2bb228db8432d0cdc106cb64c22e55ba))
    :qid FStar.Algebra.Monoid_pre_typing_Tm_arrow_2bb228db8432d0cdc106cb64c22e55ba))
  :named FStar.Algebra.Monoid_pre_typing_Tm_arrow_2bb228db8432d0cdc106cb64c22e55ba))
; interpretation_Tm_arrow_2bb228db8432d0cdc106cb64c22e55ba
;;; Fact-ids: 
(assert
 (! ;; def=FStar.Algebra.Monoid.fst(60,17-60,27); use=Prims.fst(422,7-422,10)
  (forall ((@x0 Term))
   (! (iff
     (HasTypeZ @x0 Tm_arrow_2bb228db8432d0cdc106cb64c22e55ba)
     (and
      ;; def=FStar.Algebra.Monoid.fst(60,17-60,27); use=Prims.fst(422,7-422,10)
      (forall ((@x1 Term) (@x2 Term))
       (! (implies
         (and (HasType @x1 Prims.nat) (HasType @x2 Prims.nat))
         (HasType (ApplyTT (ApplyTT @x0 @x1) @x2) Prims.nat))
        :pattern ((ApplyTT (ApplyTT @x0 @x1) @x2))
        :qid FStar.Algebra.Monoid_interpretation_Tm_arrow_2bb228db8432d0cdc106cb64c22e55ba.1))
      (IsTotFun @x0)
      ;; def=FStar.Algebra.Monoid.fst(60,17-60,27); use=Prims.fst(422,7-422,10)
      (forall ((@x1 Term))
       (! (implies (HasType @x1 Prims.nat) (IsTotFun (ApplyTT @x0 @x1)))
        :pattern ((ApplyTT @x0 @x1))
        :qid FStar.Algebra.Monoid_interpretation_Tm_arrow_2bb228db8432d0cdc106cb64c22e55ba.2))))
    :pattern ((HasTypeZ @x0 Tm_arrow_2bb228db8432d0cdc106cb64c22e55ba))
    :qid FStar.Algebra.Monoid_interpretation_Tm_arrow_2bb228db8432d0cdc106cb64c22e55ba))
  :named FStar.Algebra.Monoid_interpretation_Tm_arrow_2bb228db8432d0cdc106cb64c22e55ba))

; Encoding query formula : (forall (x: Prims.nat) (y: Prims.nat). (* - Could not prove post-condition *) x + y >= 0) /\
; (forall (any_result: (x: Prims.nat -> y: Prims.nat -> Prims.nat)).
;     (fun x y -> x + y <: Prims.nat) == any_result ==>
;     FStar.Algebra.Monoid.right_unitality_lemma Prims.nat 0 any_result /\
;     FStar.Algebra.Monoid.left_unitality_lemma Prims.nat 0 any_result /\
;     FStar.Algebra.Monoid.associativity_lemma Prims.nat any_result)
; Context: While encoding a query
; While checking for top-level effects
; While typechecking the top-level declaration ‘let nat_plus_monoid’
(push) ;; push{0
; <fuel='8' ifuel='2'>
;;; Fact-ids: 
(assert
 (! (= MaxFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel (SFuel ZFuel)))))))))
  :named @MaxFuel_assumption))
;;; Fact-ids: 
(assert (! (= MaxIFuel (SFuel (SFuel ZFuel))) :named @MaxIFuel_assumption))
; query
;;; Fact-ids: 
(assert
 (! (not
   ;; def=Prims.fst(427,77-427,89); use=Prims.fst(427,77-427,89)
   (and
    (forall ((@x0 Term) (@x1 Term))
     (! (implies
       (and (HasType @x0 Prims.nat) (HasType @x1 Prims.nat))
       ;; def=Prims.fst(642,18-642,24); use=FStar.Algebra.Monoid.fst(60,30-60,35)
       (or
        label_1
        ;; def=Prims.fst(642,18-642,24); use=FStar.Algebra.Monoid.fst(60,30-60,35)
        (>= (BoxInt_proj_0 (Prims.op_Addition @x0 @x1)) (BoxInt_proj_0 (BoxInt 0)))))
      :qid @query))
    ;; def=Prims.fst(419,66-419,102); use=Prims.fst(422,31-422,44)
    (forall ((@x0 Term))
     (! (implies
       (and
        (HasType @x0 Tm_arrow_2bb228db8432d0cdc106cb64c22e55ba)
        ;; def=FStar.Algebra.Monoid.fst(60,6-60,35); use=FStar.Algebra.Monoid.fst(60,6-60,35)
        (=
         (WithType
          ;; def=FStar.Algebra.Monoid.fst(60,30-60,35); use=FStar.Algebra.Monoid.fst(60,30-60,35)
          (Tm_lambda
           Prims.nat
           ;; def=FStar.Algebra.Monoid.fst(60,30-60,35); use=FStar.Algebra.Monoid.fst(60,30-60,35)
           (lambda ((@x1 Term))
            ;; def=FStar.Algebra.Monoid.fst(60,30-60,35); use=FStar.Algebra.Monoid.fst(60,30-60,35)
            (Tm_lambda
             Prims.nat
             ;; def=FStar.Algebra.Monoid.fst(60,30-60,35); use=FStar.Algebra.Monoid.fst(60,30-60,35)
             (lambda ((@x2 Term)) (Prims.op_Addition @x1 @x2)))))
          Tm_arrow_2bb228db8432d0cdc106cb64c22e55ba)
         @x0))
       ;; def=FStar.Algebra.Monoid.fst(51,14-51,109); use=FStar.Algebra.Monoid.fst(61,2-61,14)
       (and
        ;; def=FStar.Algebra.Monoid.fst(51,15-51,45); use=FStar.Algebra.Monoid.fst(61,2-61,14)
        (or
         label_2
         ;; def=FStar.Algebra.Monoid.fst(51,15-51,45); use=FStar.Algebra.Monoid.fst(61,2-61,14)
         (Valid
          ;; def=FStar.Algebra.Monoid.fst(51,15-51,45); use=FStar.Algebra.Monoid.fst(61,2-61,14)
          (FStar.Algebra.Monoid.right_unitality_lemma U_zero Prims.nat (BoxInt 0) @x0)))
        ;; def=FStar.Algebra.Monoid.fst(51,49-51,78); use=FStar.Algebra.Monoid.fst(61,2-61,14)
        (or
         label_3
         ;; def=FStar.Algebra.Monoid.fst(51,49-51,78); use=FStar.Algebra.Monoid.fst(61,2-61,14)
         (Valid
          ;; def=FStar.Algebra.Monoid.fst(51,49-51,78); use=FStar.Algebra.Monoid.fst(61,2-61,14)
          (FStar.Algebra.Monoid.left_unitality_lemma U_zero Prims.nat (BoxInt 0) @x0)))
        ;; def=FStar.Algebra.Monoid.fst(51,82-51,108); use=FStar.Algebra.Monoid.fst(61,2-61,14)
        (or
         label_4
         ;; def=FStar.Algebra.Monoid.fst(51,82-51,108); use=FStar.Algebra.Monoid.fst(61,2-61,14)
         (Valid
          ;; def=FStar.Algebra.Monoid.fst(51,82-51,108); use=FStar.Algebra.Monoid.fst(61,2-61,14)
          (FStar.Algebra.Monoid.associativity_lemma U_zero Prims.nat @x0)))))
      :qid @query.1))))
  :named @query))
(set-option :rlimit 2500000)
(echo "<initial_stats>")
(echo "<statistics>") (get-info :all-statistics) (echo "</statistics>")
(echo "</initial_stats>")
(echo "<result>")
(check-sat)
(echo "</result>")
(set-option :rlimit 0)
(echo "<reason-unknown>") (get-info :reason-unknown) (echo "</reason-unknown>")
(echo "<labels>")
(echo "label_4")
(eval label_4)
(echo "label_3")
(eval label_3)
(echo "label_2")
(eval label_2)
(echo "label_1")
(eval label_1)
(echo "</labels>")
(echo "Done!")
(pop) ;; 0}pop

failedQueries-FStar.DependentMap-1.smt2

; Z3 invocation started by F*
; F* version: 2026.06.07~dev -- commit hash: b2f48b84ce63139b95d6548587e8835bc03c8392
; Z3 version (according to F*): 4.17.0

(set-option :global-decls false)
(set-option :smt.mbqi false)
(set-option :auto_config false)
(set-option :produce-unsat-cores true)
(set-option :model true)
(set-option :smt.case_split 3)
(set-option :smt.relevancy 2)
(set-option :rewriter.enable_der false)
(set-option :rewriter.sort_disjunctions false)
(set-option :pi.decompose_patterns false)
(set-option :smt.arith.solver 6)
(set-option :smt.random-seed 0)


(declare-sort FString)
(declare-fun FString_constr_id (FString) Int)

(declare-sort Term)
(declare-sort Universe)
(declare-fun U_zero () Universe)
(declare-fun U_succ (Universe) Universe)
(declare-fun ulevel ((Universe)) Int)
(declare-fun Univ (Int) Universe)
(assert (= (ulevel U_zero) 0))
(assert (forall ((u Universe)) (! (= (ulevel (U_succ u)) (+ 1 (ulevel u))) :pattern ((ulevel (U_succ u))))))
(assert (forall ((u Universe)) (! (>= (ulevel u) 0) :pattern ((ulevel u)))))
(assert (forall ((u Universe)) (! (= (Univ (ulevel u)) u) :pattern ((ulevel u)))))
(assert (forall ((i Int)) (! (implies (>= i 0) (= (ulevel (Univ i)) i)) :pattern ((Univ i)))))
(declare-fun U_max (Universe Universe) Universe)
(assert (forall ((u1 Universe) (u2 Universe))
(! (= (U_max u1 u2)
(ite (<= (ulevel u1) (ulevel u2)) u2 u1))
:pattern ((U_max u1 u2)))))
(declare-fun U_unif (Int) Universe)
(declare-fun U_unknown () Universe)
(declare-fun Term_constr_id (Term) Int)
(declare-sort Dummy_sort)
(declare-fun Dummy_value () Dummy_sort)
(declare-datatypes () ((Fuel 
(ZFuel) 
(SFuel (prec Fuel)))))
(declare-fun MaxIFuel () Fuel)
(declare-fun MaxFuel () Fuel)
(declare-fun PreType (Term) Term)
(declare-fun Valid (Term) Bool)
(declare-fun HasTypeFuel (Fuel Term Term) Bool)
(define-fun HasTypeZ ((x Term) (t Term)) Bool
(HasTypeFuel ZFuel x t))
(define-fun HasType ((x Term) (t Term)) Bool
(HasTypeFuel MaxIFuel x t))
(declare-fun IsTotFun (Term) Bool)

                ;;fuel irrelevance
(assert (forall ((f Fuel) (x Term) (t Term))
(! (= (HasTypeFuel (SFuel f) x t)
(HasTypeZ x t))
:pattern ((HasTypeFuel (SFuel f) x t)))))
(declare-fun NoHoist (Term Bool) Bool)
;;no-hoist
(assert (forall ((dummy Term) (b Bool))
(! (= (NoHoist dummy b) b)
:pattern ((NoHoist dummy b)))))
(define-fun  IsTyped ((x Term)) Bool
(exists ((t Term)) (HasTypeZ x t)))
(declare-fun ApplyTF (Term Fuel) Term)
(declare-fun ApplyTT (Term Term) Term)
(declare-fun Prec (Term Term) Bool)
(assert (forall ((x Term) (y Term) (z Term))
(! (implies (and (Prec x y) (Prec y z)) (Prec x z))
:pattern ((Prec x z) (Prec x y)))))
(assert (forall ((x Term) (y Term))
(implies (Prec x y)
(not (Prec y x)))))
(declare-fun Closure (Term) Term)
(declare-fun ConsTerm (Term Term) Term)
(declare-fun ConsFuel (Fuel Term) Term)
(declare-fun Tm_uvar (Int) Term)
(define-fun Reify ((x Term)) Term x)
(declare-fun Prims.precedes (Universe Universe Term Term Term Term) Term)
(declare-fun Range_const (Int) Term)
(declare-fun _mul (Int Int) Int)
(declare-fun _div (Int Int) Int)
(declare-fun _mod (Int Int) Int)
(declare-fun __uu__PartialApp () Term)
(assert (forall ((x Int) (y Int)) (! (= (_mul x y) (* x y)) :pattern ((_mul x y)))))
(assert (forall ((x Int) (y Int)) (! (= (_div x y) (div x y)) :pattern ((_div x y)))))
(assert (forall ((x Int) (y Int)) (! (= (_mod x y) (mod x y)) :pattern ((_mod x y)))))
(declare-fun _rmul (Real Real) Real)
(declare-fun _rdiv (Real Real) Real)
(assert (forall ((x Real) (y Real)) (! (= (_rmul x y) (* x y)) :pattern ((_rmul x y)))))
(assert (forall ((x Real) (y Real)) (! (= (_rdiv x y) (/ x y)) :pattern ((_rdiv x y)))))
(define-fun Unreachable () Bool false)
(declare-fun Tm_refinement (Term (=> Term Bool)) Term)
(assert (forall ((x Term) (base Term) (f (=> Term Bool)))
                  (! (iff (and (HasType x base) (select f x))
                          (HasType x (Tm_refinement base f)))
                  :pattern ((HasType x (Tm_refinement base f)))
                  :qid refine_interpretation)))
(assert (forall ((t Term) (base Term) (f (=> Term Bool)))
                  (! (iff (HasType base t)
                          (HasType (Tm_refinement base f) t))
                  :pattern ((HasType (Tm_refinement base f) t))
                  :qid refine_typing)))
(declare-fun Tm_lambda (Term (=> Term Term)) Term)
(assert (forall ((t Term) (f (=> Term Term)) (x Term))
                  (! (implies (HasTypeFuel ZFuel x t)
                              (= (ApplyTT (Tm_lambda t f) x)
                                 (select f x)))
                  :pattern ((ApplyTT (Tm_lambda t f) x))
                  :qid beta_reduction)))
(declare-fun WithType (Term Term) Term)
(assert (forall ((t Term) (ty Term))
                        (! (and (HasType (WithType t ty) ty)
                                (= (WithType t ty) t))
                          :pattern ((WithType t ty)))))
(declare-fun WithInterp (Term Bool) Term)
(assert (forall ((t Term) (interp Bool))
                        (! (and (= (Valid t) interp)
                                (= (WithInterp t interp) t))
                          :pattern ((WithInterp t interp)))))
; <start constructor FString_const>
; Constructor
(declare-fun FString_const (Int) FString)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= 0 (FString_constr_id (FString_const @u0)))
    :pattern ((FString_const @u0))
    :qid constructor_distinct_FString_const))
  :named constructor_distinct_FString_const))
; Projector
(declare-fun FString_const_proj_0 (FString) Int)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= (FString_const_proj_0 (FString_const @u0)) @u0)
    :pattern ((FString_const @u0))
    :qid projection_inverse_FString_const_proj_0))
  :named projection_inverse_FString_const_proj_0))
; Discriminator definition
(define-fun is-FString_const ((__@u0 FString)) Bool
 (and (= (FString_constr_id __@u0) 0) (= __@u0 (FString_const (FString_const_proj_0 __@u0)))))
; </end constructor FString_const>
; <start constructor Tm_type>
; Constructor
(declare-fun Tm_type (Universe) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Universe))
   (! (= 2 (Term_constr_id (Tm_type @u0)))
    :pattern ((Tm_type @u0))
    :qid constructor_distinct_Tm_type))
  :named constructor_distinct_Tm_type))
; Projector
(declare-fun Tm_type_0 (Term) Universe)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Universe))
   (! (= (Tm_type_0 (Tm_type @u0)) @u0) :pattern ((Tm_type @u0)) :qid projection_inverse_Tm_type_0))
  :named projection_inverse_Tm_type_0))
; Discriminator definition
(define-fun is-Tm_type ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 2) (= __@x0 (Tm_type (Tm_type_0 __@x0)))))
; </end constructor Tm_type>
; <start constructor Tm_arrow>
; Constructor
(declare-fun Tm_arrow (Int) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= 3 (Term_constr_id (Tm_arrow @u0)))
    :pattern ((Tm_arrow @u0))
    :qid constructor_distinct_Tm_arrow))
  :named constructor_distinct_Tm_arrow))
; Projector
(declare-fun Tm_arrow_id (Term) Int)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= (Tm_arrow_id (Tm_arrow @u0)) @u0)
    :pattern ((Tm_arrow @u0))
    :qid projection_inverse_Tm_arrow_id))
  :named projection_inverse_Tm_arrow_id))
; Discriminator definition
(define-fun is-Tm_arrow ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 3) (= __@x0 (Tm_arrow (Tm_arrow_id __@x0)))))
; </end constructor Tm_arrow>
; <start constructor Tm_unit>
; Constructor
(declare-fun Tm_unit () Term)
; Constructor distinct
;;; Fact-ids: 
(assert (! (= 6 (Term_constr_id Tm_unit)) :named constructor_distinct_Tm_unit))
; Discriminator definition
(define-fun is-Tm_unit ((__@x0 Term)) Bool (and (= (Term_constr_id __@x0) 6) (= __@x0 Tm_unit)))
; </end constructor Tm_unit>
; <start constructor BoxInt>
; Constructor
(declare-fun BoxInt (Int) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= 7 (Term_constr_id (BoxInt @u0))) :pattern ((BoxInt @u0)) :qid constructor_distinct_BoxInt))
  :named constructor_distinct_BoxInt))
; Projector
(declare-fun BoxInt_proj_0 (Term) Int)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Int))
   (! (= (BoxInt_proj_0 (BoxInt @u0)) @u0)
    :pattern ((BoxInt @u0))
    :qid projection_inverse_BoxInt_proj_0))
  :named projection_inverse_BoxInt_proj_0))
; Discriminator definition
(define-fun is-BoxInt ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 7) (= __@x0 (BoxInt (BoxInt_proj_0 __@x0)))))
; </end constructor BoxInt>
; <start constructor BoxBool>
; Constructor
(declare-fun BoxBool (Bool) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Bool))
   (! (= 8 (Term_constr_id (BoxBool @u0)))
    :pattern ((BoxBool @u0))
    :qid constructor_distinct_BoxBool))
  :named constructor_distinct_BoxBool))
; Projector
(declare-fun BoxBool_proj_0 (Term) Bool)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Bool))
   (! (= (BoxBool_proj_0 (BoxBool @u0)) @u0)
    :pattern ((BoxBool @u0))
    :qid projection_inverse_BoxBool_proj_0))
  :named projection_inverse_BoxBool_proj_0))
; Discriminator definition
(define-fun is-BoxBool ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 8) (= __@x0 (BoxBool (BoxBool_proj_0 __@x0)))))
; </end constructor BoxBool>
; <start constructor BoxString>
; Constructor
(declare-fun BoxString (FString) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 FString))
   (! (= 9 (Term_constr_id (BoxString @u0)))
    :pattern ((BoxString @u0))
    :qid constructor_distinct_BoxString))
  :named constructor_distinct_BoxString))
; Projector
(declare-fun BoxString_proj_0 (Term) FString)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 FString))
   (! (= (BoxString_proj_0 (BoxString @u0)) @u0)
    :pattern ((BoxString @u0))
    :qid projection_inverse_BoxString_proj_0))
  :named projection_inverse_BoxString_proj_0))
; Discriminator definition
(define-fun is-BoxString ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 9) (= __@x0 (BoxString (BoxString_proj_0 __@x0)))))
; </end constructor BoxString>
; <start constructor BoxReal>
; Constructor
(declare-fun BoxReal (Real) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Real))
   (! (= 10 (Term_constr_id (BoxReal @u0)))
    :pattern ((BoxReal @u0))
    :qid constructor_distinct_BoxReal))
  :named constructor_distinct_BoxReal))
; Projector
(declare-fun BoxReal_proj_0 (Term) Real)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@u0 Real))
   (! (= (BoxReal_proj_0 (BoxReal @u0)) @u0)
    :pattern ((BoxReal @u0))
    :qid projection_inverse_BoxReal_proj_0))
  :named projection_inverse_BoxReal_proj_0))
; Discriminator definition
(define-fun is-BoxReal ((__@x0 Term)) Bool
 (and (= (Term_constr_id __@x0) 10) (= __@x0 (BoxReal (BoxReal_proj_0 __@x0)))))
; </end constructor BoxReal>
; <start constructor LexCons>
; Constructor
(declare-fun LexCons (Term Term Term) Term)
; Constructor distinct
;;; Fact-ids: 
(assert
 (! (forall ((@x0 Term) (@x1 Term) (@x2 Term))
   (! (= 11 (Term_constr_id (LexCons @x0 @x1 @x2)))
    :pattern ((LexCons @x0 @x1 @x2))
    :qid constructor_distinct_LexCons))
  :named constructor_distinct_LexCons))
; Projector
(declare-fun LexCons_0 (Term) Term)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@x0 Term) (@x1 Term) (@x2 Term))
   (! (= (LexCons_0 (LexCons @x0 @x1 @x2)) @x0)
    :pattern ((LexCons @x0 @x1 @x2))
    :qid projection_inverse_LexCons_0))
  :named projection_inverse_LexCons_0))
; Projector
(declare-fun LexCons_1 (Term) Term)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@x0 Term) (@x1 Term) (@x2 Term))
   (! (= (LexCons_1 (LexCons @x0 @x1 @x2)) @x1)
    :pattern ((LexCons @x0 @x1 @x2))
    :qid projection_inverse_LexCons_1))
  :named projection_inverse_LexCons_1))
; Projector
(declare-fun LexCons_2 (Term) Term)
; Projection inverse
;;; Fact-ids: 
(assert
 (! (forall ((@x0 Term) (@x1 Term) (@x2 Term))
   (! (= (LexCons_2 (LexCons @x0 @x1 @x2)) @x2)
    :pattern ((LexCons @x0 @x1 @x2))
    :qid projection_inverse_LexCons_2))
  :named projection_inverse_LexCons_2))
; Discriminator definition
(define-fun is-LexCons ((__@x0 Term)) Bool
 (and
  (= (Term_constr_id __@x0) 11)
  (= __@x0 (LexCons (LexCons_0 __@x0) (LexCons_1 __@x0) (LexCons_2 __@x0)))))
; </end constructor LexCons>
(declare-fun Prims.precedes@tok (Universe Universe) Term)
(assert
(forall ((u0 Universe) (u1 Universe) (@x0 Term) (@x1 Term) (@x2 Term) (@x3 Term))
(! (= (ApplyTT (ApplyTT (ApplyTT (ApplyTT (Prims.precedes@tok u0 u1) @x0) @x1) @x2) @x3)
(Prims.precedes u0 u1 @x0 @x1 @x2 @x3))
:pattern ((ApplyTT (ApplyTT (ApplyTT (ApplyTT (Prims.precedes@tok u0 u1) @x0) @x1) @x2) @x3)))))

(define-fun is-Prims.LexCons ((t Term)) Bool 
(is-LexCons t))
(declare-fun Prims.lex_t () Term)
(declare-fun LexTop () Term)
(assert (forall ((u0 Universe) (u1 Universe) (t1 Term) (t2 Term) (x1 Term) (x2 Term) (y1 Term) (y2 Term))
(iff (Valid (Prims.precedes u0 u1 Prims.lex_t Prims.lex_t (LexCons t1 x1 x2) (LexCons t2 y1 y2)))
(or (Valid (Prims.precedes u0 u1 t1 t2 x1 y1))
(and (= x1 y1)
(Valid (Prims.precedes u0 u1 Prims.lex_t Prims.lex_t x2 y2)))))))
(assert (forall ((u0 Universe) (u1 Universe) (t1 Term) (t2 Term) (e1 Term) (e2 Term))
(! (iff (Valid (Prims.precedes u0 u1 t1 t2 e1 e2))
(Valid (Prims.precedes U_zero U_zero Prims.lex_t Prims.lex_t e1 e2)))
:pattern (Prims.precedes u0 u1 t1 t2 e1 e2))))
(assert (forall ((u0 Universe) (u1 Universe) (t1 Term) (t2 Term))
(! (iff (Valid (Prims.precedes u0 u1 Prims.lex_t Prims.lex_t t1 t2)) 
(Prec t1 t2))
:pattern ((Prims.precedes u0 u1 Prims.lex_t Prims.lex_t t1 t2)))))
(assert (forall ((u Universe) (t Term))
(! (iff (HasType (Tm_type u) t)
(= t (Tm_type (U_succ u))))
:pattern ((HasType (Tm_type u) t)))))

; Constructor
(declare-fun FStar.DependentMap.Mkt (Universe Term Term Term) Term)
; Projector
(declare-fun FStar.DependentMap.Mkt_@0 (Term) Universe)
; Projector
(declare-fun FStar.DependentMap.Mkt_@key (Term) Term)
; Projector
(declare-fun FStar.DependentMap.Mkt_@mappings (Term) Term)
; Projector
(declare-fun FStar.DependentMap.Mkt_@value (Term) Term)
(declare-fun FStar.DependentMap.__proj__Mkt__item__mappings (Universe Term Term Term) Term)
(declare-fun FStar.DependentMap.__proj__Mkt__item__mappings@tok (Universe) Term)
(declare-fun FStar.DependentMap.sel (Universe Term Term Term Term) Term)
; Constructor
(declare-fun FStar.DependentMap.t (Universe Term Term) 

... (truncated due to discussion size limits)

### Run
- Workflow run: https://github.com/Z3Prover/z3/actions/runs/27239186162