(def-language three-place-predicate
    (embedded-language generic-theory-1)
      (constants (rel "[ind_1,ind_1,ind_1 -> prop]")
    ))

(def-theory three-place-predicate-theory 
    (language three-place-predicate)
    (component-theories generic-theory-1)
      )

(def-constant rel%closed 
    "lambda(s:sets[ind_1],forall(x,y,z:ind_1,x in s and y in s and rel(x,y,z)
              implies z in s))"
    (theory three-place-predicate-theory))

(def-constant rel%closure 
    "lambda(s:sets[ind_1],iota(t:sets[ind_1],rel%closed(t) and s subseteq t and
        forall(u:sets[ind_1], rel%closed(u) and s subseteq u
              implies t subseteq u)))"
    (theory three-place-predicate-theory))

(def-theorem iota-free-characterization-of-rel%closure 
    "forall(s,t:sets[ind_1],rel%closure(s)=t iff (s subseteq t and
          rel%closed(t) and
        forall(u:sets[ind_1],s subseteq u and rel%closed(u)
              implies t subseteq u)))"
    (theory three-place-predicate-theory)
    (proof
      (
        (unfold-single-defined-constant (0) rel%closure)
        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)")
          (contrapose "with(t,f:sets[ind_1],f=t);")
          (apply-macete-with-minor-premises eliminate-iota-macete)
          (contrapose "with(p:prop,not(p));"))
        (block 
          (script-comment "`direct-and-antecedent-inference-strategy' at (0 0 2 0 0 0)")
          (contrapose "with(t,f:sets[ind_1],f=t);")
          (apply-macete-with-minor-premises eliminate-iota-macete)
          (contrapose "with(p:prop,forsome(x:ind_1,p));")
          (antecedent-inference "with(p:prop,p and p);")
          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
          simplify
          (block 
            (script-comment "`direct-and-antecedent-inference-strategy' at (1 0 0 0 0)")
            (apply-macete-with-minor-premises tr%subseteq-antisymmetry)
            direct-and-antecedent-inference-strategy
            simplify
            simplify)))))
    

(def-constant span 
    "lambda(s:sets[ind_1],indic{y:ind_1, y in s or forsome(a,b:ind_1, a in s 
      and b in s and rel(a,b,y))})"
    (theory three-place-predicate-theory)
    )

(def-translation iterate->three-place-predicate 
    force-under-quick-load
    (source generic-theory-1)
    (target three-place-predicate-theory)
    (fixed-theories h-o-real-arithmetic)
    (sort-pairs (ind_1 "sets[ind_1]")))

(def-transported-symbols iterate
    (renamer iterate-renamer)
    (translation iterate->three-place-predicate))

(def-overloading iterate
    (generic-theory-1 iterate) (three-place-predicate-theory span%iterate))

(def-theorem span-definedness 
    "total_q{span,[sets[ind_1],sets[ind_1]]}"
    (theory three-place-predicate-theory)
    (usages d-r-convergence)  
    (proof
      (
        
        (unfold-single-defined-constant-globally span)
        simplify
        insistent-direct-inference
        beta-reduce-repeatedly
        )))

(def-theorem span-includes-set 
    "forall(s:sets[ind_1], s subseteq span(s))"
    (theory three-place-predicate-theory)
    (proof
      (
        direct-and-antecedent-inference-strategy
        insistent-direct-inference
        direct-and-antecedent-inference-strategy
        (unfold-single-defined-constant-globally span)
        simplify
        )))

(def-theorem monotonicity-of-span 
    "forall(s,t:sets[ind_1], s subseteq t implies span(s) subseteq span(t))"
    (theory three-place-predicate-theory)
    (proof
      (
      
        direct-and-antecedent-inference-strategy
        (unfold-single-defined-constant-globally span)
        insistent-direct-inference
        simplify
        direct-and-antecedent-inference-strategy
        (simplify-antecedent "with(p:prop,not(p));")
        (block 
          (script-comment "`direct-and-antecedent-inference-strategy' at (0 0 1 0 0)")
          (instantiate-existential ("b" "a"))
          simplify
          simplify)
        )))

(def-theorem rel%closed-iff-fixed-under-span 
    "forall(s:sets[ind_1],rel%closed(s) iff span(s)=s)"
    (theory three-place-predicate-theory)
    (proof
      ( 
        (apply-macete-with-minor-premises tr%subseteq-antisymmetry)
        (apply-macete-with-minor-premises span-includes-set)
        unfold-defined-constants
        simplify-insistently
        direct-and-antecedent-inference-strategy
        (block 
          (script-comment "`direct-and-antecedent-inference-strategy'")
          (backchain "with(p:prop,forall(z:ind_1,p));")
          auto-instantiate-existential)
        (block 
          (script-comment "`direct-and-antecedent-inference-strategy'")
          (backchain "with(p:prop,forall(x:ind_1,p));")
          direct-and-antecedent-inference-strategy
          auto-instantiate-existential)
        )))

(def-theorem strong-monotonicity-of-iterate 
    "forall(s:sets[ind_1],n,m:zz, 0<=n and n<=m implies
                iterate(span,s)(n) subseteq iterate(span,s)(m))"
    (theory three-place-predicate-theory)
    (proof
      (
        (induction trivial-integer-inductor ("m"))
        simplify
        (block 
          (script-comment "`induction' at (0 0 0 0 0 0 0 1 0 0 0 0 0 0 0)")
          (apply-macete-with-minor-premises tr%subseteq-transitivity)
          (block 
            (script-comment "`apply-macete-with-minor-premises' at (0)")
            (antecedent-inference "with(p:prop,p implies p);")
            (instantiate-existential ("iterate(span,s)(t)"))
            (apply-macete-with-minor-premises span-includes-set)
            (apply-macete-with-minor-premises tr%iterate-definedness)
            simplify-insistently)
          (block 
            (script-comment "`apply-macete-with-minor-premises' at (1)")
            (apply-macete-with-minor-premises tr%iterate-definedness)
            simplify-insistently)
          (block 
            (script-comment "`apply-macete-with-minor-premises' at (2)")
            (apply-macete-with-minor-premises tr%iterate-definedness)
            simplify-insistently))
        )))

(def-constant union%of%iterates 
    "lambda(s:sets[ind_1],big_u{lambda(n:zz,iterate(span,s)(n))})"
    (theory three-place-predicate-theory))

(def-theorem span-invariance  
    "forall( s:sets[ind_1],  
                      (span(s) subseteq s)
                              iff 
                      forall(x,y,z:ind_1, x in s and y in s and 
                                                              rel(x,y,z) implies z in s))"
    (theory three-place-predicate-theory)
    (proof
      (
        
        direct-and-antecedent-inference-strategy
        (block 
          (script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0 0 0)")
          (incorporate-antecedent "with(s,f:sets[ind_1],f subseteq s);")
          (unfold-single-defined-constant (0) span)
          insistent-direct-inference
          (backchain "with(s,f:sets[ind_1],f subseteq s);")
          (apply-macete-with-minor-premises indicator-facts-macete)
          beta-reduce-repeatedly
          direct-and-antecedent-inference-strategy
          auto-instantiate-existential)
        (block 
          (script-comment "`direct-and-antecedent-inference-strategy' at (0 1)")
          (unfold-single-defined-constant (0) span)
          simplify-insistently
          direct-and-antecedent-inference-strategy
          (backchain "with(p:prop,forall(x,y,z:ind_1,p));")
          auto-instantiate-existential)
        )))

(def-theorem union%of%iterates-closed-under-span 
    "forall(s:sets[ind_1],span(union%of%iterates(s))=union%of%iterates(s))"
    (theory three-place-predicate-theory)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises tr%subseteq-antisymmetry)
        direct-and-antecedent-inference-strategy
        (move-to-sibling 1)
        (block 
          (script-comment "`direct-and-antecedent-inference-strategy' at (1)")
          (apply-macete-with-minor-premises span-includes-set)
          (unfold-single-defined-constant (0) union%of%iterates))
        (block 
          (script-comment "`direct-and-antecedent-inference-strategy' at (0)")
          (apply-macete-with-minor-premises span-invariance)
          (block 
            (script-comment "`apply-macete-with-minor-premises' at (0)")
            (unfold-single-defined-constant-globally union%of%iterates)
            (apply-macete-with-minor-premises tr%big-union-member)
            beta-reduce-repeatedly
            direct-and-antecedent-inference-strategy
            (cut-with-single-formula "0<=i and 0<=i_$0")
            (move-to-sibling 1)
            (block 
              (script-comment "`cut-with-single-formula' at (1)")
              (cut-with-single-formula "#(iterate(span,s)(i)) and #( iterate(span,s)(i_$0))")
              (block 
	(script-comment "`cut-with-single-formula' at (0)")
	(antecedent-inference "with(p:prop,p and p);")
	direct-and-antecedent-inference-strategy
	(block 
	  (script-comment "`direct-and-antecedent-inference-strategy' at (0)")
	  (contrapose "with(i:zz,s:sets[ind_1],#(iterate(span,s)(i)));")
	  (apply-macete-with-minor-premises tr%undefined-for-negative)
	  simplify)
	(block 
	  (script-comment "`direct-and-antecedent-inference-strategy' at (1)")
	  (contrapose "with(i_$0:zz,s:sets[ind_1],#(iterate(span,s)(i_$0)));")
	  (apply-macete-with-minor-premises tr%undefined-for-negative)
	  simplify))
              simplify)
            (block 
              (script-comment "`cut-with-single-formula' at (0)")
              (cut-with-single-formula "0<=max(i,i_$0)")
              (move-to-sibling 1)
              simplify
              (block 
	(script-comment "`cut-with-single-formula' at (0)")
	(instantiate-existential ("1+max(i,i_$0)"))
	(unfold-single-defined-constant (0) span%iterate)
	simplify
	(unfold-single-defined-constant (0) span)
	simplify
	beta-reduce-with-minor-premises
	(block 
	  (script-comment "`beta-reduce-with-minor-premises' at (0)")
	  (apply-macete-with-minor-premises indicator-facts-macete)
	  beta-reduce
	  direct-and-antecedent-inference-strategy
	  auto-instantiate-existential
	  (block 
	    (script-comment "`auto-instantiate-existential' at (0 0)")
	    (cut-with-single-formula "iterate(span,s)(i_$0) subseteq iterate(span,s)(max(i,i_$0))")
	    (block 
	      (script-comment "`cut-with-single-formula' at (0)")
	      (cut-with-single-formula "i_$0<=max(i,i_$0)")
	      (move-to-sibling 1)
	      simplify
	      (backchain "with(f:sets[ind_1],f subseteq f);"))
	    (block 
	      (script-comment "`cut-with-single-formula' at (1)")
	      (apply-macete-with-minor-premises strong-monotonicity-of-iterate)
	      simplify))
	  (block 
	    (script-comment "`auto-instantiate-existential' at (0 1)")
	    (cut-with-single-formula "iterate(span,s)(i) subseteq iterate(span,s)(max(i,i_$0))")
	    (block 
	      (script-comment "`cut-with-single-formula' at (0)")
	      (cut-with-single-formula "i<=max(i,i_$0)")
	      (move-to-sibling 1)
	      simplify
	      (backchain "with(f:sets[ind_1],f subseteq f);"))
	    (block 
	      (script-comment "`cut-with-single-formula' at (1)")
	      (apply-macete-with-minor-premises strong-monotonicity-of-iterate)
	      simplify)))
	(block 
	  (script-comment "`beta-reduce-with-minor-premises' at (1)")
	  (apply-macete-with-minor-premises tr%iterate-definedness)
	  simplify-insistently))))
          (unfold-single-defined-constant (0) union%of%iterates))
        )))

