real.why 8.04 KB
 Jean-Christophe Filliâtre committed Mar 23, 2010 1 `````` `````` MARCHE Claude committed Oct 19, 2010 2 ``````theory Real `````` MARCHE Claude committed Mar 26, 2010 3 `````` `````` Andrei Paskevich committed Jun 29, 2011 4 5 `````` function zero : real = 0.0 function one : real = 1.0 `````` MARCHE Claude committed Oct 19, 2010 6 `````` `````` Andrei Paskevich committed Jun 29, 2011 7 8 9 `````` predicate (< ) real real predicate (> ) (x y : real) = y < x predicate (<=) (x y : real) = x < y \/ x = y `````` MARCHE Claude committed Oct 19, 2010 10 `````` `````` Andrei Paskevich committed Jun 29, 2011 11 12 `````` clone export algebra.OrderedField with type t = real, function zero = zero, function one = one, predicate (<=) = (<=) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 13 `````` `````` MARCHE Claude committed Sep 05, 2011 14 ``````(* `````` MARCHE Claude committed Sep 04, 2011 15 `````` lemma sub_zero: forall x y:real. x - y = 0.0 -> x = y `````` MARCHE Claude committed Sep 05, 2011 16 ``````*) `````` MARCHE Claude committed Sep 04, 2011 17 `````` `````` MARCHE Claude committed Oct 19, 2010 18 19 20 21 22 23 ``````end theory RealInfix use import Real `````` Andrei Paskevich committed Jun 29, 2011 24 25 26 27 28 `````` function (+.) (x:real) (y:real) : real = x + y function (-.) (x:real) (y:real) : real = x - y function ( *.) (x:real) (y:real) : real = x * y function (/.) (x:real) (y:real) : real = x / y function (-._) (x:real) : real = - x `````` MARCHE Claude committed Oct 19, 2010 29 `````` `````` Andrei Paskevich committed Jun 29, 2011 30 31 32 33 `````` predicate (<=.) (x:real) (y:real) = x <= y predicate (>=.) (x:real) (y:real) = x >= y predicate ( <.) (x:real) (y:real) = x < y predicate ( >.) (x:real) (y:real) = x > y `````` MARCHE Claude committed Oct 19, 2010 34 35 `````` end `````` Jean-Christophe Filliâtre committed Mar 23, 2010 36 37 38 39 40 `````` theory Abs use import Real `````` Andrei Paskevich committed Jun 29, 2011 41 `````` function abs(x : real) : real = if x >= 0.0 then x else -x `````` Jean-Christophe Filliâtre committed Mar 23, 2010 42 `````` `````` Andrei Paskevich committed Jun 21, 2010 43 `````` lemma Abs_le: forall x y:real. abs x <= y <-> -y <= x <= y `````` MARCHE Claude committed Mar 25, 2010 44 `````` `````` Andrei Paskevich committed Jun 21, 2010 45 `````` lemma Abs_pos: forall x:real. abs x >= 0.0 `````` MARCHE Claude committed Mar 26, 2010 46 `````` `````` MARCHE Claude committed Sep 05, 2011 47 ``````(* `````` MARCHE Claude committed Sep 04, 2011 48 `````` lemma Abs_zero: forall x:real. abs x = 0.0 -> x = 0.0 `````` MARCHE Claude committed Sep 05, 2011 49 ``````*) `````` MARCHE Claude committed Sep 04, 2011 50 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 51 52 53 54 55 56 ``````end theory MinMax use import Real `````` Andrei Paskevich committed Jun 29, 2011 57 58 `````` function min real real : real function max real real : real `````` Jean-Christophe Filliâtre committed Mar 23, 2010 59 `````` `````` Andrei Paskevich committed Jun 29, 2011 60 61 62 63 `````` axiom Max_is_ge : forall x y:real. max x y >= x /\ max x y >= y axiom Max_is_some : forall x y:real. max x y = x \/ max x y = y axiom Min_is_le : forall x y:real. min x y <= x /\ min x y <= y axiom Min_is_some : forall x y:real. min x y = x \/ min x y = y `````` Jean-Christophe Filliâtre committed Mar 23, 2010 64 65 66 67 68 69 70 71 `````` end theory FromInt use int.Int use import Real `````` Andrei Paskevich committed Jun 29, 2011 72 `````` function from_int int : real `````` Jean-Christophe Filliâtre committed Mar 23, 2010 73 `````` `````` Andrei Paskevich committed Jun 21, 2010 74 75 `````` axiom Zero: from_int 0 = 0.0 axiom One: from_int 1 = 1.0 `````` Jean-Christophe Filliâtre committed Mar 23, 2010 76 `````` `````` MARCHE Claude committed Oct 19, 2010 77 `````` axiom Add: `````` Andrei Paskevich committed Jun 21, 2010 78 `````` forall x y:int. from_int (Int.(+) x y) = from_int x + from_int y `````` MARCHE Claude committed Oct 19, 2010 79 `````` axiom Sub: `````` Andrei Paskevich committed Jun 21, 2010 80 `````` forall x y:int. from_int (Int.(-) x y) = from_int x - from_int y `````` MARCHE Claude committed Oct 19, 2010 81 `````` axiom Mul: `````` Andrei Paskevich committed Jun 21, 2010 82 `````` forall x y:int. from_int (Int.(*) x y) = from_int x * from_int y `````` MARCHE Claude committed Oct 19, 2010 83 `````` axiom Neg: `````` Andrei Paskevich committed Jun 21, 2010 84 `````` forall x y:int. from_int (Int.(-_) (x)) = - from_int x `````` Jean-Christophe Filliâtre committed Mar 23, 2010 85 `````` `````` MARCHE Claude committed Mar 26, 2010 86 87 88 89 90 91 ``````end theory FromIntTest use import FromInt `````` Andrei Paskevich committed Jun 21, 2010 92 `````` lemma Test1: from_int 2 = 2.0 `````` MARCHE Claude committed Mar 26, 2010 93 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 94 95 96 97 ``````end theory Truncate `````` MARCHE Claude committed Mar 26, 2010 98 99 100 101 102 `````` use import Real use import FromInt (* truncate: rounds towards zero *) `````` Andrei Paskevich committed Jun 29, 2011 103 `````` function truncate real : int `````` MARCHE Claude committed Mar 26, 2010 104 105 `````` axiom Truncate_int : `````` Andrei Paskevich committed Jun 21, 2010 106 `````` forall i:int. truncate (from_int i) = i `````` MARCHE Claude committed Mar 26, 2010 107 108 `````` axiom Truncate_down_pos: `````` MARCHE Claude committed Oct 19, 2010 109 `````` forall x:real. x >= 0.0 -> `````` Andrei Paskevich committed Jun 21, 2010 110 `````` from_int (truncate x) <= x < from_int (Int.(+) (truncate x) 1) `````` MARCHE Claude committed Mar 26, 2010 111 112 `````` axiom Truncate_up_neg: `````` MARCHE Claude committed Oct 19, 2010 113 `````` forall x:real. x <= 0.0 -> `````` Andrei Paskevich committed Jun 21, 2010 114 `````` from_int (Int.(-) (truncate x) 1) < x <= from_int (truncate x) `````` MARCHE Claude committed Mar 26, 2010 115 116 `````` axiom Real_of_truncate: `````` Andrei Paskevich committed Jun 21, 2010 117 `````` forall x:real. x - 1.0 <= from_int (truncate x) <= x + 1.0 `````` MARCHE Claude committed Mar 26, 2010 118 119 `````` axiom Truncate_monotonic: `````` Andrei Paskevich committed Jun 21, 2010 120 `````` forall x y:real. x <= y -> Int.(<=) (truncate x) (truncate y) `````` MARCHE Claude committed Mar 26, 2010 121 122 `````` axiom Truncate_monotonic_int1: `````` Andrei Paskevich committed Jun 21, 2010 123 `````` forall x:real, i:int. x <= from_int i -> Int.(<=) (truncate x) i `````` MARCHE Claude committed Mar 26, 2010 124 125 `````` axiom Truncate_monotonic_int2: `````` Andrei Paskevich committed Jun 21, 2010 126 `````` forall x:real, i:int. from_int i <= x -> Int.(<=) i (truncate x) `````` MARCHE Claude committed Mar 26, 2010 127 128 129 `````` (* roundings up and down *) `````` Andrei Paskevich committed Jun 29, 2011 130 131 `````` function floor real : int function ceil real : int `````` MARCHE Claude committed Mar 26, 2010 132 133 `````` axiom Floor_int : `````` Andrei Paskevich committed Jun 21, 2010 134 `````` forall i:int. floor (from_int i) = i `````` MARCHE Claude committed Mar 26, 2010 135 136 `````` axiom Ceil_int : `````` Andrei Paskevich committed Jun 21, 2010 137 `````` forall i:int. floor (from_int i) = i `````` MARCHE Claude committed Mar 26, 2010 138 139 `````` axiom Floor_down: `````` Andrei Paskevich committed Jun 21, 2010 140 `````` forall x:real. from_int (floor x) <= x < from_int (Int.(+) (floor x) 1) `````` MARCHE Claude committed Mar 26, 2010 141 142 `````` axiom Ceil_up: `````` Andrei Paskevich committed Jun 21, 2010 143 `````` forall x:real. from_int (Int.(-) (ceil x) 1) < x <= from_int (ceil x) `````` MARCHE Claude committed Mar 26, 2010 144 145 `````` axiom Floor_monotonic: `````` Andrei Paskevich committed Jun 21, 2010 146 `````` forall x y:real. x <= y -> Int.(<=) (floor x) (floor y) `````` MARCHE Claude committed Mar 26, 2010 147 148 `````` axiom Ceil_monotonic: `````` Andrei Paskevich committed Jun 21, 2010 149 `````` forall x y:real. x <= y -> Int.(<=) (ceil x) (ceil y) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 150 151 152 `````` end `````` MARCHE Claude committed Mar 26, 2010 153 `````` `````` MARCHE Claude committed Mar 24, 2010 154 155 156 157 ``````theory Square use import Real `````` Andrei Paskevich committed Jun 29, 2011 158 `````` function sqr (x : real) : real = x * x `````` MARCHE Claude committed Mar 24, 2010 159 `````` `````` Andrei Paskevich committed Jun 29, 2011 160 `````` function sqrt real : real `````` MARCHE Claude committed Mar 24, 2010 161 `````` `````` MARCHE Claude committed Oct 19, 2010 162 `````` axiom Sqrt_positive: `````` Andrei Paskevich committed Jun 21, 2010 163 `````` forall x:real. x >= 0.0 -> sqrt x >= 0.0 `````` MARCHE Claude committed Mar 24, 2010 164 `````` `````` MARCHE Claude committed Oct 19, 2010 165 `````` axiom Sqrt_square: `````` Andrei Paskevich committed Jun 21, 2010 166 `````` forall x:real. x >= 0.0 -> sqr (sqrt x) = x `````` MARCHE Claude committed Mar 24, 2010 167 `````` `````` MARCHE Claude committed Oct 19, 2010 168 `````` axiom Square_sqrt: `````` Andrei Paskevich committed Jun 21, 2010 169 `````` forall x:real. x >= 0.0 -> sqrt (x*x) = x `````` Jean-Christophe Filliâtre committed Mar 23, 2010 170 171 172 `````` end `````` MARCHE Claude committed Mar 29, 2010 173 174 175 176 ``````theory SquareTest use import Square `````` Andrei Paskevich committed Jun 21, 2010 177 178 179 `````` lemma Sqrt_zero: sqrt 0.0 = 0.0 lemma Sqrt_one: sqrt 1.0 = 1.0 lemma Sqrt_four: sqrt 4.0 = 2.0 `````` MARCHE Claude committed Mar 29, 2010 180 181 182 `````` end `````` Jean-Christophe Filliâtre committed Mar 23, 2010 183 184 ``````theory ExpLog `````` MARCHE Claude committed Mar 24, 2010 185 186 `````` use import Real `````` Andrei Paskevich committed Jun 29, 2011 187 `````` function exp real : real `````` MARCHE Claude committed Mar 24, 2010 188 `````` axiom Exp_zero : exp(0.0) = 1.0 `````` Andrei Paskevich committed Jun 21, 2010 189 `````` axiom Exp_sum : forall x y:real. exp (x+y) = exp x * exp y `````` MARCHE Claude committed Mar 24, 2010 190 `````` `````` Andrei Paskevich committed Jun 29, 2011 191 `````` function e : real = exp 1.0 `````` MARCHE Claude committed Mar 25, 2010 192 `````` `````` Andrei Paskevich committed Jun 29, 2011 193 `````` function log real : real `````` Andrei Paskevich committed Jun 21, 2010 194 `````` axiom Log_one : log 1.0 = 0.0 `````` MARCHE Claude committed Oct 19, 2010 195 `````` axiom Log_mul : `````` Andrei Paskevich committed Jun 29, 2011 196 `````` forall x y:real. x > 0.0 /\ y > 0.0 -> log (x*y) = log x + log y `````` MARCHE Claude committed Mar 24, 2010 197 `````` `````` Andrei Paskevich committed Jun 21, 2010 198 `````` axiom Log_exp: forall x:real. log (exp x) = x `````` MARCHE Claude committed Mar 24, 2010 199 `````` `````` Andrei Paskevich committed Jun 21, 2010 200 `````` axiom Exp_log: forall x:real. x > 0.0 -> exp (log x) = x `````` MARCHE Claude committed Mar 24, 2010 201 `````` `````` Andrei Paskevich committed Jun 29, 2011 202 203 `````` function log2 (x : real) : real = log x / log 2.0 function log10 (x : real) : real = log x / log 10.0 `````` Jean-Christophe Filliâtre committed Mar 23, 2010 204 205 206 `````` end `````` MARCHE Claude committed Mar 29, 2010 207 208 209 210 ``````theory ExpLogTest use import ExpLog `````` Andrei Paskevich committed Jun 21, 2010 211 `````` lemma Log_e : log e = 1.0 `````` MARCHE Claude committed Mar 29, 2010 212 213 214 215 `````` end `````` MARCHE Claude committed Oct 19, 2010 216 ``````theory Power `````` Jean-Christophe Filliâtre committed Mar 23, 2010 217 `````` `````` MARCHE Claude committed Mar 24, 2010 218 219 220 221 `````` use import Real use import Square use import ExpLog `````` Andrei Paskevich committed Jun 29, 2011 222 `````` function pow real real : real `````` MARCHE Claude committed Mar 24, 2010 223 224 `````` axiom Pow_zero_y: `````` Andrei Paskevich committed Jun 21, 2010 225 `````` forall y:real. y <> 0.0 -> pow 0.0 y = 0.0 `````` MARCHE Claude committed Mar 24, 2010 226 227 `````` axiom Pow_x_zero: `````` Andrei Paskevich committed Jun 21, 2010 228 `````` forall x:real. x <> 0.0 -> pow x 0.0 = 1.0 `````` MARCHE Claude committed Mar 24, 2010 229 230 `````` axiom Pow_x_one: `````` Andrei Paskevich committed Jun 21, 2010 231 `````` forall x:real. pow x 1.0 = x `````` MARCHE Claude committed Mar 24, 2010 232 233 `````` axiom Pow_one_y: `````` Andrei Paskevich committed Jun 21, 2010 234 `````` forall y:real. pow 1.0 y = 1.0 `````` MARCHE Claude committed Mar 24, 2010 235 236 `````` axiom Pow_x_two: `````` Andrei Paskevich committed Jun 21, 2010 237 `````` forall x:real. pow x 2.0 = sqr x `````` MARCHE Claude committed Mar 24, 2010 238 239 `````` axiom Pow_half: `````` MARCHE Claude committed Oct 19, 2010 240 `````` forall x:real. x >= 0.0 -> pow x 0.5 = sqrt x `````` MARCHE Claude committed Mar 24, 2010 241 242 `````` axiom Pow_exp_log: `````` Andrei Paskevich committed Jun 21, 2010 243 `````` forall x y:real. x > 0.0 -> pow x y = exp (y * log x) `````` MARCHE Claude committed Mar 24, 2010 244 `````` `````` Jean-Christophe Filliâtre committed Mar 23, 2010 245 246 ``````end `````` MARCHE Claude committed Mar 29, 2010 247 248 249 250 ``````theory PowerTest use import Power `````` Andrei Paskevich committed Jun 21, 2010 251 `````` lemma Pow_2_2 : pow 2.0 2.0 = 4.0 `````` MARCHE Claude committed Mar 29, 2010 252 253 254 255 256 `````` end `````` MARCHE Claude committed Oct 19, 2010 257 ``````(** Trigonometric functions `````` MARCHE Claude committed Mar 25, 2010 258 259 `````` [http://en.wikipedia.org/wiki/Trigonometric_function] *) `````` MARCHE Claude committed Mar 29, 2010 260 ``````theory Trigonometry `````` MARCHE Claude committed Mar 25, 2010 261 262 263 264 265 `````` use import Real use import Square use import Abs `````` Andrei Paskevich committed Jun 29, 2011 266 267 `````` function cos real : real function sin real : real `````` MARCHE Claude committed Mar 25, 2010 268 269 `````` axiom Pythagorean_identity: `````` Andrei Paskevich committed Jun 21, 2010 270 `````` forall x:real. sqr (cos x) + sqr (sin x) = 1.0 `````` MARCHE Claude committed Mar 25, 2010 271 `````` `````` Andrei Paskevich committed Jun 21, 2010 272 273 `````` lemma Cos_le_one: forall x:real. abs (cos x) <= 1.0 lemma Sin_le_one: forall x:real. abs (sin x) <= 1.0 `````` MARCHE Claude committed Mar 25, 2010 274 `````` `````` Andrei Paskevich committed Jun 21, 2010 275 276 `````` axiom Cos_0: cos 0.0 = 1.0 axiom Sin_0: sin 0.0 = 0.0 `````` MARCHE Claude committed Mar 25, 2010 277 `````` `````` Andrei Paskevich committed Jun 29, 2011 278 `````` function pi : real `````` MARCHE Claude committed Mar 25, 2010 279 `````` `````` MARCHE Claude committed Apr 08, 2010 280 281 282 283 284 `````` axiom Pi_interval: 3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196 < pi < 3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197 `````` Andrei Paskevich committed Jun 21, 2010 285 286 `````` axiom Cos_pi: cos pi = -1.0 axiom Sin_pi: sin pi = 0.0 `````` MARCHE Claude committed Mar 25, 2010 287 `````` `````` Andrei Paskevich committed Jun 21, 2010 288 289 `````` axiom Cos_pi2: cos (0.5 * pi) = 0.0 axiom Sin_pi2: sin (0.5 * pi) = 1.0 `````` Jean-Christophe Filliâtre committed Mar 23, 2010 290 `````` `````` Andrei Paskevich committed Jun 21, 2010 291 292 `````` axiom Cos_plus_pi: forall x:real. cos (x + pi) = - cos x axiom Sin_plus_pi: forall x:real. sin (x + pi) = - sin x `````` MARCHE Claude committed Mar 25, 2010 293 `````` `````` Andrei Paskevich committed Jun 21, 2010 294 295 `````` axiom Cos_plus_pi2: forall x:real. cos (x + 0.5*pi) = - sin x axiom Sin_plus_pi2: forall x:real. sin (x + 0.5*pi) = cos x `````` MARCHE Claude committed Mar 25, 2010 296 297 `````` axiom Cos_neg: `````` Andrei Paskevich committed Jun 21, 2010 298 `````` forall x:real. cos (-x) = cos x `````` MARCHE Claude committed Mar 25, 2010 299 `````` axiom Sin_neg: `````` Andrei Paskevich committed Jun 21, 2010 300 `````` forall x:real. sin (-x) = - sin x `````` MARCHE Claude committed Oct 19, 2010 301 `````` `````` MARCHE Claude committed Mar 25, 2010 302 `````` axiom Cos_sum: `````` Andrei Paskevich committed Jun 21, 2010 303 `````` forall x y:real. cos (x+y) = cos x * cos y - sin x * sin y `````` MARCHE Claude committed Mar 25, 2010 304 `````` axiom Sin_sum: `````` Andrei Paskevich committed Jun 21, 2010 305 `````` forall x y:real. sin (x+y) = sin x * cos y + cos x * sin y `````` MARCHE Claude committed Mar 25, 2010 306 `````` `````` Andrei Paskevich committed Jun 29, 2011 307 308 `````` function tan (x : real) : real = sin x / cos x function atan real : real `````` MARCHE Claude committed Mar 25, 2010 309 `````` axiom Tan_atan: `````` Andrei Paskevich committed Jun 21, 2010 310 `````` forall x:real. tan (atan x) = x `````` Jean-Christophe Filliâtre committed Mar 23, 2010 311 312 313 `````` end `````` MARCHE Claude committed Mar 29, 2010 314 315 316 317 318 319 ``````theory TrigonometryTest use import Real use import Trigonometry use import Square `````` Andrei Paskevich committed Jun 21, 2010 320 `````` lemma Cos_2_pi : cos (2.0 * pi) = 1.0 `````` Jean-Christophe Filliâtre committed Jul 08, 2010 321 `````` lemma Sin_2_pi : sin (2.0 * pi) = 0. `````` Andrei Paskevich committed Jun 21, 2010 322 323 `````` lemma Tan_pi_3 : tan (pi / 2.0) = sqrt 3.0 lemma Atan_1 : atan 1.0 = pi / 4.0 `````` MARCHE Claude committed Mar 29, 2010 324 325 326 `````` end `````` MARCHE Claude committed Oct 19, 2010 327 ``````(** hyperbolic functions `````` MARCHE Claude committed Mar 25, 2010 328 329 `````` [http://en.wikipedia.org/wiki/Hyperbolic_function] *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 330 331 ``````theory Hyperbolic `````` MARCHE Claude committed Mar 25, 2010 332 333 334 335 `````` use import Real use import Square use import ExpLog `````` Andrei Paskevich committed Jun 29, 2011 336 337 338 `````` function sinh (x : real) : real = 0.5 * (exp x - exp (-x)) function cosh (x : real) : real = 0.5 * (exp x + exp (-x)) function tanh (x : real) : real = sinh x / cosh x `````` MARCHE Claude committed Mar 25, 2010 339 `````` `````` Andrei Paskevich committed Jun 29, 2011 340 341 `````` function asinh (x : real) : real = log (x + sqrt (sqr x + 1.0)) function acosh (x : real) : real `````` MARCHE Claude committed Dec 15, 2010 342 343 `````` axiom Acosh_def: forall x:real. x >= 1.0 -> acosh x = log (x + sqrt (sqr x - 1.0)) `````` Andrei Paskevich committed Jun 29, 2011 344 `````` function atanh (x : real) : real `````` MARCHE Claude committed Dec 15, 2010 345 346 `````` axiom Atanh_def: forall x:real. -1.0 < x < 1.0 -> atanh x = 0.5 * log ((1.0+x)/(1.0-x)) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 347 348 349 `````` end `````` MARCHE Claude committed Oct 19, 2010 350 ``````(** polar coordinates: atan2, hypot `````` MARCHE Claude committed Mar 25, 2010 351 352 `````` [http://en.wikipedia.org/wiki/Atan2] *) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 353 354 ``````theory Polar `````` MARCHE Claude committed Mar 25, 2010 355 356 `````` use import Real use import Square `````` MARCHE Claude committed Mar 29, 2010 357 `````` use import Trigonometry `````` MARCHE Claude committed Mar 25, 2010 358 `````` `````` Andrei Paskevich committed Jun 29, 2011 359 360 `````` function hypot (x y : real) : real = sqrt (sqr x + sqr y) function atan2 real real : real `````` MARCHE Claude committed Oct 19, 2010 361 `````` `````` MARCHE Claude committed Mar 25, 2010 362 `````` axiom X_from_polar: `````` Andrei Paskevich committed Jun 21, 2010 363 `````` forall x y:real. x = hypot x y * cos (atan2 y x) `````` MARCHE Claude committed Mar 25, 2010 364 365 `````` axiom Y_from_polar: `````` Andrei Paskevich committed Jun 21, 2010 366 `````` forall x y:real. y = hypot x y * sin (atan2 y x) `````` Jean-Christophe Filliâtre committed Mar 23, 2010 367 368 ``````end ``````