include "ground/arith/nat_succ.ma".
include "ground/relocation/gr_isi.ma".
-(* FINITE COLENGTH ASSIGNMENT FOR GENERIC RELOCATION MAPS ***********************************************************)
+(* FINITE COLENGTH ASSIGNMENT FOR GENERIC RELOCATION MAPS *******************)
(*** fcla *)
inductive gr_fcla: relation2 gr_map nat ā
"finite colength assignment (generic relocation maps)"
'RFunC f n = (gr_fcla f n).
-(* Basic inversion lemmas ***************************************************)
+(* Basic inversions *********************************************************)
(*** fcla_inv_px *)
lemma gr_fcla_inv_push (g) (m): šāŖgā« ā m ā āf. ā«Æf = g ā šāŖfā« ā m.
]
qed-.
-(* Advanced inversion lemmas ************************************************)
+(* Advanced inversions ******************************************************)
(*** cla_inv_nn *)
lemma gr_cla_inv_next_succ (g) (m): šāŖgā« ā m ā āf,n. āf = g ā ān = m ā šāŖfā« ā n.