(* "Knowledge/biegelinie-4.sml"

   author: Walther Neuper 190515

   (c) due to copyright terms

*)

"table of contents ---------------------------------------------------------------------------";

"---------------------------------------------------------------------------------------------";

"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto TODO investigate failure ------";

"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me ---------------------------------";

"---------------------------------------------------------------------------------------------";

"---------------------------------------------------------------------------------------------";

"---------------------------------------------------------------------------------------------";

"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto TODO investigate failure ------";

"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto TODO investigate failure ------";

"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto TODO investigate failure ------";

(* the error in this test might be independent from introduction of y, dy

   as arguments in IntegrierenUndKonstanteBestimmen2,

   rather due to so far untested use of "auto" *)

val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",

	     "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",

	     "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",

       "AbleitungBiegelinie dy"];

val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],

		     ["IntegrierenUndKonstanteBestimmen2"]);

reset_states ();

CalcTree [(fmz, (dI',pI',mI'))];                                     

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

val ((pt, p),_) = get_calc 1;

if p = ([], Pbl) then () else error ""

get_obj I pt (fst p); (*TODO investigate failure*)

(* NOTE: ^^^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed ^^^^^^^^^^^^^^^^^ * )

(*[], Met*)autoCalculate 1 CompleteCalcHead;

(*[1], Pbl*)autoCalculate 1 (Step 1); (* into SubProblem *)

(*[1], Res*)autoCalculate 1 CompleteSubpbl; (**)

(*[2], Pbl*)autoCalculate 1 (Step 1); (* out of SubProblem *)

(*[2], Res*)autoCalculate 1 CompleteSubpbl;

(*[3], Pbl*)autoCalculate 1 (Step 1); (* out of SubProblem *)

(*[3], Met*)autoCalculate 1 CompleteCalcHead;

(*[3, 1], Frm*)autoCalculate 1 (Step 1); (* solve SubProblem *)

(*(**)autoCalculate 1 CompleteSubpbl;  error in kernel 4: generate1: not impl.for Empty_Tac_*)

(*[3, 1], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)

(*[3, 2], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)

(*[3, 3], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)

(*[3, 4], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)

(*[3, 5], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)

(*[3, 6], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)

(*[3, 7], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)

(*[3, 8], Pbl*)autoCalculate 1 (Step 1); (* solve SubProblem *)

(*[3, 8], Met*)autoCalculate 1 CompleteCalcHead;

(*[3, 8, 1], Frm*)autoCalculate 1 (Step 1); (* solve SubProblem *)

(*[3, 8, 1], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)

(*(**)autoCalculate 1 (Step 1); 

*** generate1: not impl.for Empty_Tac_ 

val it = <AUTOCALC><CALCID>1</CALCID><CALCMESSAGE>helpless</CALCMESSAGE></AUTOCALC>: XML.tree *)

val ((pt,_),_) = get_calc 1;

val ip = get_pos 1 1;

val (Form f, tac, asms) = pt_extract (pt, ip);

if ip = ([3, 8, 1], Res) andalso 

term2str f = "[-1 * c_4 / -1 = 0,\n (6 * c_4 * EI + 6 * L * c_3 * EI + -3 * L ^^^ 2 * c_2 + -1 * L ^^^ 3 * c) /\n (6 * EI) =\n L ^^^ 4 * q_0 / (-24 * EI),\n c_2 = 0, c_2 + L * c = L ^^^ 2 * q_0 / 2]"

then 

  case tac of

    SOME (Check_Postcond ["normalise", "4x4", "LINEAR", "system"]) => ()

  | _ => error "ERROR biegel.7.70 changed 1"

else error "ERROR biegel.7.70 changed 2";

( * NOTE: ^^^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed ^^^^^^^^^^^^^^^^^ *)

"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";

"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";

"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";

"----- Bsp 7.70 with me";

val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",

	     "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",

	     "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",

       "AbleitungBiegelinie dy"];

val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],

		     ["IntegrierenUndKonstanteBestimmen2"]);

