Lines Matching defs:when
30 let when = definition `tempabs` `when`;;
63 Def ((reset when (isHi clk)) t) /\
64 Defn n ((inp when (isHi clk)) t) /\
65 (((reset when (isHi clk)) t = Hi) \/
66 (Defn n ((out when (isHi clk)) t)))
68 Defn n ((out when (isHi clk)) (t+1)) /\
69 (WordVal n (WordAbs ((out when (isHi clk)) (t+1))) =
70 (BoolAbs ((reset when (isHi clk)) t) =>
71 (WordVal n (WordAbs ((inp when (isHi clk)) t))) |
72 (((WordVal n (WordAbs ((out when (isHi clk)) t))) + 1)
74 let REGn_thm = (BETA_RULE (PURE_REWRITE_RULE [when] REGn_CORRECT))
76 PURE_REWRITE_TAC [COUNT_IMP;when] THEN
101 (!t. Def ((reset when (isHi clk)) t)) /\
102 (!t. Defn n ((inp when (isHi clk)) t))
105 ((reset when (isHi clk)) sysinit = Hi)
108 Defn n ((out when (isHi clk)) (t+1)) /\
109 (WordVal n (WordAbs ((out when (isHi clk)) (t+1))) =
110 (BoolAbs ((reset when (isHi clk)) t) =>
111 (WordVal n (WordAbs ((inp when (isHi clk)) t))) |
112 (((WordVal n (WordAbs ((out when (isHi clk)) t))) + 1)
150 (!t. sysinit <= t ==> Def ((reset when (isHi clk)) t)) /\
151 (!t. sysinit <= t ==> Defn n ((inp when (isHi clk)) t)) /\
152 ((reset when (isHi clk)) sysinit = Hi)
155 Defn n ((out when (isHi clk)) (t+1)) /\
156 (WordVal n (WordAbs ((out when (isHi clk)) (t+1))) =
157 (BoolAbs ((reset when (isHi clk)) t) =>
158 (WordVal n (WordAbs ((inp when (isHi clk)) t))) |
159 (((WordVal n (WordAbs ((out when (isHi clk)) t))) + 1)