628 " isolate_bdvs False)) @@ " ^ |
628 " isolate_bdvs False)) @@ " ^ |
629 " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ |
629 " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ |
630 " simplify_System_parenthesized False)) @@ " ^ |
630 " simplify_System_parenthesized False)) @@ " ^ |
631 " (Try (Rewrite_Set order_system False))) es_ " ^ |
631 " (Try (Rewrite_Set order_system False))) es_ " ^ |
632 " in (SubProblem (EqSystem_,[linear,system],[no_met]) " ^ |
632 " in (SubProblem (EqSystem_,[linear,system],[no_met]) " ^ |
633 " [bool_list_ es__, real_list_ vs_]))" |
633 " [BOOL_LIST es__, REAL_LIST vs_]))" |
634 )); |
634 )); |
635 |
635 |
636 (*this is for nth_ only*) |
636 (*this is for nth_ only*) |
637 val srls = Rls {id="srls_normalize_4x4", |
637 val srls = Rls {id="srls_normalize_4x4", |
638 preconds = [], |
638 preconds = [], |
674 " (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), " ^ |
674 " (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), " ^ |
675 " (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] " ^ |
675 " (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] " ^ |
676 " simplify_System_parenthesized False)) @@ " ^ |
676 " simplify_System_parenthesized False)) @@ " ^ |
677 " (Try (Rewrite_Set order_system False))) es_ " ^ |
677 " (Try (Rewrite_Set order_system False))) es_ " ^ |
678 " in (SubProblem (EqSystem_,[linear,system],[no_met]) " ^ |
678 " in (SubProblem (EqSystem_,[linear,system],[no_met]) " ^ |
679 " [bool_list_ es__, real_list_ vs_]))" |
679 " [BOOL_LIST es__, REAL_LIST vs_]))" |
680 )); |
680 )); |
681 store_met |
681 store_met |
682 (prep_met thy "met_eqsys_topdown_4x4" [] e_metID |
682 (prep_met thy "met_eqsys_topdown_4x4" [] e_metID |
683 (["EqSystem","top_down_substitution","4x4"], |
683 (["EqSystem","top_down_substitution","4x4"], |
684 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
684 [("#Given" ,["equalities es_", "solveForVars vs_"]), |