761 quotient_definition

   762   "Vr5 :: name \<Rightarrow> trm5"

   763 as

   764   "rVr5"

   765 

   766 quotient_definition

   767   "Ap5 :: trm5 \<Rightarrow> trm5 \<Rightarrow> trm5"

   768 as

   769   "rAp5"

   770 

   771 quotient_definition

   772   "Lt5 :: lts \<Rightarrow> trm5 \<Rightarrow> trm5"

   773 as

   774   "rLt5"

   775 

   776 quotient_definition

   777   "Lnil :: lts"

   778 as

   779   "rLnil"

   780 

   781 quotient_definition

   782   "Lcons :: name \<Rightarrow> trm5 \<Rightarrow> lts \<Rightarrow> lts"

   783 as

   784   "rLcons"

   785 

   786 quotient_definition

   787    "fv_trm5 :: trm5 \<Rightarrow> atom set"

   788 as

   789   "rfv_trm5"

   790 

   791 quotient_definition

   792    "fv_ltr :: lts \<Rightarrow> atom set"

   793 as

   794   "rfv_lts"

   795