% For HTML
fir_filter5[w: [subrange(1, 5) -> real]]: THEORY
BEGIN
IMPORTING time, signal[real], sum
t: VAR time
% -- Signal Declarations
x: signal
y: signal
D(i: subrange(1, 8)): signal
% -- Behavior
ax1: AXIOM FORALL (i: subrange(1, 4)):
D(i)(t + 1) = w(i) * x(t)
ax2: AXIOM D(5)(t + 2) = w(5) * x(t)
ax3: AXIOM FORALL (i: subrange(6, 8)):
D(i)(t + 1) = D(10 - i)(t) + D(i - 1)(t)
ax4: AXIOM y(t) = D(1)(t) + D(8)(t)
% -- Invariant
fir_filter_char: THEOREM
FORALL (t: upfrom(5)):
y(t) = sum(LAMBDA (i: subrange(1, 5)): w(i) * x(t - i))
END fir_filter5