1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Mon Apr 19 20:44:18 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Tue Apr 20 16:58:44 2021 +0200
     1.3 @@ -9,10 +9,10 @@
     1.4    rule1: "1 = \<delta>[n]" and
     1.5    rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and
     1.6    rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and 
     1.7 -  rule4: "c * (z / (z - \<alpha>)) = c * \<alpha>^^^n * u [n]" and
     1.8 -  rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha>^^^n) * u [-n - 1]" and
     1.9 -  rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]" (*and
    1.10 -  rule42: "(a * (z/(z-b)) + c * (z/(z-d))) = (a * b^^^n * u [n] + c * d^^^n * u [n])"*)
    1.11 +  rule4: "c * (z / (z - \<alpha>)) = c * \<alpha> \<up> n * u [n]" and
    1.12 +  rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha> \<up> n) * u [-n - 1]" and
    1.13 +  rule6: "|| z || > 1 ==> z/(z - 1) \<up> 2 = n * u [n]" (*and
    1.14 +  rule42: "(a * (z/(z-b)) + c * (z/(z-d))) = (a * b \<up> n * u [n] + c * d \<up> n * u [n])"*)
    1.15  
    1.16  axiomatization where
    1.17  (*ruleZY: "(X z = a / b) = (d_d z X = a / (z * b))"         ..looks better, but types are flawed*)