(def-theorem union%of%iterates-includes-s 
    "forall(s:sets[ind_1],s subseteq union%of%iterates(s))"
    (theory three-place-predicate-theory)
    (proof
      (
        unfold-defined-constants
        insistent-direct-inference-strategy
        (apply-macete-with-minor-premises tr%big-union-member)
        (instantiate-existential ("0"))
        beta-reduce-insistently
        (unfold-single-defined-constant (0) span%iterate)
        )))

(def-theorem union%of%iterates-is-rel%closure 
    "forall(s:sets[ind_1],rel%closure(s)=union%of%iterates(s))"
    (theory three-place-predicate-theory)
    (proof
      (
        (apply-macete-with-minor-premises iota-free-characterization-of-rel%closure)
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises union%of%iterates-includes-s)
        (block 
          (script-comment "`direct-and-antecedent-inference-strategy' at (0 1)")
          (apply-macete-with-minor-premises rel%closed-iff-fixed-under-span)
          (apply-macete-with-minor-premises union%of%iterates-closed-under-span)
          simplify
          (unfold-single-defined-constant (0) union%of%iterates))
        (block 
          (script-comment "`direct-and-antecedent-inference-strategy'")
          (unfold-single-defined-constant (0) union%of%iterates)
          insistent-direct-inference
          (apply-macete-with-minor-premises tr%big-union-member)
          beta-reduce
          direct-and-antecedent-inference-strategy
          (cut-with-single-formula "forall(i:zz,0<=i implies iterate(span,s)(i) subseteq u)")
          (block 
            (script-comment "`cut-with-single-formula' at (0)")
            (cut-with-single-formula "0<=i")
            (block 
              (script-comment "`cut-with-single-formula' at (0)")
            (backchain "with(p:prop,forall(i:zz,p));")
              auto-instantiate-existential)
            (block 
              (script-comment "`cut-with-single-formula' at (1)")
              (cut-with-single-formula "#(iterate(span,s)(i))")
              (contrapose "with(f:sets[ind_1],#(f));")
              (apply-macete-with-minor-premises tr%undefined-for-negative)
              simplify))
          (block 
            (script-comment "`cut-with-single-formula' at (1)")
            (induction trivial-integer-inductor ("i"))
            (block 
              (script-comment "`induction' at (0 0)")
              beta-reduce
              (unfold-single-defined-constant (0) span%iterate))
            (block 
              (script-comment "`induction' at (0 1 0 0 0 0 0 0)")
              (incorporate-antecedent "with(u:sets[ind_1],rel%closed(u));")
              (apply-macete-with-minor-premises rel%closed-iff-fixed-under-span)
              direct-and-antecedent-inference-strategy
              (backchain-backwards "with(u,f:sets[ind_1],f=u);")
              (apply-macete-with-minor-premises monotonicity-of-span)
              (apply-macete-with-minor-premises tr%iterate-definedness)
              simplify-insistently)))
        )))

(def-theorem rel%closure-exists 
    "forall(s:sets[ind_1],#(rel%closure(s)))"
    (theory three-place-predicate-theory)
    (usages transportable-macete)
    (proof
      (
        insistent-direct-inference
        (apply-macete-with-minor-premises union%of%iterates-is-rel%closure)
        (unfold-single-defined-constant (0) union%of%iterates)
        )))