(* RELOCATION MAP ***********************************************************)
inductive fcla: relation2 rtmap nat ā
-| fcla_isid: āf. šāŖfā« ā fcla f 0
+| fcla_isid: āf. šāŖfā« ā fcla f (š)
| fcla_push: āf,n. fcla f n ā fcla (ā«Æf) n
| fcla_next: āf,n. fcla f n ā fcla (āf) (ān)
.
lemma cla_inv_nn: āg,m. šāŖgā« ā m ā āf,n. āf = g ā ān = m ā šāŖfā« ā n.
#g #m #H #f #n #H1 #H2 elim (fcla_inv_nx ā¦ H ā¦ H1) -g
-#x #Hf #H destruct //
+#x #Hf #H destruct <(eq_inv_nsucc_bi ā¦ H) -n //
qed-.
-lemma cla_inv_np: āg,m. šāŖgā« ā m ā āf. āf = g ā 0 = m ā ā„.
+lemma cla_inv_np: āg,m. šāŖgā« ā m ā āf. āf = g ā š = m ā ā„.
#g #m #H #f #H1 elim (fcla_inv_nx ā¦ H ā¦ H1) -g
-#x #_ #H1 #H2 destruct
+#x #_ #H1 #H2 destruct /2 width=2 by eq_inv_zero_nsucc/
qed-.
-lemma fcla_inv_xp: āg,m. šāŖgā« ā m ā 0 = m ā šāŖgā«.
+lemma fcla_inv_xp: āg,m. šāŖgā« ā m ā š = m ā šāŖgā«.
#g #m #H elim H -g -m /3 width=3 by isid_push/
-#g #m #_ #_ #H destruct
+#g #m #_ #_ #H destruct elim (eq_inv_zero_nsucc ā¦ H)
qed-.
-lemma fcla_inv_isid: āf,n. šāŖfā« ā n ā šāŖfā« ā 0 = n.
+lemma fcla_inv_isid: āf,n. šāŖfā« ā n ā šāŖfā« ā š = 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-.
[ /2 width=3 by fcla_inv_isid/
| /3 width=3 by fcla_inv_px/
| #f #n1 #_ #IH #n2 #H elim (fcla_inv_nx ā¦ H) -H [2,3 : // ]
- #g #Hf #H destruct /3 width=1 by eq_f/
+ #g #Hf #H destruct >IH //
]
qed-.