(* RELOCATION MAP ***********************************************************)
inductive fcla: relation2 rtmap nat ≝
(* RELOCATION MAP ***********************************************************)
inductive fcla: relation2 rtmap nat ≝
| fcla_push: ∀f,n. fcla f n → fcla (⫯f) n
| fcla_next: ∀f,n. fcla f n → fcla (↑f) (↑n)
.
| fcla_push: ∀f,n. fcla f n → fcla (⫯f) n
| fcla_next: ∀f,n. fcla f n → fcla (↑f) (↑n)
.
#g #m * -g -m /3 width=3 by fcla_isid, isid_inv_push/
#g #m #_ #f #H elim (discr_push_next … H)
qed-.
#g #m * -g -m /3 width=3 by fcla_isid, isid_inv_push/
#g #m #_ #f #H elim (discr_push_next … H)
qed-.
-lemma fcla_inv_nx: â\88\80g,m. ð\9d\90\82â¦\83gâ¦\84 ≘ m → ∀f. ↑f = g →
- â\88\83â\88\83n. ð\9d\90\82â¦\83fâ¦\84 ≘ n & ↑n = m.
+lemma fcla_inv_nx: â\88\80g,m. ð\9d\90\82â\9dªgâ\9d« ≘ m → ∀f. ↑f = g →
+ â\88\83â\88\83n. ð\9d\90\82â\9dªfâ\9d« ≘ n & ↑n = m.
#g #m * -g -m /2 width=3 by ex2_intro/
[ #g #Hg #f #H elim (isid_inv_next … H) -H //
| #g #m #_ #f #H elim (discr_next_push … H)
#g #m * -g -m /2 width=3 by ex2_intro/
[ #g #Hg #f #H elim (isid_inv_next … H) -H //
| #g #m #_ #f #H elim (discr_next_push … H)
-lemma cla_inv_nn: â\88\80g,m. ð\9d\90\82â¦\83gâ¦\84 â\89\98 m â\86\92 â\88\80f,n. â\86\91f = g â\86\92 â\86\91n = m â\86\92 ð\9d\90\82â¦\83fâ¦\84 ≘ n.
+lemma cla_inv_nn: â\88\80g,m. ð\9d\90\82â\9dªgâ\9d« â\89\98 m â\86\92 â\88\80f,n. â\86\91f = g â\86\92 â\86\91n = m â\86\92 ð\9d\90\82â\9dªfâ\9d« ≘ n.
#f #n #H elim H -f -n /3 width=3 by isid_inv_push/
#f #n #_ #_ #H elim (isid_inv_next … H) -H //
qed-.
(* Main forward lemmas ******************************************************)
#f #n #H elim H -f -n /3 width=3 by isid_inv_push/
#f #n #_ #_ #H elim (isid_inv_next … H) -H //
qed-.
(* Main forward lemmas ******************************************************)
#n #f1 #H elim H -f1 -n /3 width=3 by fcla_isid, isid_eq_repl_back/
#f1 #n #_ #IH #g2 #H [ elim (eq_inv_px … H) | elim (eq_inv_nx … H) ] -H
/3 width=3 by fcla_push, fcla_next/
qed-.
#n #f1 #H elim H -f1 -n /3 width=3 by fcla_isid, isid_eq_repl_back/
#f1 #n #_ #IH #g2 #H [ elim (eq_inv_px … H) | elim (eq_inv_nx … H) ] -H
/3 width=3 by fcla_push, fcla_next/
qed-.