Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FSet.thy
changeset 376 e99c0334d8bf
parent 375 f7dee6e808eb
child 379 57bde65f6eb2
equal deleted inserted replaced
375:f7dee6e808eb 376:e99c0334d8bf 
   335 lemma "\<forall>f g z a x. FOLD f g (z::'b) (INSERT a x) =
 
   335 lemma "\<forall>f g z a x. FOLD f g (z::'b) (INSERT a x) =
 
   336   (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"
 
   336   (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"
 
   337 apply (tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 
   337 apply (tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 
   338 done
 
   338 done
 
   339 
   339 
   340 ML {*
 
       
   341 
       
   342 fun lambda_prs_conv ctxt quot ctrm =
 
       
   343   case (Thm.term_of ctrm) of
 
       
   344     (Const (@{const_name "fun_map"}, _) $ y $ z) $ (Abs (_, T, x)) =>
 
       
   345       let
 
       
   346         val _ = tracing "AAA";
 
       
   347         val lty = T;
 
       
   348         val rty = fastype_of x;
 
       
   349         val thy = ProofContext.theory_of ctxt;
 
       
   350         val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
 
       
   351         val inst = [SOME lcty, NONE, SOME rcty];
 
       
   352         val lpi = Drule.instantiate' inst [] @{thm LAMBDA_PRS};
 
       
   353         val tac =
 
       
   354           (compose_tac (false, lpi, 2)) THEN_ALL_NEW
 
       
   355           (quotient_tac quot);
 
       
   356         val gc = Drule.strip_imp_concl (cprop_of lpi);
 
       
   357         val t = Goal.prove_internal [] gc (fn _ => tac 1)
 
       
   358         val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t
 
       
   359         val te = @{thm eq_reflection} OF [ts]
 
       
   360         val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm));
 
       
   361         val _ = tracing (Syntax.string_of_term @{context} (term_of (Thm.lhs_of te)));
 
       
   362         val insts = matching_prs (ProofContext.theory_of ctxt) (term_of ctrm) (term_of (Thm.lhs_of te));
 
       
   363         val ti = Drule.instantiate insts te;
 
       
   364         val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti)));
 
       
   365       in
 
       
   366         Conv.rewr_conv (eq_reflection OF [ti]) ctrm
 
       
   367       end
 
       
   368   | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm
 
       
   369   | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm
 
       
   370   | _ => Conv.all_conv ctrm
 
       
   371 *}
 
       
   372 
       
   373 ML {*
 
       
   374 fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) =>
 
       
   375   CONVERSION
 
       
   376     (Conv.params_conv ~1 (fn ctxt =>
 
       
   377        (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv
 
       
   378           Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)
 
       
   379 *}
 
       
   380 
       
   381 ML {*
 
       
   382 val ctrm = @{cterm "((ABS_fset ---> id) ---> id) (\<lambda>x. id ((REP_fset ---> id) x))"}
 
       
   383 val pat =  @{cpat  "((ABS_fset ---> id) ---> id) (\<lambda>x. ?f ((REP_fset ---> id) x))"}
 
       
   384 *}
 
       
   385 
       
   386 ML {* matching_prs @{theory} (term_of pat) (term_of ctrm); *}
 
       
   387 
       
   388 ML {*
 
       
   389   lambda_prs_conv @{context} quot ctrm
 
       
   390 *}
 
       
   391 
       
   392 
       
   393 ML {* 
       
   394 val t = @{thm LAMBDA_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT] IDENTITY_QUOTIENT]}
 
       
   395 val te = @{thm eq_reflection} OF [t]
 
       
   396 val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] te
 
       
   397 val tl = Thm.lhs_of ts
 
       
   398  *}
 
       
   399 
       
   400 ML {* val inst = matching_prs @{theory} (term_of tl) (term_of ctrm); *}
 
       
   401 
       
   402 ML {* val trm = @{cterm "(((ABS_fset ---> id) ---> id) (\<lambda>(P\<Colon>('a list \<Rightarrow> bool)).
 
       
   403               All ((REP_fset ---> id) (\<lambda>(list\<Colon>('a list)).
 
       
   404                         (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset [])) \<longrightarrow>
 
       
   405                True \<longrightarrow> (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset list))))))"} *}
 
       
   406 
       
   407 ML {*
 
       
   408   lambda_prs_conv @{context} quot trm
 
       
   409 *}
 
       
   410 
       
   411 
       
   412 
       
   413 (*ML {* val trm = @{cterm "(((ABS_fset ---> id) ---> id) (\<lambda>(?P\<Colon>('a list \<Rightarrow> bool)). (g (id P)"} *} *)
 
       
   414 
       
   415 
       
   416 
       
   417 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 
       
   418 apply(tactic {* procedure_tac @{thm list.induct} @{context} 1 *})
 
       
   419 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
 
       
   420 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})
 
       
   421 apply(tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
 
       
   422 apply(tactic {* lambda_prs_tac @{context} quot 1 *})
 
       
   423 
       
   424 
       
   425 ML_prf {* Subgoal.focus @{context} 1 (#goal (Isar.goal ())) *}
 
       
   426 
       
   427 apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *})
 
       
   428 
       
   429 
       
   430 thm LAMBDA_PRS
 
       
   431 apply(tactic {* EqSubst.eqsubst_tac @{context} [0] @{thms LAMBDA_PRS} 1 *})
 
       
   432 
       
   433 apply(tactic {*  (lambda_prs_tac @{context} quot) 1 *})
 
       
   434 
       
   435 apply(tactic {* REPEAT_ALL_NEW (lambda_prs_tac @{context} quot) 1 *})
 
       
   436 
       
   437 apply(tactic {* clean_tac @{context} quot defs reps_same 1 *})
 
       
   438 apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *})
 
       
   439 ML {* lift_thm_fset @{context} @{thm list.induct} *}
 
       
   440 ML {* lift_thm_g_fset @{context} @{thm list.induct} @{term "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"} *}
 
       
   441 
       
   442 
       
   443 
       
   444 
       
   445 thm map_append
 
       
   446 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
 
   340 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
 
   447 apply(tactic {* procedure_tac @{thm map_append} @{context} 1 *})
 
       
   448 apply(tactic {* prepare_tac 1 *})
 
       
   449 thm map_append
 
       
   450 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
 
   341 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
 
   451 done
 
   342 done
 
   452 
       
   453 
       
   454 
   343 
   455 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"
 
   344 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"
 
   456 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})
 
   345 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})
 
   457 done
 
   346 done
 
   458 
   347 
   459 ML {* atomize_thm @{thm fold1.simps(2)} *}
 
   348 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *}
 
   460 (*ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} @{term "FOLD f g (z::'b) (INSERT a x) =
 
   349 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
 
   461     (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"} *}*)
 
   350 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 
   462 
   351 apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *})
 
   463 
   352 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *})
 
   464 *)
 
   353 apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
 
   465 ML {* lift_thm_g_fset @{context} @{thm map_append} @{term "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"} *}
 
   354 done
 
   466 
       
   467 
       
   468 ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "\<forall>x xa a. x = xa \<Longrightarrow> INSERT a x = INSERT a xa"}) *}
 
       
   469 
       
   470 
       
   471 ML {* lift_thm_fset @{context} @{thm map_append} *}
 
       
   472 
       
   473 
       
   474 (*
 
       
   475 apply(tactic {* procedure_tac @{thm m1} @{context} 1 *})
 
       
   476 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
 
       
   477 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})
 
       
   478 apply(tactic {* clean_tac @{context} quot defs reps_same 1 *})
 
       
   479 apply(tactic {* TRY' (REPEAT_ALL_NEW (allex_prs_tac @{context} quot)) 1 *})
 
       
   480 apply(tactic {* TRY' (REPEAT_ALL_NEW (lambda_prs_tac @{context} quot)) 1 *})
 
       
   481 ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *}
 
       
   482 apply(tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1*})
 
       
   483 apply(tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
 
       
   484 *)
 
       
   485 
       
   486 
       
   487 
       
   488 (*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*)
 
       
   489 
   355 
   490 quotient_def
 
   356 quotient_def
 
   491   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 
   357   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 
   492 where
 
   358 where
 
   493   "fset_rec \<equiv> list_rec"
 
   359   "fset_rec \<equiv> list_rec"
 
   508 lemma list_case_rsp:
 
   374 lemma list_case_rsp:
 
   509   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
 
   375   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
 
   510   apply (auto simp add: FUN_REL_EQ)
 
   376   apply (auto simp add: FUN_REL_EQ)
 
   511   sorry
 
   377   sorry
 
   512 
   378 
   513 
       
   514 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
 
   379 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
 
   515 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *}
 
   380 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *}
 
   516 
   381 
   517 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *}
 
   382 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *}
 
   518 ML {* fun lift_thm_g_fset lthy t g = lift_thm_goal lthy qty "fset" rsp_thms defs t g *}
 
   383 ML {* fun lift_thm_g_fset lthy t g = lift_thm_goal lthy qty "fset" rsp_thms defs t g *}
 
   519 
   384 ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *}
 
   520 thm list.recs(2)
 
   385 
   521 ML {* lift_thm_fset @{context} @{thm list.recs(2)} *}
 
   386 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.recs(2)})) *}
 
   522 ML {* lift_thm_g_fset @{context} @{thm list.recs(2)} @{term "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"} *}
 
   387 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
 
   523 
   388 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
 
   524 
   389 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})
 
   525 ML {* val gl = @{term "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"} *}
 
   390 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *})
 
   526 ML {* val t_a = atomize_thm @{thm list.recs(2)} *}
 
   391 apply (tactic {* (simp_tac (HOL_ss addsimps
 
   527 ML {* val qtrm = atomize_goal @{theory} gl *}
 
   392   @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id})) 1 *})
 
   528 ML {* val rg = cterm_of @{theory}(Syntax.check_term @{context} (REGULARIZE_trm @{context} (prop_of t_a) qtrm)) *}
 
   393 ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *}
 
   529 ML {* val rg2 = cterm_of @{theory}(my_reg @{context} rel rty (prop_of t_a)) *}
 
   394 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *})
 
   530 
   395 apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
 
   531 ML {* val t_r = regularize_goal @{context} t_a rel_eqv rel_refl qtrm *}
 
   396 done
 
   532 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
 
   397 
   533 
   398 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.cases(2)})) *}
 
   534 ML {* val rg = cterm_of @{theory}(Syntax.check_term @{context} (inj_REPABS @{context} ((prop_of t_r), qtrm))) *}
 
   399 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
 
   535 ML {* val rg2 = cterm_of @{theory} (build_repabs_term @{context} t_r consts rty qty) *}
 
   400 
   536 ML {* val t_t = repabs_goal @{context} t_r rty quot rel_refl trans2 rsp_thms qtrm *}
 
   401 
   537 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
 
   402 ML {* map (lift_thm_fset @{context}) @{thms list.cases(2)} *}
 
   538 ML {*
 
   403 lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa"
 
   539   val lthy = @{context}
 
   404 apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *})
 
   540   val (alls, exs) = findallex lthy rty qty (prop_of t_a);
 
   405 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *})
 
   541   val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls
 
   406 apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
 
   542   val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs
 
   407 done
 
   543   val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t
 
       
   544   val abs = findabs rty (prop_of t_a);
 
       
   545   val aps = findaps rty (prop_of t_a);
 
       
   546   val app_prs_thms = map (applic_prs lthy rty qty absrep) aps;
 
       
   547   val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;
 
       
   548   val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;
 
       
   549   val defs_sym = flat (map (add_lower_defs lthy) defs);
 
       
   550   val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;
 
       
   551   val t_id = simp_ids lthy t_l;
 
       
   552   val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id;
 
       
   553   val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;
 
       
   554   val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
 
       
   555   val t_rv = ObjectLogic.rulify t_r
 
       
   556 
       
   557 *}
 
       
   558 
       
   559 
       
   560 
       
   561 
       
   562 
       
   563 
       
   564 ML {* map (lift_thm_fset @{context}) @{thms list.cases} *}
 
       
   565 
       
   566 
       
   567 
       
   568 
       
   569 ML {* atomize_thm @{thm m1} *}
 
       
   570 ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "IN x EMPTY = False"}) *}
 
       
   571 ML {* lift_thm_fset @{context} @{thm m1} *}
 
       
   572 (* ML {* lift_thm_g_fset @{context} @{thm m1} @{term "IN x EMPTY = False"}) *} *)
 
       
   573 
       
   574 
   408 
   575 lemma list_induct_part:
 
   409 lemma list_induct_part:
 
   576   assumes a: "P (x :: 'a list) ([] :: 'a list)"
 
   410   assumes a: "P (x :: 'a list) ([] :: 'a list)"
 
   577   assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)"
 
   411   assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)"
 
   578   shows "P x l"
 
   412   shows "P x l"
 
   581   apply (rule b)
 
   415   apply (rule b)
 
   582   apply (assumption)
 
   416   apply (assumption)
 
   583   done
 
   417   done
 
   584 
   418 
   585 
   419 
       
   420 
   586 (* Construction site starts here *)
 
   421 (* Construction site starts here *)
 
   587 
   422 
   588 
   423 
   589 ML {* val consts = lookup_quot_consts defs *}
 
   424 ML {* val consts = lookup_quot_consts defs *}
 
   590 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 
   425 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 
   591 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *}
 
   426 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *}
 
   592 
   427 
   593 thm list.recs(2)
 
       
   594 ML {* val t_a = atomize_thm @{thm list_induct_part} *}
 
   428 ML {* val t_a = atomize_thm @{thm list_induct_part} *}
 
   595 
   429 
   596 
   430 
   597 (* prove {* build_regularize_goal t_a rty rel @{context}  *}
 
   431 (* prove {* build_regularize_goal t_a rty rel @{context}  *}
 
   598  ML_prf {*  fun tac ctxt = FIRST' [
 
   432  ML_prf {*  fun tac ctxt = FIRST' [
 
   752 ML {* val t_l = repeat_eqsubst_thm @{context} (lam_prs_thms) t_t *}
 
   586 ML {* val t_l = repeat_eqsubst_thm @{context} (lam_prs_thms) t_t *}
 
   753 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_l *}
 
   587 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_l *}
 
   754 ML {* val t_al = MetaSimplifier.rewrite_rule (allthms) t_d *}
 
   588 ML {* val t_al = MetaSimplifier.rewrite_rule (allthms) t_d *}
 
   755 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_al *}
 
   589 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_al *}
 
   756 
   590 
   757 
       
   758 ML {*
 
       
   759   fun lift_thm_fset_note name thm lthy =
 
       
   760     let
 
       
   761       val lifted_thm = lift_thm_fset lthy thm;
 
       
   762       val (_, lthy2) = note (name, lifted_thm) lthy;
 
       
   763     in
 
       
   764       lthy2
 
       
   765     end;
 
       
   766 *}
 
       
   767 
       
   768 local_setup {*
 
       
   769   lift_thm_fset_note @{binding "m1l"} @{thm m1} #>
 
       
   770   lift_thm_fset_note @{binding "m2l"} @{thm m2} #>
 
       
   771   lift_thm_fset_note @{binding "leqi4l"} @{thm list_eq.intros(4)} #>
 
       
   772   lift_thm_fset_note @{binding "leqi5l"} @{thm list_eq.intros(5)}
 
       
   773 *}
 
       
   774 thm m1l
 
       
   775 thm m2l
 
       
   776 thm leqi4l
 
       
   777 thm leqi5l
 
       
   778 
       
   779 end
 
   591 end
nominal2