(def-language bird-language
    (base-types elem value))

(def-theory bird 
    (language bird-language)
    (component-theories h-o-real-arithmetic))

(def-translation seq->bird 
    (source sequences)
    (target bird)
    (fixed-theories h-o-real-arithmetic)
    (sort-pairs (ind_1 elem))
    (theory-interpretation-check using-simplification))

(def-constant map 
    "lambda(f:[elem_0,elem_1], lambda(s:[nn,elem_0], lambda(m:nn, f(s(m)))))"
    (theory bird-2-tuples))
    

(def-theorem map-means-compose 
    "forall(f:[elem_0,elem_1], s:[nn,elem_0], map(f)(s)=f oo s)"
    (theory bird-2-tuples)
    (usages transportable-macete)
    )

(def-theorem domain-of-total-map 
    "forall(f:[elem_0,elem_1], s:[nn,elem_0], total_q{f,[elem_0,elem_1]} implies
dom{map(f)(s)}=dom{s})"
    (theory bird-2-tuples)
    (usages transportable-macete)
    )

(def-theorem map-f-is-total 
    "forall(y:[nn,elem_0],f:[elem_0,elem_1], #(map(f)(y)))"
    (theory bird-2-tuples)
    (usages rewrite transportable-rewrite)
    )
    

(def-theorem domain-of-almost-total-map 
    "forall(f:[elem_0,elem_1], s:[nn,elem_0], 
                forall(x:elem_0, x in ran{s} implies #(f(x)))
              implies
	dom{map(f)(s)}=dom{s})"
    (theory bird-2-tuples)
    (usages transportable-macete)
    (proof "$theories/bird/proofs/domain-of-almost-total-map.t"))

(def-theorem map-through-nil 
    "forall(f:[elem_0,elem_1], map(f)(nil{elem_0})=nil{elem_1})"
    (theory bird-2-tuples)
    (usages transportable-macete transportable-rewrite rewrite)
    )

(def-theorem map-totality 
    "total_q{map,[[elem_0,elem_1],[[nn,elem_0],[nn,elem_1]]]}"
    (theory bird-2-tuples)
    (usages d-r-convergence)
    )
  

(def-theorem map-cons 
    "forall(f:[elem_0,elem_1], s:[nn,elem_0], a:elem_0,
            map(f)(cons{a,s})=cons{f(a),map(f)(s)})"
    (theory bird-2-tuples)
    (usages rewrite transportable-rewrite)
  (proof "$theories/bird/proofs/map-cons.t"))

(def-inductor elem-sequence-inductor
    sequence-induction
    (theory bird)
    (translation seq->bird)
    (base-case-hook simplify))

(def-inductor elem_0-sequence-inductor
    sequence-induction-for-elem-sequence-inductor
    (theory bird-0)
    (translation bird-to-bird-0)
    (base-case-hook simplify))

(def-theorem map-append 
    "forall(f:[elem_0,elem_1],x,y:[nn,elem_0], 
            f_seq_q{x} and total_q{f,[elem_0,elem_1]}
          implies
            map(f)(append{x,y})=append{map(f)(x), map(f)(y)})"
    (theory bird-2-tuples)
    (usages transportable-macete)
    (proof  "$theories/bird/proofs/map-append.t"))

(def-theory-ensemble-instances
  bird
  (multiples 2)
  (target-multiple 3))
(theory-ensemble-install-overloadings-for-defined-constants bird-ensemble 3)

(def-theorem map-distributes-over-composition 
  "forall(f:[elem_0,elem_1], g:[elem_1,elem_2], map(g oo f) = (map(g)) oo (map(f)))"
  (theory bird-3-tuples)
  (usages transportable-macete)
  (proof "$theories/bird/proofs/map-comp-distributes.t"))

(def-theorem map-inverse 
  "forall(f:[elem_0,elem_1], injective_q{f} and surjective_q{f}
  implies inverse{map(inverse{f})} = map(f) )"
  (theory bird-3-tuples)
  (usages transportable-macete)
  (proof "$theories/bird/proofs/map-inverse.t"))

(def-theorem map-inverse-1 
    "forall(f:[elem_0,elem_1],  injective_q{f} and surjective_q{f}
  implies inverse{map(f)} = map(inverse{f}))"
    (theory bird-3-tuples)
    (usages transportable-macete)
    (proof "$theories/bird/proofs/map-inverse-1.t"))
(pop-current-syntax)
(pop-current-theory)