(* 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)
.
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
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
[ /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 : // ]
[ /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 : // ]