neuper@42256: (* Title: Test_Z_Transform neuper@42256: Author: Jan Rocnik neuper@42256: (c) copyright due to lincense terms. neuper@42256: 12345678901234567890123456789012345678901234567890123456789012345678901234567890 neuper@42256: 10 20 30 40 50 60 70 80 neuper@42256: *) neuper@42256: neuper@42290: theory Inverse_Z_Transform imports PolyEq DiffApp Partial_Fractions begin neuper@42256: neuper@42256: axiomatization where neuper@42256: rule1: "1 = \[n]" and neuper@42256: rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and neuper@42256: rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and jan@42367: rule4: "c * (z / (z - \)) = c * \^^^n * u [n]" and neuper@42256: rule5: "|| z || < || \ || ==> z / (z - \) = -(\^^^n) * u [-n - 1]" and jan@42367: rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]" (*and jan@42367: rule42: "(a * (z/(z-b)) + c * (z/(z-d))) = (a * b^^^n * u [n] + c * d^^^n * u [n])"*) neuper@42256: neuper@42256: axiomatization where jan@42367: ruleZY: "(X z = a / b) = (X' z = a / (z * b))" and jan@42367: ruleYZ: "(a/b + c/d) = (a*(z/b) + c*(z/d))" neuper@42256: wneuper@59472: subsection\Define the Field Descriptions for the specification\ neuper@42279: consts neuper@42279: filterExpression :: "bool => una" neuper@42279: stepResponse :: "bool => una" neuper@42279: jan@42366: wneuper@59472: ML \ s1210629013@55444: val inverse_z = prep_rls'( wneuper@59416: Rule.Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), wneuper@59416: erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [], jan@42366: rules = jan@42367: [ wneuper@59416: Rule.Thm ("rule4", @{thm rule4}) jan@42366: ], wneuper@59416: scr = Rule.EmptyScr}); wneuper@59472: \ jan@42366: jan@42366: wneuper@59472: text \store the rule set for math engine\ jan@42366: wneuper@59472: setup \KEStore_Elems.add_rlss [("inverse_z", (Context.theory_name @{theory}, inverse_z))]\ jan@42366: wneuper@59472: subsection\Define the Specification\ wneuper@59472: ML \ neuper@42256: val thy = @{theory}; wneuper@59472: \ wneuper@59472: setup \KEStore_Elems.add_pbts wneuper@59416: [(Specify.prep_pbt thy "pbl_SP" [] Celem.e_pblID (["SignalProcessing"], [], Rule.e_rls, NONE, [])), wneuper@59406: (Specify.prep_pbt thy "pbl_SP_Ztrans" [] Celem.e_pblID wneuper@59416: (["Z_Transform","SignalProcessing"], [], Rule.e_rls, NONE, [])), wneuper@59406: (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Celem.e_pblID s1210629013@55339: (["Inverse", "Z_Transform", "SignalProcessing"], s1210629013@55339: (*^ capital letter breaks coding standard s1210629013@55339: because "inverse" = Const ("Rings.inverse_class.inverse", ..*) s1210629013@55339: [("#Given" ,["filterExpression (X_eq::bool)"]), s1210629013@55339: ("#Find" ,["stepResponse (n_eq::bool)"])], wneuper@59416: Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE, s1210629013@55339: [["SignalProcessing","Z_Transform","Inverse"]])), wneuper@59406: (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Celem.e_pblID s1210629013@55339: (["Inverse", "Z_Transform", "SignalProcessing"], s1210629013@55339: [("#Given" ,["filterExpression X_eq"]), s1210629013@55339: ("#Find" ,["stepResponse n_eq"])], wneuper@59416: Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE, wneuper@59472: [["SignalProcessing","Z_Transform","Inverse"]]))]\ neuper@42256: wneuper@59472: subsection \Define Name and Signature for the Method\ neuper@42256: consts neuper@42256: InverseZTransform :: "[bool, bool] => bool" neuper@42256: ("((Script InverseZTransform (_ =))// (_))" 9) neuper@42256: wneuper@59472: subsection \Setup Parent Nodes in Hierarchy of Method\ wneuper@59472: ML \val thy = @{theory}; (*latest version of thy required*)\ wneuper@59472: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_SP" [] Celem.e_metID s1210629013@55373: (["SignalProcessing"], [], wneuper@59416: {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls, wneuper@59416: errpats = [], nrls = Rule.e_rls}, "empty_script"), wneuper@59406: Specify.prep_met thy "met_SP_Ztrans" [] Celem.e_metID s1210629013@55373: (["SignalProcessing", "Z_Transform"], [], wneuper@59416: {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls, wneuper@59473: errpats = [], nrls = Rule.e_rls}, "empty_script")] wneuper@59473: \ wneuper@59505: (*ok wneuper@59504: partial_function (tailrec) inverse_ztransform :: "bool \ bool" wneuper@59504: where wneuper@59504: "inverse_ztransform X_eq = \ \(1/z) instead of z ^^^ -1\ wneuper@59504: (let X = Take X_eq; wneuper@59504: X' = Rewrite ''ruleZY'' False X; \ \z * denominator\ wneuper@59504: X' = (Rewrite_Set ''norm_Rational'' False) X'; \ \simplify\ wneuper@59504: funterm = Take (rhs X'); \ \drop X' z = for equation solving\ wneuper@59504: denom = (Rewrite_Set ''partial_fraction'' False) funterm; \ \get_denominator\ wneuper@59504: equ = (denom = (0::real)); wneuper@59504: fun_arg = Take (lhs X'); wneuper@59504: arg = (Rewrite_Set ''partial_fraction'' False) X'; \ \get_argument TODO\ wneuper@59504: L_L = SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''], wneuper@59504: [''Test'',''solve_linear'']) [BOOL equ, STRING ''z''] \ \PROG string\ wneuper@59504: in X) " wneuper@59505: *) wneuper@59473: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID s1210629013@55373: (["SignalProcessing", "Z_Transform", "Inverse"], s1210629013@55373: [("#Given" ,["filterExpression (X_eq::bool)"]), s1210629013@55373: ("#Find" ,["stepResponse (n_eq::bool)"])], wneuper@59416: {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls, wneuper@59416: errpats = [], nrls = Rule.e_rls}, s1210629013@55373: "Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*) s1210629013@55373: " (let X = Take X_eq;" ^ wneuper@59489: " X' = Rewrite ''ruleZY'' False X;" ^ (*z * denominator*) wneuper@59489: " X' = (Rewrite_Set ''norm_Rational'' False) X';" ^ (*simplify*) s1210629013@55373: " funterm = Take (rhs X');" ^ (*drop X' z = for equation solving*) wneuper@59489: " denom = (Rewrite_Set ''partial_fraction'' False) funterm;" ^ (*get_denominator*) s1210629013@55373: " equ = (denom = (0::real));" ^ s1210629013@55373: " fun_arg = Take (lhs X');" ^ wneuper@59489: " arg = (Rewrite_Set ''partial_fraction'' False) X';" ^ (*get_argument TODO*) s1210629013@55373: " (L_L::bool list) = " ^ wneuper@59489: " (SubProblem (''Test'', " ^ wneuper@59489: " [''LINEAR'',''univariate'',''equation'',''test'']," ^ wneuper@59489: " [''Test'',''solve_linear'']) " ^ s1210629013@55373: " [BOOL equ, REAL z]) " ^ wneuper@59473: " in X)")] wneuper@59473: \ wneuper@59504: (* wneuper@59504: Type unification failed: Clash of types "bool" and "_ itself" wneuper@59504: Type error in application: incompatible operand type wneuper@59504: Operator: Let (Take X_eq) :: (??'a itself \ ??'b) \ ??'b wneuper@59504: Operand: wneuper@59504: \X. let X' = Rewrite ''ruleZY'' ... wneuper@59504: : wneuper@59504: :partial_function (tailrec) inverse_ztransform2 :: "bool \ bool" wneuper@59504: where wneuper@59504: "inverse_ztransform X_eq = \ \(1/z) instead of z ^^^ -1\ wneuper@59504: (let X = Take X_eq; wneuper@59504: X' = Rewrite ''ruleZY'' False X; \ \z * denominator\ wneuper@59504: (num_orig::real) = get_numerator (rhs X'); wneuper@59504: X' = (Rewrite_Set ''norm_Rational'' False) X'; \ \simplify\ wneuper@59504: (X'_z::real) = lhs X'; wneuper@59504: (zzz::real) = argument_in X'_z; wneuper@59504: (funterm::real) = rhs X'; \ \drop X' z = for equation solving\ wneuper@59504: (denom::real) = get_denominator funterm; \ \get_denominator\ wneuper@59504: (num::real) = get_numerator funterm; \ \get_numerator\ wneuper@59504: (equ::bool) = (denom = (0::real)); wneuper@59504: (L_L::bool list) = (SubProblem (''PolyEq'', wneuper@59504: [''abcFormula'',''degree_2'',''polynomial'',''univariate'',''equation''], wneuper@59504: [''no_met'']) wneuper@59504: [BOOL equ, REAL zzz]); wneuper@59504: (facs::real) = factors_from_solution L_L; wneuper@59504: (eql::real) = Take (num_orig / facs); \ \---\ wneuper@59504: (eqr::real) = (Try (Rewrite_Set ''ansatz_rls'' False)) eql; \ \---\ wneuper@59504: (eq::bool) = Take (eql = eqr); \ \Maybe possible to use HOLogic.mk_eq ??\ wneuper@59504: eq = (Try (Rewrite_Set ''equival_trans'' False)) eq; \ \---\ wneuper@59504: (z1::real) = (rhs (NTH 1 L_L)); \ \prepare equation for a - eq_a therefor substitute z with solution 1 - z1\ wneuper@59504: (z2::real) = (rhs (NTH 2 L_L)); \ \---\ wneuper@59504: (eq_a::bool) = Take eq; wneuper@59504: eq_a = (Substitute [zzz=z1]) eq; wneuper@59504: eq_a = (Rewrite_Set ''norm_Rational'' False) eq_a; wneuper@59504: (sol_a::bool list) = wneuper@59504: (SubProblem (''Isac'', wneuper@59504: [''univariate'',''equation''],[''no_met'']) wneuper@59504: [BOOL eq_a, REAL (A::real)]); wneuper@59504: (a::real) = (rhs(NTH 1 sol_a)); \ \---\ wneuper@59504: (eq_b::bool) = Take eq; wneuper@59504: eq_b = (Substitute [zzz=z2]) eq_b; wneuper@59504: eq_b = (Rewrite_Set ''norm_Rational'' False) eq_b; wneuper@59504: (sol_b::bool list) = wneuper@59504: (SubProblem (''Isac'', wneuper@59504: [''univariate'',''equation''],[''no_met'']) wneuper@59504: [BOOL eq_b, REAL (B::real)]); wneuper@59504: (b::real) = (rhs(NTH 1 sol_b)); \ \---\ wneuper@59504: (pbz::real) = Take eqr; wneuper@59504: pbz = ((Substitute [A=a, B=b]) pbz); \ \---\ wneuper@59504: pbz = Rewrite ''ruleYZ'' False pbz; wneuper@59504: (X_z::bool) = Take (X_z = pbz); wneuper@59512: (n_eq::bool) = (Rewrite_Set ''inverse_z'' False) X_z wneuper@59504: in n_eq)" wneuper@59504: *) wneuper@59473: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID s1210629013@55373: (["SignalProcessing", "Z_Transform", "Inverse"], s1210629013@55373: [("#Given" ,["filterExpression X_eq"]), s1210629013@55373: ("#Find" ,["stepResponse n_eq"])], wneuper@59416: {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = srls_partial_fraction, prls = Rule.e_rls, wneuper@59416: crls = Rule.e_rls, errpats = [], nrls = Rule.e_rls}, s1210629013@55373: "Script InverseZTransform (X_eq::bool) = "^ s1210629013@55373: (*(1/z) instead of z ^^^ -1*) s1210629013@55373: "(let X = Take X_eq; "^ wneuper@59489: " X' = Rewrite ''ruleZY'' False X; "^ s1210629013@55373: (*z * denominator*) s1210629013@55373: " (num_orig::real) = get_numerator (rhs X'); "^ wneuper@59489: " X' = (Rewrite_Set ''norm_Rational'' False) X'; "^ s1210629013@55373: (*simplify*) s1210629013@55373: " (X'_z::real) = lhs X'; "^ s1210629013@55373: " (zzz::real) = argument_in X'_z; "^ s1210629013@55373: " (funterm::real) = rhs X'; "^ s1210629013@55373: (*drop X' z = for equation solving*) s1210629013@55373: " (denom::real) = get_denominator funterm; "^ s1210629013@55373: (*get_denominator*) s1210629013@55373: " (num::real) = get_numerator funterm; "^ s1210629013@55373: (*get_numerator*) s1210629013@55373: " (equ::bool) = (denom = (0::real)); "^ wneuper@59489: " (L_L::bool list) = (SubProblem (''PolyEq'', "^ wneuper@59489: " [''abcFormula'',''degree_2'',''polynomial'',''univariate'',''equation''], "^ wneuper@59489: " [''no_met'']) "^ s1210629013@55373: " [BOOL equ, REAL zzz]); "^ s1210629013@55373: " (facs::real) = factors_from_solution L_L; "^ s1210629013@55373: " (eql::real) = Take (num_orig / facs); "^ s1210629013@55373: wneuper@59499: " (eqr::real) = (Try (Rewrite_Set ''ansatz_rls'' False)) eql; "^ s1210629013@55373: s1210629013@55373: " (eq::bool) = Take (eql = eqr); "^ s1210629013@55373: (*Maybe possible to use HOLogic.mk_eq ??*) wneuper@59489: " eq = (Try (Rewrite_Set ''equival_trans'' False)) eq; "^ s1210629013@55373: s1210629013@55373: " (z1::real) = (rhs (NTH 1 L_L)); "^ s1210629013@55373: (* s1210629013@55373: * prepare equation for a - eq_a s1210629013@55373: * therefor substitute z with solution 1 - z1 s1210629013@55373: *) s1210629013@55373: " (z2::real) = (rhs (NTH 2 L_L)); "^ s1210629013@55373: s1210629013@55373: " (eq_a::bool) = Take eq; "^ s1210629013@55373: " eq_a = (Substitute [zzz=z1]) eq; "^ wneuper@59499: " eq_a = (Rewrite_Set ''norm_Rational'' False) eq_a; "^ s1210629013@55373: " (sol_a::bool list) = "^ wneuper@59489: " (SubProblem (''Isac'', "^ wneuper@59489: " [''univariate'',''equation''],[''no_met'']) "^ s1210629013@55373: " [BOOL eq_a, REAL (A::real)]); "^ s1210629013@55373: " (a::real) = (rhs(NTH 1 sol_a)); "^ s1210629013@55373: s1210629013@55373: " (eq_b::bool) = Take eq; "^ s1210629013@55373: " eq_b = (Substitute [zzz=z2]) eq_b; "^ wneuper@59489: " eq_b = (Rewrite_Set ''norm_Rational'' False) eq_b; "^ s1210629013@55373: " (sol_b::bool list) = "^ wneuper@59489: " (SubProblem (''Isac'', "^ wneuper@59489: " [''univariate'',''equation''],[''no_met'']) "^ s1210629013@55373: " [BOOL eq_b, REAL (B::real)]); "^ s1210629013@55373: " (b::real) = (rhs(NTH 1 sol_b)); "^ s1210629013@55373: s1210629013@55373: " (pbz::real) = Take eqr; "^ s1210629013@55373: " pbz = ((Substitute [A=a, B=b]) pbz); "^ s1210629013@55373: wneuper@59489: " pbz = Rewrite ''ruleYZ'' False pbz; "^ s1210629013@55373: s1210629013@55373: " (X_z::bool) = Take (X_z = pbz); "^ wneuper@59512: " (n_eq::bool) = (Rewrite_Set ''inverse_z'' False) X_z "^ wneuper@59473: "in n_eq)")] wneuper@59473: \ wneuper@59504: (* same error as in inverse_ztransform2 wneuper@59504: :partial_function (tailrec) inverse_ztransform3 :: "bool \ bool" wneuper@59504: where wneuper@59504: "inverse_ztransform X_eq = wneuper@59504: (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*) wneuper@59504: (let X = Take X_eq; wneuper@59504: (*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) wneuper@59504: X' = Rewrite ''ruleZY'' False X; wneuper@59504: (* ?X' z*) wneuper@59504: (X'_z::real) = lhs X'; wneuper@59504: (* z *) wneuper@59504: (zzz::real) = argument_in X'_z; wneuper@59504: (* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) wneuper@59504: (funterm::real) = rhs X'; wneuper@59504: (*-----*) wneuper@59504: (pbz::real) = (SubProblem (''Isac'', wneuper@59504: [''partial_fraction'',''rational'',''simplification''], wneuper@59504: [''simplification'',''of_rationals'',''to_partial_fraction'']) wneuper@59504: (*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) wneuper@59504: [REAL funterm, REAL zzz]); wneuper@59504: (*-----*) wneuper@59504: (*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) wneuper@59504: (pbz_eq::bool) = Take (X'_z = pbz); wneuper@59504: (*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*) wneuper@59504: pbz_eq = Rewrite ''ruleYZ'' False pbz_eq; wneuper@59504: (* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) wneuper@59504: (*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) wneuper@59504: (X_zeq::bool) = Take (X_z = rhs pbz_eq); wneuper@59504: (*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*) wneuper@59512: n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq wneuper@59504: (* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) wneuper@59504: in n_eq) " wneuper@59504: *) wneuper@59473: setup \KEStore_Elems.add_mets wneuper@59473: [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID s1210629013@55373: (["SignalProcessing", "Z_Transform", "Inverse_sub"], s1210629013@55373: [("#Given" ,["filterExpression X_eq"]), s1210629013@55373: ("#Find" ,["stepResponse n_eq"])], wneuper@59416: {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], wneuper@59416: srls = Rule.Rls {id="srls_partial_fraction", s1210629013@55373: preconds = [], rew_ord = ("termlessI",termlessI), wneuper@59416: erls = Rule.append_rls "erls_in_srls_partial_fraction" Rule.e_rls s1210629013@55373: [(*for asm in NTH_CONS ...*) wneuper@59416: Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"), s1210629013@55373: (*2nd NTH_CONS pushes n+-1 into asms*) wneuper@59416: Rule.Calc("Groups.plus_class.plus", eval_binop "#add_")], wneuper@59416: srls = Rule.Erls, calc = [], errpatts = [], wneuper@59416: rules = [Rule.Thm ("NTH_CONS", @{thm NTH_CONS}), wneuper@59416: Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"), wneuper@59416: Rule.Thm ("NTH_NIL", @{thm NTH_NIL}), wneuper@59491: Rule.Calc ("Tools.lhs", Tools.eval_lhs "eval_lhs_"), wneuper@59491: Rule.Calc ("Tools.rhs", Tools.eval_rhs"eval_rhs_"), wneuper@59416: Rule.Calc ("Atools.argument'_in", eval_argument_in "Atools.argument'_in"), wneuper@59416: Rule.Calc ("Rational.get_denominator", eval_get_denominator "#get_denominator"), wneuper@59416: Rule.Calc ("Rational.get_numerator", eval_get_numerator "#get_numerator"), wneuper@59416: Rule.Calc ("Partial_Fractions.factors_from_solution", wneuper@59512: eval_factors_from_solution "#factors_from_solution") wneuper@59512: ], scr = Rule.EmptyScr}, wneuper@59416: prls = Rule.e_rls, crls = Rule.e_rls, errpats = [], nrls = norm_Rational}, s1210629013@55373: (*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*) s1210629013@55373: "Script InverseZTransform (X_eq::bool) = "^ s1210629013@55373: (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*) s1210629013@55373: "(let X = Take X_eq; "^ s1210629013@55373: (*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) wneuper@59489: " X' = Rewrite ''ruleZY'' False X; "^ s1210629013@55373: (* ?X' z*) s1210629013@55373: " (X'_z::real) = lhs X'; "^ s1210629013@55373: (* z *) s1210629013@55373: " (zzz::real) = argument_in X'_z; "^ s1210629013@55373: (* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*) s1210629013@55373: " (funterm::real) = rhs X'; "^ s1210629013@55373: wneuper@59489: " (pbz::real) = (SubProblem (''Isac'', "^ wneuper@59489: " [''partial_fraction'',''rational'',''simplification''], "^ wneuper@59489: " [''simplification'',''of_rationals'',''to_partial_fraction'']) "^ s1210629013@55373: (*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) s1210629013@55373: " [REAL funterm, REAL zzz]); "^ s1210629013@55373: s1210629013@55373: (*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*) s1210629013@55373: " (pbz_eq::bool) = Take (X'_z = pbz); "^ s1210629013@55373: (*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*) wneuper@59489: " pbz_eq = Rewrite ''ruleYZ'' False pbz_eq; "^ s1210629013@55373: (* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) s1210629013@55373: (*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*) s1210629013@55373: " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^ s1210629013@55373: (*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*) wneuper@59512: " n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq "^ s1210629013@55373: (* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) s1210629013@55373: (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*) s1210629013@55373: "in n_eq)")] wneuper@59472: \ neuper@42256: neuper@42256: end neuper@42256: