(def-theorem archimedean 
    "forall(a:rr,forsome(n:zz,a<n))"
    (theory h-o-real-arithmetic)
    (proof 
      (
        direct-and-antecedent-inference-strategy
        (instantiate-theorem completeness ("lambda(j:zz, truth)"))
        (block (script-comment "node added by `instantiate-theorem' at (0 0 0)")
	      (instantiate-universal-antecedent "with(p:prop,p);" ("1"))
	      (contrapose "with(p:prop,p);")
	      simplify)
        (block (script-comment "node added by `instantiate-theorem' at (0 0 1)")
	      (contrapose "with(p:prop,p);")
	      (instantiate-existential ("a"))
	      (instantiate-universal-antecedent "with(p:prop,forall(n:zz,p));"
					          ("theta"))
	      simplify)
        (block (script-comment "node added by `instantiate-theorem' at (0 1 0 0)")
	      (contrapose "with(gamma:rr,p:prop,
    forall(gamma_1:rr,
        forall(theta:rr,p) implies gamma<=gamma_1));")
	      (instantiate-existential ("gamma-1"))
	      (prove-by-logic-and-simplification 3)
	      simplify)
        )))

(def-constant convergent%to%infinity 
    "lambda(s:[zz,rr],
                  forall(m:rr,forsome(x:zz, forall(j:zz, x<=j implies m<=s(j)))))"
    (theory h-o-real-arithmetic))

(def-theorem convergent%to%infinity-linear-form 
    "forall(a,b:rr, 0<a implies convergent%to%infinity(lambda(j:zz,a*j+b)))"
    (theory h-o-real-arithmetic)
    
    (proof
      (
        (unfold-single-defined-constant (0) convergent%to%infinity)
        direct-and-antecedent-inference-strategy
        (force-substitution "forall(j_$0:zz,x_$0<=j_$0 implies m_$0<=a*j_$0+b)" "a^[-1]*(m_$0-b)<x_$0" (0))
        (apply-macete-with-minor-premises archimedean)
        (force-substitution "m_$0<=a*j_$0+b" "a^[-1]*(m_$0-b)<j_$0" (0))
        direct-and-antecedent-inference-strategy
        simplify
        (apply-macete-with-minor-premises fractional-expression-manipulation)
        simplify
        )))

(def-theorem bernoullis-inequality 
    "forall(h:rr,n:zz,-1<h and 1<=n implies 1+n*h<=(1+h)^n)"
    (theory h-o-real-arithmetic)
    (proof 
      (
        (induction integer-inductor ("n"))
        (cut-with-single-formula "0<=t*h^2 and (1+h)*(1+h*t)<=(1+h)*(1+h)^t")
        simplify
        simplify
        )))

(def-theorem unbounded-heredity 
    "forall(s,t:[zz,rr],convergent%to%infinity(s) and forsome(m:zz,forall(n:zz,m<=n implies s(n)<=t(n))) implies convergent%to%infinity(t))"
    (theory h-o-real-arithmetic)
    (proof
      (
        unfold-defined-constants
        direct-and-antecedent-inference-strategy
        (instantiate-universal-antecedent "with(p:prop,forall(m:rr,forsome(x:zz,p)));"
				            ("m"))
        (instantiate-existential ("max(m_$0,x)"))
        (apply-macete-with-minor-premises transitivity-of-<=)
        (block (script-comment "node added by `apply-macete-with-minor-premises' at (0)")
	      (instantiate-existential ("s(j_$0)"))
	      (block (script-comment "node added by `instantiate-existential' at (0 0)")
		    (backchain "with(s:[zz,rr],m:rr,x:zz,forall(j:zz,x<=j implies m<=s(j)));")
		    (apply-macete-with-minor-premises transitivity-of-<=)
		    (instantiate-existential ("max(m_$0,x)"))
		    (apply-macete-with-minor-premises maximum-2nd-arg))
	      (block (script-comment "node added by `instantiate-existential' at (0 1)")
		    (backchain "with(t,s:[zz,rr],m_$0:zz,
    forall(n:zz,m_$0<=n implies s(n)<=t(n)));")
		    (apply-macete-with-minor-premises transitivity-of-<=)
		    (instantiate-existential ("max(m_$0,x)"))
		    (apply-macete-with-minor-premises maximum-1st-arg))
	      (cut-with-single-formula "s(j_$0)<=t(j_$0)"))
        (cut-with-single-formula "s(j_$0)<=t(j_$0)"))))

(def-theorem r^n-convergent-to-infinity 
    "forall(r:rr,1<r implies convergent%to%infinity(lambda(n:zz,r^n)))"
    (theory h-o-real-arithmetic)
    (proof
      (
        
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises unbounded-heredity)
        (instantiate-existential ("lambda(k:zz, (r-1)*k+1)"))
        (block (script-comment "node added by `instantiate-existential' at (0 0)")
	      (apply-macete-with-minor-premises convergent%to%infinity-linear-form)
	      simplify)
        (block (script-comment "node added by `instantiate-existential' at (0 1)")
	      beta-reduce-repeatedly
	      (force-substitution "(r-1)*n_$0+1<=r^n_$0"
			              "1+n_$0*(r-1)<=(1+(r-1))^n_$0"
			              (0))
	      (block (script-comment "node added by `force-substitution' at (0)")
		    (apply-macete-with-minor-premises bernoullis-inequality)
		    (instantiate-existential ("1"))
		    simplify)
	      simplify)
        )))

(def-theorem complete-induction 
    "forall(p:[zz,prop],n:zz,
          forall(m:zz,
              n<=m and forall(k:zz,n<=k and k<m implies p(k))
                implies 
              p(m))
            implies 
          forall(k:zz,n<=k implies p(k)))"
    (theory h-o-real-arithmetic)
    (proof
      (
        
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "forall(k:zz,n<=k implies forall(s:zz, n<=s and s<= k implies p(s)))")
        (block (script-comment "node added by `cut-with-single-formula' at (0)")
	      (backchain "with(p:prop,n:zz,forall(k:zz,n<=k implies forall(s:zz,p)));")
	      (instantiate-existential ("k"))
	      simplify)
        (block (script-comment "node added by `cut-with-single-formula' at (1)")
	      (weaken (0))
	      (induction integer-inductor ())
	      (block (script-comment "node added by `induction' at (0 0 0)")
		    direct-and-antecedent-inference-strategy
		    (backchain "with(p:prop,forall(m:zz,p));")
		    direct-and-antecedent-inference-strategy
		    (contrapose "with(n,s_$0:zz,s_$0<=n);")
		    simplify)
	      (prove-by-logic-and-simplification 3))
        )))

(def-theorem complete-induction-schema 
  Remark: This entry is multiply defined. See:  [1] [2]
    "forall(p:[zz,prop],n:zz,
                    forall(k:zz,n<=k implies p(k))
                      iff
                    (truth
                        and
                    forall(m:zz,
                      n<=m and forall(k:zz,n<=k and k<m implies p(k))
                        implies 
                        p(m))))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (backchain "with(p:[zz,prop],n:zz,forall(k:zz,n<=k implies p(k)));")
        (apply-macete-with-minor-premises complete-induction)
        (instantiate-existential ("n"))
        )))

(def-inductor complete-inductor
    complete-induction-schema
    (theory h-o-real-arithmetic))

(def-theorem well-ordering-for-integers 
    "forall(s:[zz,prop],forsome(y:zz,s(y)) and
          forsome(n:zz, forall(m:zz,m<=n implies not(s(m))))
                    implies
          forsome(u:zz, s(u) and forall(v:zz,v<u implies not s(v))))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (contrapose "with(y:zz,s:[zz,prop],s(y));")
        (cut-with-single-formula "y<=n or n<=y")
        (antecedent-inference "with(n,y:zz,y<=n or n<=y);")
        (backchain "with(s:[zz,prop],n:zz,forall(m:zz,m<=n implies not(s(m))));")
        (incorporate-antecedent "with(y,n:zz,n<=y);")
        (force-substitution "not s(y)" "lambda (z:zz,not s(z))(y)" (0))
        (apply-macete-with-minor-premises complete-induction)
        beta-reduce-repeatedly
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("n"))
        (backchain "with(s:[zz,prop],
    forall(u:zz,not(s(u)) or forsome(v:zz,v<u and s(v))));")
        direct-and-antecedent-inference-strategy
        (case-split ("n<=v"))
        (prove-by-logic-and-simplification 3)
        simplify
        beta-reduce-repeatedly
        simplify
        )))

(def-constant set%min 
    "lambda(s:sets[zz], iota(k:zz, k in s and forall(j:zz, j<k implies not(j in s))))"
    (theory h-o-real-arithmetic))

