Bloat6.smt2

; Starting query at ./bloat6.fst(5,29-8,68)
;;;;;;;;;;;;;;;;n#54 : Bloat6.nat (Bloat6.nat)
(declare-fun x_a42ae5f759af5bb08f7f27c259de7ecb_0 () Term)
;;;;;;;;;;;;;;;;binder_x_a42ae5f759af5bb08f7f27c259de7ecb_0
(assert (!
(HasType x_a42ae5f759af5bb08f7f27c259de7ecb_0
Bloat6.nat)
:named binder_x_a42ae5f759af5bb08f7f27c259de7ecb_0))
(declare-fun Tm_refine_132efab4ca0e1877b81a374a0ce191e7 (Term) Term)
;;;;;;;;;;;;;;;;refinement kinding
(assert (!
(forall ((@x0 Term))
 (! (HasType (Tm_refine_132efab4ca0e1877b81a374a0ce191e7 @x0)
Tm_type)
  
:pattern ((HasType (Tm_refine_132efab4ca0e1877b81a374a0ce191e7 @x0)
Tm_type))))
:named refinement_kinding_Tm_refine_132efab4ca0e1877b81a374a0ce191e7))
;;;;;;;;;;;;;;;;(uu___#58:Bloat6.nat{(Prims.precedes uu___@0 n#54)})
(assert (!
(forall ((@u0 Fuel) (@x1 Term) (@x2 Term))
 (! (iff (HasTypeFuel @u0
@x1
(Tm_refine_132efab4ca0e1877b81a374a0ce191e7 @x2))
(and (HasTypeFuel @u0
@x1
@x2)
(Valid (Prims.precedes @x2
@x2
@x1
x_a42ae5f759af5bb08f7f27c259de7ecb_0))))
  
:pattern ((HasTypeFuel @u0
@x1
(Tm_refine_132efab4ca0e1877b81a374a0ce191e7 @x2)))))
:named refinement_interpretation_Tm_refine_132efab4ca0e1877b81a374a0ce191e7))
;;;;;;;;;;;;;;;;haseq for Tm_refine_132efab4ca0e1877b81a374a0ce191e7
(assert (!
(forall ((@x0 Term))
 (! (iff (Valid (Prims.hasEq (Tm_refine_132efab4ca0e1877b81a374a0ce191e7 @x0)))
(Valid (Prims.hasEq @x0)))
  
:pattern ((Valid (Prims.hasEq (Tm_refine_132efab4ca0e1877b81a374a0ce191e7 @x0))))))
:named haseqTm_refine_132efab4ca0e1877b81a374a0ce191e7))
(declare-fun Bloat6.factorial (Term) Term)
;;;;;;;;;;;;;;;;(uu___#719:(uu___#58:Bloat6.nat{(Prims.precedes uu___@0 n#54)}) -> Tot Bloat6.nat)
(declare-fun Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f (Term) Term)
;;;;;;;;;;;;;;;;kinding_Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f
(assert (!
(forall ((@x0 Term))
 (! (HasType (Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f @x0)
Tm_type)
  
:pattern ((HasType (Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f @x0)
Tm_type))))
:named kinding_Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f))
;;;;;;;;;;;;;;;;pre-typing for functions
(assert (!
(forall ((@u0 Fuel) (@x1 Term) (@x2 Term))
 (! (implies (HasTypeFuel @u0
@x1
(Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f @x2))
(is-Tm_arrow (PreType @x1)))
  
:pattern ((HasTypeFuel @u0
@x1
(Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f @x2)))))
:named pre_typing_Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f))
;;;;;;;;;;;;;;;;interpretation_Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f
(assert (!
(forall ((@x0 Term) (@x1 Term))
 (! (iff (HasTypeZ @x0
(Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f @x1))
(forall ((@x2 Term))
 (! (implies (HasType @x2
(Tm_refine_132efab4ca0e1877b81a374a0ce191e7 @x1))
(HasType (ApplyTT @x0
@x2)
@x1))
  
:pattern ((ApplyTT @x0
@x2)))))
  
:pattern ((HasTypeZ @x0
(Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f @x1)))))
:named interpretation_Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f))
(declare-fun Bloat6.factorial@tok () Term)
;;;;;;;;;;;;;;;;fresh token
(assert (!
(= 1970
(Term_constr_id Bloat6.factorial@tok))
:named fresh_token_Bloat6.factorial@tok))
;;;;;;;;;;;;;;;;Name-token correspondence
(assert (!
(forall ((@x0 Term))
 (! (= (ApplyTT Bloat6.factorial@tok
@x0)
(Bloat6.factorial @x0))
  
:pattern ((ApplyTT Bloat6.factorial@tok
@x0))

:pattern ((Bloat6.factorial @x0))))
:named token_correspondence_Bloat6.factorial))
;;;;;;;;;;;;;;;;function token typing
(assert (!
(HasType Bloat6.factorial@tok
(Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f Bloat6.nat))
:named function_token_typing_Bloat6.factorial))
;;;;;;;;;;;;;;;;free var typing
(assert (!
(forall ((@x0 Term))
 (! (implies (HasType @x0
(Tm_refine_132efab4ca0e1877b81a374a0ce191e7 Bloat6.nat))
(HasType (Bloat6.factorial @x0)
Bloat6.nat))
  
:pattern ((Bloat6.factorial @x0))))
:named typing_Bloat6.factorial))
(declare-fun label_38 () Bool)
(declare-fun label_37 () Bool)
(declare-fun label_36 () Bool)
(declare-fun label_35 () Bool)
(declare-fun label_34 () Bool)
(declare-fun label_33 () Bool)
(declare-fun label_32 () Bool)
(push)

; <fuel='2' ifuel='1'>
(assert (= MaxFuel
(SFuel (SFuel ZFuel))))
(assert (= MaxIFuel
(SFuel ZFuel)))
;;;;;;;;;;;;;;;;query
(assert (!
(not (forall ((@x0 Term))
 (implies (and (= @x0
x_a42ae5f759af5bb08f7f27c259de7ecb_0)
(HasType @x0
Bloat6.nat))
(forall ((@x1 Term))
 (implies (and (= @x1
(BoxInt 0))
(HasType @x1
Prims.int))
(forall ((@x2 Term))
 (implies (and (HasType @x2
Prims.bool)
(= @x2
(Prims.op_Equality Prims.int
x_a42ae5f759af5bb08f7f27c259de7ecb_0
(BoxInt 0))))
(forall ((@x3 Term))
 (implies (and (= @x3
@x2)
(HasType @x3
Prims.bool))
(forall ((@x4 Term))
 (implies (and (forall ((@x5 Term))
 (! (iff (Valid (ApplyTT @x4
@x5))
true)
 :weight 0
 
:pattern ((ApplyTT @x4
@x5))))
(HasType @x4
(Prims.pure_post Bloat6.nat)))
(and (implies (not (= @x3
(BoxBool true)))
(forall ((@x5 Term))
 (implies (and (= @x3
@x5)
(HasType @x5
Prims.bool))
(and (forall ((@x6 Term))
 (implies (and (= @x6
(Prims.op_Subtraction x_a42ae5f759af5bb08f7f27c259de7ecb_0
(BoxInt 1)))
(HasType @x6
(Tm_refine_132efab4ca0e1877b81a374a0ce191e7 Bloat6.nat)))
(forall ((@x7 Term))
 (implies (and (HasType @x7
Bloat6.nat)
(= @x7
(Bloat6.factorial (Prims.op_Subtraction x_a42ae5f759af5bb08f7f27c259de7ecb_0
(BoxInt 1)))))
(forall ((@x8 Term))
 (implies (and (= @x8
@x7)
(HasType @x8
Bloat6.nat))
(forall ((@x9 Term))
 (implies (and (HasType @x9
Prims.int)
(= @x9
(Prims.op_Multiply x_a42ae5f759af5bb08f7f27c259de7ecb_0
(Bloat6.factorial (Prims.op_Subtraction x_a42ae5f759af5bb08f7f27c259de7ecb_0
(BoxInt 1))))))
(forall ((@x10 Term))
 (implies (and (= @x10
@x9)
(HasType @x10
Prims.int))
(and (forall ((@x11 Term))
 (implies (and (= @x11
@x10)
(HasType @x11
Bloat6.nat))
(or label_37
(Valid (ApplyTT @x4
@x11)))));;no pats

(or label_36
(>= (BoxInt_proj_0 @x10)
(BoxInt_proj_0 (BoxInt 0)))))));;no pats
));;no pats
));;no pats
));;no pats
));;no pats

(or label_35
(Valid (Prims.precedes Bloat6.nat
Bloat6.nat
(Prims.op_Subtraction x_a42ae5f759af5bb08f7f27c259de7ecb_0
(BoxInt 1))
x_a42ae5f759af5bb08f7f27c259de7ecb_0)))
(or label_34
(>= (BoxInt_proj_0 (Prims.op_Subtraction x_a42ae5f759af5bb08f7f27c259de7ecb_0
(BoxInt 1)))
(BoxInt_proj_0 (BoxInt 0)))))));;no pats
)
(implies (= @x3
(BoxBool true))
(and (forall ((@x5 Term))
 (implies (and (= @x5
(BoxInt 1))
(HasType @x5
Prims.int))
(or label_33
(Valid (ApplyTT @x4
@x5)))));;no pats

(or label_32
(>= (BoxInt_proj_0 (BoxInt 1))
(BoxInt_proj_0 (BoxInt 0)))))))));;no pats
));;no pats
));;no pats
));;no pats
));;no pats
)
:named @query))
(set-option :timeout 5000)
(check-sat)
(echo "label_38")
(eval label_38)
(echo "label_37")
(eval label_37)
(echo "label_36")
(eval label_36)
(echo "label_35")
(eval label_35)
(echo "label_34")
(eval label_34)
(echo "label_33")
(eval label_33)
(echo "label_32")
(eval label_32)
(echo "Done!")
(pop)
(pop)

; Ending query at ./bloat6.fst(5,29-8,68)
(push)

; Starting query at ./bloat6.fst(8,11-8,16)
;;;;;;;;;;;;;;;;n#54 : Bloat6.nat (Bloat6.nat)
(declare-fun x_a42ae5f759af5bb08f7f27c259de7ecb_0 () Term)
;;;;;;;;;;;;;;;;binder_x_a42ae5f759af5bb08f7f27c259de7ecb_0
(assert (!
(HasType x_a42ae5f759af5bb08f7f27c259de7ecb_0
Bloat6.nat)
:named binder_x_a42ae5f759af5bb08f7f27c259de7ecb_0))
(declare-fun Tm_refine_132efab4ca0e1877b81a374a0ce191e7 (Term) Term)
;;;;;;;;;;;;;;;;refinement kinding
(assert (!
(forall ((@x0 Term))
 (! (HasType (Tm_refine_132efab4ca0e1877b81a374a0ce191e7 @x0)
Tm_type)
  
:pattern ((HasType (Tm_refine_132efab4ca0e1877b81a374a0ce191e7 @x0)
Tm_type))))
:named refinement_kinding_Tm_refine_132efab4ca0e1877b81a374a0ce191e7))
;;;;;;;;;;;;;;;;(uu___#58:Bloat6.nat{(Prims.precedes uu___@0 n#54)})
(assert (!
(forall ((@u0 Fuel) (@x1 Term) (@x2 Term))
 (! (iff (HasTypeFuel @u0
@x1
(Tm_refine_132efab4ca0e1877b81a374a0ce191e7 @x2))
(and (HasTypeFuel @u0
@x1
@x2)
(Valid (Prims.precedes @x2
@x2
@x1
x_a42ae5f759af5bb08f7f27c259de7ecb_0))))
  
:pattern ((HasTypeFuel @u0
@x1
(Tm_refine_132efab4ca0e1877b81a374a0ce191e7 @x2)))))
:named refinement_interpretation_Tm_refine_132efab4ca0e1877b81a374a0ce191e7))
;;;;;;;;;;;;;;;;haseq for Tm_refine_132efab4ca0e1877b81a374a0ce191e7
(assert (!
(forall ((@x0 Term))
 (! (iff (Valid (Prims.hasEq (Tm_refine_132efab4ca0e1877b81a374a0ce191e7 @x0)))
(Valid (Prims.hasEq @x0)))
  
:pattern ((Valid (Prims.hasEq (Tm_refine_132efab4ca0e1877b81a374a0ce191e7 @x0))))))
:named haseqTm_refine_132efab4ca0e1877b81a374a0ce191e7))
(declare-fun Bloat6.factorial (Term) Term)
;;;;;;;;;;;;;;;;(uu___#861:(uu___#58:Bloat6.nat{(Prims.precedes uu___@0 n#54)}) -> Tot Bloat6.nat)
(declare-fun Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f (Term) Term)
;;;;;;;;;;;;;;;;kinding_Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f
(assert (!
(forall ((@x0 Term))
 (! (HasType (Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f @x0)
Tm_type)
  
:pattern ((HasType (Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f @x0)
Tm_type))))
:named kinding_Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f))
;;;;;;;;;;;;;;;;pre-typing for functions
(assert (!
(forall ((@u0 Fuel) (@x1 Term) (@x2 Term))
 (! (implies (HasTypeFuel @u0
@x1
(Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f @x2))
(is-Tm_arrow (PreType @x1)))
  
:pattern ((HasTypeFuel @u0
@x1
(Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f @x2)))))
:named pre_typing_Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f))
;;;;;;;;;;;;;;;;interpretation_Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f
(assert (!
(forall ((@x0 Term) (@x1 Term))
 (! (iff (HasTypeZ @x0
(Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f @x1))
(forall ((@x2 Term))
 (! (implies (HasType @x2
(Tm_refine_132efab4ca0e1877b81a374a0ce191e7 @x1))
(HasType (ApplyTT @x0
@x2)
@x1))
  
:pattern ((ApplyTT @x0
@x2)))))
  
:pattern ((HasTypeZ @x0
(Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f @x1)))))
:named interpretation_Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f))
(declare-fun Bloat6.factorial@tok () Term)
;;;;;;;;;;;;;;;;fresh token
(assert (!
(= 1976
(Term_constr_id Bloat6.factorial@tok))
:named fresh_token_Bloat6.factorial@tok))
;;;;;;;;;;;;;;;;Name-token correspondence
(assert (!
(forall ((@x0 Term))
 (! (= (ApplyTT Bloat6.factorial@tok
@x0)
(Bloat6.factorial @x0))
  
:pattern ((ApplyTT Bloat6.factorial@tok
@x0))

:pattern ((Bloat6.factorial @x0))))
:named token_correspondence_Bloat6.factorial))
;;;;;;;;;;;;;;;;function token typing
(assert (!
(HasType Bloat6.factorial@tok
(Tm_arrow_42f0a006b2c21701d9516d8b8c024d2f Bloat6.nat))
:named function_token_typing_Bloat6.factorial))
;;;;;;;;;;;;;;;;free var typing
(assert (!
(forall ((@x0 Term))
 (! (implies (HasType @x0
(Tm_refine_132efab4ca0e1877b81a374a0ce191e7 Bloat6.nat))
(HasType (Bloat6.factorial @x0)
Bloat6.nat))
  
:pattern ((Bloat6.factorial @x0))))
:named typing_Bloat6.factorial))
(declare-fun label_40 () Bool)
(declare-fun label_39 () Bool)
(push)

; <fuel='2' ifuel='1'>
(assert (= MaxFuel
(SFuel (SFuel ZFuel))))
(assert (= MaxIFuel
(SFuel ZFuel)))
;;;;;;;;;;;;;;;;query
(assert (!
(not (and (or label_40
(Valid (Prims.hasEq Prims.int)))
(forall ((@x0 Term))
 (implies (and (Valid (Prims.hasEq @x0))
(HasType @x0
Tm_type))
(or label_39
(Valid (Prims.hasEq @x0)))));;no pats
))
:named @query))
(set-option :timeout 5000)
(check-sat)
(echo "label_40")
(eval label_40)
(echo "label_39")
(eval label_39)
(echo "Done!")
(pop)