val p = e_pos'; val c = [];

(*//----------------------------------vvv CalcTreeTEST ----------------------------------------\\*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*)

(*+*)val PblObj {probl, meth, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt (fst p);

(*+*)writeln (oris2str oris); (*[

(1, ["1"], #Given,Traegerlaenge, ["L"]),

(2, ["1"], #Given,Streckenlast, ["q_0"]),

(3, ["1"], #Find,Biegelinie, ["y"]),

(4, ["1"], #Relate,Randbedingungen, ["[y 0 = 0]","[y L = 0]","[M_b 0 = 0]","[M_b L = 0]"]),

(5, ["1"], #undef,FunktionsVariable, ["x"]),

(6, ["1"], #undef,GleichungsVariablen, ["[c]","[c_2]","[c_3]","[c_4]"]),

(7, ["1"], #undef,AbleitungBiegelinie, ["dy"])]*)

(*+*)itms2str_ @{context} probl = "[]";

(*+*)itms2str_ @{context} meth = "[]";

(*\\----------------------------------^^^ CalcTreeTEST ----------------------------------------//*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Traegerlaenge L"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Streckenlast q_0"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Biegelinie y"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["Biegelinien"]*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*)

(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)

(*----------- 10 -----------*)

(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)

(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "AbleitungBiegelinie dy*)

(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Apply_Method ["IntegrierenUndKonstanteBestimmen2"*)

(*//----------------------------------vvv Apply_Method ["IntegrierenUndKonstanteBestimmen2"----\\*)

(*[1], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt = Model_Problem*)

(*AMBIGUITY in creating the environment from formal args. of partial_function "Biegelinie.Biegelinie2Script"

and the actual args., ie. items of the guard of "["IntegrierenUndKonstanteBestimmen2"]" by "assoc_by_type":

formal arg. "b" type-matches with several...actual args. "["dy","y"]"

selected "dy"

with

formals: ["l","q","v","b","s","vs","id_abl"]

actuals: ["L","q_0","x","[c, c_2, c_3, c_4]","dy","y","[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]"]*)

"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, c, pt);

    val (pt''', p''') =

	    (*locatetac is here for testing by me; step would suffice in me*)

	    case locatetac tac (pt,p) of

		    ("ok", (_, _, ptp)) => ptp

;

(*+*)p    = ([], Met);

(*+*)p''' = ([1], Pbl);

(*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''' (fst p''');

(*+*)(*MISSING after locatetac:*)

(*+*)writeln (oris2str oris); (*[

(1, ["1"], #Given,Streckenlast, ["q_0"]),

(2, ["1"], #Given,FunktionsVariable, ["x"]),

(3, ["1"], #Find,Funktionen, ["funs'''"])]

MISSING:

                 Biegelinie

                 AbleitungBiegelinie

*)

"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));

      val (mI, m) = Solve.mk_tac'_ tac;

val Appl m = (*case*) Applicable.applicable_in p pt m (*of*);

(*if*) member op = Solve.specsteps mI = false; (*else*)

loc_solve_ (mI,m) ptp;

"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI,m), ptp);

Solve.solve m (pt, pos);

"~~~~~ fun solve , args:"; val (("Apply_Method", m as Tactic.Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p, _)))) =

  (m, (pt, pos));

val {srls, ...} = Specify.get_met mI;

      val itms = case get_obj I pt p of

        PblObj {meth=itms, ...} => itms

      | _ => error "solve Apply_Method: uncovered case get_obj"

      val thy' = get_obj g_domID pt p;

      val thy = Celem.assoc_thy thy';

      val srls = Lucin.get_simplifier (pt, pos)

      val (is, env, ctxt, sc) = case Lucin.init_pstate srls ctxt itms mI of

        (is as Istate.Pstate ist, ctxt, sc) =>  (is, get_env ist, ctxt, sc)

      | _ => error "solve Apply_Method: uncovered case init_pstate"

      val ini = Lucin.init_form thy sc env;

      val p = lev_dn p;

val NONE = (*case*) ini (*of*);

            val (m', (is', ctxt'), _) = determine_next_tactic sc (pt, (p, Res)) is ctxt;

	          val d = Rule.e_rls (*FIXME: get simplifier from domID*);

     val Safe_Step ((pt', p'), _, _, _) = (*case*) locate_input_tactic sc (pt,(p, Res)) is' ctxt' m' (*of*);

Safe_Step : state * Istate.T * Proof.context * Tactic.T -> input_tactic_result;

(*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt' (fst p');

(*+*)(*MISSING after locate_input_tactic:*)

(*+*)writeln (oris2str oris); (*[

(1, ["1"], #Given,Streckenlast, ["q_0"]),

(2, ["1"], #Given,FunktionsVariable, ["x"]),

(3, ["1"], #Find,Funktionen, ["funs'''"])]

MISSING:

                 Biegelinie

                 AbleitungBiegelinie

*)

"~~~~~ fun locate_input_tactic , args:"; val () = ();

(*+*)val c = [];

(*\\----------------------------------^^^ Apply_Method ["IntegrierenUndKonstanteBestimmen2"----//*)

(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Add_Given "Streckenlast q_0"*)

(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)

(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Funktionen funs'''"*)

(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*)

(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["vonBelastungZu", "Biegelinien"]*)

(*[1], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt = Specify_Method ["Biegelinien", "ausBelastung"]*)

(*----------- 20 -----------*)

(*//------------------------------------------------vvv Specify_Method ["Biegelinien", "ausBelastung"]-\\*)

(*[1], Pbl*)(*ERROR val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Apply_Method ["Biegelinien", "ausBelastung"]*)

ERROR itms2args: 'Biegelinie' not in itms*)

(*SubProblem (_, [''vonBelastungZu'', ''Biegelinien''], _)

    [REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl]

                     ^^^^^^^^^^^ ..ERROR itms2args: 'Biegelinie' not in itms*)

(*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''''' (fst p''''');

(*+*)if oris2str oris =

(*+*)  "[\n(1, [\"1\"], #Given,Streckenlast, [\"q_0\"]),\n(2, [\"1\"], #Given,FunktionsVariable, [\"x\"]),\n(3, [\"1\"], #Find,Funktionen, [\"funs'''\"])]"

(*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed oris";

writeln (oris2str oris); (*[

(1, ["1"], #Given,Streckenlast, ["q_0"]),

(2, ["1"], #Given,FunktionsVariable, ["x"]),

(3, ["1"], #Find,Funktionen, ["funs'''"])]*)

(*+*)if itms2str_ @{context} probl = "[\n(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),\n(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),\n(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))]"

(*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed probl";

writeln (itms2str_ @{context} probl); (*[

(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),

(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),

(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))]*)

(*+*)if itms2str_ @{context} meth = "[]"

(*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed meth";

writeln (itms2str_ @{context} meth); (*[]*)

"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt''''', p''''', c, pt''''');

(*  val (pt, p) = *)

	    (*locatetac is here for testing by me; step would suffice in me*)

	    case locatetac tac (pt,p) of

		    ("ok", (_, _, ptp)) => ptp

;

"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));

      val (mI, m) = Solve.mk_tac'_ tac;

val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);

(*if*) member op = Solve.specsteps mI = true; (*then*)

(*val Updated (_, _, (ctree, pos')) =*) loc_specify_ m ptp; (*creates meth-itms*)

"~~~~~ fun loc_specify_ , args:"; val (m, (pt, pos)) = (m, ptp);

(*    val (p, _, f, _, _, pt) =*) Chead.specify m pos [] pt;

"~~~~~ fun specify , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pos as (p, _)), _, pt) = (m, pos, [], pt);

        val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of

          PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>

             (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)

        val {ppc, pre, prls,...} = Specify.get_met mID

        val thy = Celem.assoc_thy dI

        val dI'' = if dI = Rule.e_domID then dI' else dI

        val pI'' = if pI = Celem.e_pblID then pI' else pI

;

(*+*)writeln (oris2str oris); (*[

(1, ["1"], #Given,Streckenlast, ["q_0"]),

(2, ["1"], #Given,FunktionsVariable, ["x"]),

(3, ["1"], #Find,Funktionen, ["funs'''"])]*)

(*+*)writeln (pats2str' ppc);

(*["(#Given, (Streckenlast, q__q))

","(#Given, (FunktionsVariable, v_v))

","(#Given, (Biegelinie, id_fun))

","(#Given, (AbleitungBiegelinie, id_abl))

","(#Find, (Funktionen, fun_s))"]*)

(*+*)writeln (pats2str' ((#ppc o Specify.get_pbt) pI));

(*["(#Given, (Streckenlast, q_q))

","(#Given, (FunktionsVariable, v_v))

","(#Find, (Funktionen, funs'''))"]*)

        val oris = Specify.add_field' thy ppc oris

        val met = if met = [] then pbl else met

        val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls ) oris

;

(*+*)writeln (itms2str_ @{context} itms); (*[

(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),

(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),

(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))] *)

(*//----------- hack for funpack: generalise handling of meths which extend problem items -----\\*)

val itms =

  if mI' = ["Biegelinien", "ausBelastung"]

  then itms @

    [(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),

        [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),

      (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),

        [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),

    (5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),

        [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),

      (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),

        [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]

  else itms

(*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)

val itms' = itms @

  [(4, [1], true, "#Given", Cor ((@{term "Biegelinie"},

      [@{term "y::real \<Rightarrow> real"}]),

    (@{term "id_fun::real \<Rightarrow> real"},

      [@{term "y::real \<Rightarrow> real"}] ))),

  (5, [1], true, "#Given", Cor ((@{term "AbleitungBiegelinie"},

      [@{term "dy::real \<Rightarrow> real"}]),

    (@{term "id_abl::real \<Rightarrow> real"},

      [@{term "dy::real \<Rightarrow> real"}] )))]

val itms'' = itms @

  [(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),

      [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),

    (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),

      [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),

  (5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),

      [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),

    (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),

      [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]

;

if itms' = itms'' then () else error "itms BUIT BY HAND ARE BROKEN";

(*//-----------------------------------------^^^ Specify_Method ["Biegelinien", "ausBelastung"]-\\*)

val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt''''';

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*----------- 30 -----------*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*----------- 40 -----------*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*----------- 50 -----------*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*----------- 60 -----------*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*----------- 70 -----------*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*----------- 80 -----------*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*----------- 90 -----------*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*---------- 100 -----------*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*---------- 110 -----------*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*---------- 120 -----------*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*---------- 130 -----------*)

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;

if p = ([3], Pbl)

then

  case nxt of

    ("Add_Given", Add_Given "solveForVars [c_2, c_3, c_4]") => 

    (case f of

      PpcKF

          (Problem [],

           {Find = [Incompl "solution []"], Given =

            [Correct

              "equalities\n [0 = -1 * c_4 / -1,\n  0 =\n  (-24 * c_4 * EI + -24 * L * c_3 * EI + 12 * L ^^^ 2 * c_2 +\n   4 * L ^^^ 3 * c +\n   -1 * L ^^^ 4 * q_0) /\n  (-24 * EI),\n  0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]",

             Incompl "solveForVars [c]"],

            Relate = [], Where = [], With = []}) => ()

    | _ => error "Bsp.7.70 me changed 1")

  | _ => error "Bsp.7.70 me changed 2"

else error "Bsp.7.70 me changed 3";

(* NOTE: ^^^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed ^^^^^^^^^^^^^^^^^ *)