(def-theorem iota-free-characterization-of-set%min 
    "forall(s:sets[zz],k:zz,  set%min(s)=k iff (k in s and forall(j:zz, j<k implies not(j in s))))"
    (theory h-o-real-arithmetic)
    (proof
      (
        (unfold-single-defined-constant-globally set%min)
        direct-and-antecedent-inference-strategy
        (block 
            (script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0)")
            (contrapose "with(p:prop,p);")
            (apply-macete-with-minor-premises eliminate-iota-macete)
            (contrapose "with(p:prop,p);"))
        (block 
            (script-comment "`direct-and-antecedent-inference-strategy' at (0 0 1 0 0)")
            (contrapose "with(k,z:zz,z=k);")
            (apply-macete-with-minor-premises eliminate-iota-macete)
            (contrapose "with(j:zz,s:sets[zz],j in s);")
            simplify)
        (block 
            (script-comment "`direct-and-antecedent-inference-strategy' at (0 1 0)")
            (apply-macete-with-minor-premises eliminate-iota-macete)
            direct-and-antecedent-inference-strategy
            (contrapose "with(b:zz,s:sets[zz],b in s);")
            (backchain "with(s:sets[zz],k:zz,forall(j:zz,j<k implies not(j in s)));")
            (contrapose "with(k:zz,s:sets[zz],k in s);")
            (backchain "with(s:sets[zz],b:zz,forall(j:zz,j<b implies not(j in s)));")
            simplify)
        )))

(def-theorem definedness-of-set%min 
    "forall(s:sets[zz], 
          #(set%min(s)) iff 
          (forsome(k:zz, k in s) and forsome(k:zz, forall(j:zz, j<=k implies not(j in s)))))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-inference
        direct-inference
        (block 
            (script-comment "`direct-inference' at (0)")
            (cut-with-single-formula "forsome(k:zz, set%min(s)=k)")
            (move-to-sibling 1)
            (instantiate-existential ("set%min(s)"))
            (block 
	(script-comment "`cut-with-single-formula' at (0)")
	(antecedent-inference "with(p:prop,forsome(k:zz,p));")
	(incorporate-antecedent "with(k,z:zz,z=k);")
	(apply-macete-with-minor-premises iota-free-characterization-of-set%min)
	direct-and-antecedent-inference-strategy
	(instantiate-existential ("k"))
	(block 
	    (script-comment "`direct-and-antecedent-inference-strategy' at (0 1 0 0)")
	    (instantiate-existential ("k-1"))
	    simplify)))
        (block 
            (script-comment "`direct-inference' at (1)")
            (cut-with-single-formula "forsome(k:zz, set%min(s)=k)")
            (antecedent-inference "with(p:prop,forsome(k:zz,p));")
            (block 
	(script-comment "`cut-with-single-formula' at (1)")
	(apply-macete-with-minor-premises iota-free-characterization-of-set%min)
	(instantiate-theorem well-ordering-for-integers
			          ("lambda(k:zz, k in s)"))
	(block 
	    (script-comment "`instantiate-theorem' at (0 0 0)")
	    (contrapose "with(p:prop,forall(y:zz,p));")
	    simplify-insistently)
	(block 
	    (script-comment "`instantiate-theorem' at (0 0 1)")
	    (contrapose "with(p:prop,forall(n:zz,p));")
	    simplify)
	(block 
	    (script-comment "`instantiate-theorem' at (0 1 0 0)")
	    (beta-reduce-antecedent "with(s:sets[zz],u:zz,
    forall(v:zz,v<u implies not(lambda(k:zz,k in s)(v))));")
	    (beta-reduce-antecedent "with(u:zz,s:sets[zz],lambda(k:zz,k in s)(u));")
	    (instantiate-existential ("u")))))
        )))

(def-theorem well-ordering-for-natural-numbers 
    "forall(s:[nn,prop],
          nonvacuous_q{s}
                    implies
          forsome(u:nn, s(u) and forall(v:nn,v<u implies not s(v))))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-theorem well-ordering-for-integers ("s"))
        (instantiate-universal-antecedent "with(p:prop, forall(y:zz,p))" ("x_0"))
        (instantiate-universal-antecedent "with(p:prop, forall(n:zz,p))" ("[-1]"))
        (cut-with-single-formula "not(#(m,nn))")
        (apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic)
        simplify
        auto-instantiate-existential
        (backchain "with(p:prop, forall(v:zz,p))")
        )))

(def-constant floor 
    "lambda(x:rr, iota(z:zz,z<=x and x<1+z))"
    (theory h-o-real-arithmetic))

(def-theorem floor-definedness 
    "forall(x:rr, #(floor(x)))"
    (usages d-r-convergence)
    (proof
      (
        insistent-direct-inference
        unfold-defined-constants
        (eliminate-iota 0)
        (cut-with-single-formula "forsome(y%iota:zz,y%iota<=x and x<1+y%iota)")
        (instantiate-existential ("y%iota"))
        simplify
        (instantiate-theorem well-ordering-for-integers ("lambda(u:zz,x<u)"))
        (contrapose 0)
        beta-reduce-insistently
        (apply-macete-with-minor-premises archimedean)
        (contrapose 0)
        (cut-with-single-formula "forsome(u:zz,-x<u)")
        (instantiate-existential ("-u"))
        simplify
        (apply-macete-with-minor-premises archimedean)
        (instantiate-existential ("u-1"))
        (instantiate-universal-antecedent 0 ("u-1"))
        simplify
        (contrapose 0)
        simplify
        (simplify-antecedent 0)
        simplify
))
    
    (theory h-o-real-arithmetic))

(def-theorem floor-characterization 
    "forall(x:rr, n:zz, floor(x)=n iff (n<=x and x<n+1))"
    (theory h-o-real-arithmetic)
    (proof
      (
        (unfold-single-defined-constant (0) floor)
        (apply-macete-with-minor-premises eliminate-iota-macete)
        direct-and-antecedent-inference-strategy
        simplify
        simplify
        simplify
        )))

(def-theorem floor-below-arg 
    "forall(x:rr, floor(x)<=x)"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-inference
        (instantiate-theorem floor-definedness ("x"))
        (incorporate-antecedent "with(p:prop,p);")
        (unfold-single-defined-constant-globally floor)
        direct-and-antecedent-inference-strategy
        (eliminate-defined-iota-expression 0 i))))

(def-theorem floor-plus-1-exceeds-arg 
    "forall(x:rr, x<1+floor(x))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-inference
        (instantiate-theorem floor-definedness ("x"))
        (incorporate-antecedent "with(p:prop,p);")
        (unfold-single-defined-constant-globally floor)
        direct-and-antecedent-inference-strategy
        (eliminate-defined-iota-expression 0 i))))

(def-theorem floor-not-much-below-arg 
    "forall(x:rr, n:zz, n<=x implies n<=floor(x))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-theorem floor-definedness ("x"))
        (incorporate-antecedent "with(z:zz,#(z));")
        (unfold-single-defined-constant-globally floor)
        direct-and-antecedent-inference-strategy
        (eliminate-defined-iota-expression 0 f)
        simplify)))

(def-theorem floor-inequality-characterization 
    "forall(x,y:rr, (floor(x)<=floor(y) iff floor(x)<=y))"
    (theory h-o-real-arithmetic)
    (proof
      (direct-and-antecedent-inference-strategy-with-simplification)))

(def-theorem monotonicity-of-floor 
    "forall(x,y:rr, x<=y implies floor(x)<=floor(y))"
    (theory h-o-real-arithmetic)
    (proof
      (simplify)))

(def-theorem integer-exponentiation-definedness  
    "forall(m,n:zz, 1<=n implies #(m^n,zz))"
    (theory h-o-real-arithmetic)
    (proof
      (
        (induction integer-inductor ())
        (apply-macete-with-minor-premises exp-out)
        sort-definedness
        simplify)))

(def-theorem integer-exponentiation-definedness-dr 
    "forall(m,n:ind, #(m,zz) and #(n,zz) and 1<=n implies #(m^n,zz))"
    (usages d-r-convergence)
    (theory h-o-real-arithmetic)
    (proof
      (
        (apply-macete-with-minor-premises integer-exponentiation-definedness)
        simplify)))

(def-theorem product-power-is-iterated-power 
    "forall(z:rr, n,m:zz, 1<=n and 1<=m implies z^(n*m) ==(z^n)^m)"
    (theory h-o-real-arithmetic)
    (proof
      (
        simplify)))

(def-constant mod 
    "lambda(a,b:rr, a-b*floor(a/b))"
    (theory h-o-real-arithmetic))

(def-theorem mod-of-negative 
    "forall(a,b:rr, mod(-b,-a)==-mod(b,a))"
    (theory h-o-real-arithmetic)
    (proof
      (
          
        (unfold-single-defined-constant-globally mod)
        simplify
        )))

(def-constant div 
    "lambda(x,y:rr, floor(x/y))"
    (theory h-o-real-arithmetic))

(def-theorem mod-of-integer-is-integer 
    "forall(a,b:zz, not(b=0) implies #(a mod b,zz))"
    (theory h-o-real-arithmetic)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (unfold-single-defined-constant (0) mod)
        sort-definedness
        )))