matita/matita/contribs/lambdadelta/ground/etc/relocation/tr.etc

   1 lemma pippo (f):
   2       f@❨𝟏❩⨮⇂f = f.
   3 * #p #f //
   4 qed.
   5
   6 corec lemma tr_compose_id_dx (f):
   7             f ≗ f∘𝐢.
   8 cases tr_id_unfold
   9 cases tr_compose_unfold
  10 cases (pippo f) in ⊢ (??%?);
  11 @stream_eq_cons /2 width=1 by/
  12 qed.
  13
  14 axiom pippo2 (f) (p):
  15       f@❨p❩ + (⇂*[ninj p]f)@❨𝟏❩ = f@❨↑p❩.
  16
  17 lemma tr_uni_tl (n):
  18       (𝐢) = ⇂𝐮❨n❩.
  19 // qed.
  20
  21 axiom tr_uni_tls_pos (p:pnat) (n):
  22       (𝐢) = ⇂*[p]𝐮❨n❩.
  23 (*
  24 #p #n
  25 >nsucc_pnpred <stream_tls_swap
  26 <tr_uni_tl <tr_id_tls
  27 // qed.
  28 *)
  29