#|
Copyright (C) 1994 by Robert S. Boyer, J Strother Moore, and Mike Green.  All
Rights Reserved.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
Robert S. Boyer, J Strother Moore, and Mike Green PROVIDE ABSOLUTELY NO
WARRANTY.  THE EVENT SCRIPT IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND,
EITHER EXPRESS OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.  THE
ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE SCRIPT IS WITH YOU.
SHOULD THE SCRIPT PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY
SERVICING, REPAIR OR CORRECTION.
IN NO EVENT WILL Robert S. Boyer, J Strother Moore, or Mike Green BE LIABLE
TO YOU FOR ANY DAMAGES, ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL,
INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE
THIS SCRIPT (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED
INACCURATE OR LOSSES SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US
OF THE POSSIBILITY OF SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.''
|#

Event: Start with the library "fortran" using the compiled version.

Event: For efficiency, compile those definitions not yet compiled.

Theorem: zplus-comm1 zplus (x, y) = zplus (y, x)

Theorem: zplus-comm2 zplus (x, zplus (y, z)) = zplus (y, zplus (x, z))

Theorem: zplus-assoc zplus (zplus (x, y), z) = zplus (x, zplus (y, z))

Event: Disable zplus.

Event: Add the shell vehicle-state, with recognizer function symbol vehiclestatep and 3 accessors: w, with type restriction (none-of) and default value zero; y, with type restriction (none-of) and default value zero; v, with type restriction (none-of) and default value zero.

Definition: hd (x) = car (x)

Definition: tl (x) = cdr (x)

Definition: empty (x) = (¬ listp (x))

Theorem: tl-rewrite tl (x) = cdr (x)

Event: Disable tl.

Theorem: down-on-tl (¬ empty (x)) → (count (tl (x)) < count (x))

Definition: random-delta-ws (lst) = if empty (lst) then t

else ((hd (lst) = -1)

∨ (hd (lst) = 0) ∨ (hd (lst) = 1)) ∧ random-delta-ws (tl (lst)) endif

Definition: controller (sgn-y, sgn-old-y) = zplus (ztimes (-3, sgn-y), ztimes (2, sgn-old-y))

Event: Disable controller.

Definition: sgn (x) = if negativep (x)

then if negative-guts (x) = 0 then 0

else -1 endif elseif x ≃ 0 then 0 else 1 endif

Event: Disable sgn.

Definition: next-state (delta-w, state) = vehicle-state (zplus (w (state), delta-w),

zplus (y (state), zplus (v (state), zplus (w (state), delta-w))), zplus (v (state),

controller (sgn (zplus (y (state),

zplus (v (state),

zplus (w (state), delta-w)))),

sgn (y (state)))))

Definition: final-state-of-vehicle (delta-ws, state) = if empty (delta-ws) then state

else final-state-of-vehicle (tl (delta-ws), next-state (hd (delta-ws), state)) endif

Definition: good-statep (state) = if y (state) = 0

then (zplus (v (state), w (state)) = -1)

∨ (zplus (v (state), w (state)) = 0) ∨ (zplus (v (state), w (state)) = 1)

elseif y (state) = 1 then (zplus (v (state), w (state)) = -2)

∨ (zplus (v (state), w (state)) = -3) elseif y (state) = 2 then (zplus (v (state), w (state)) = -1)

∨ (zplus (v (state), w (state)) = -2) elseif y (state) = 3 then zplus (v (state), w (state)) = -1 elseif y (state) = -3 then zplus (v (state), w (state)) = 1 elseif y (state) = -2 then (zplus (v (state), w (state)) = 1)

∨ (zplus (v (state), w (state)) = 2) elseif y (state) = -1 then (zplus (v (state), w (state)) = 2)

∨ (zplus (v (state), w (state)) = 3) else f endif

Theorem: next-good-state (good-statep (state) ∧ ((r = -1) ∨ (r = 0) ∨ (r = 1))) → good-statep (next-state (r, state))

Definition: zero-delta-ws (lst) = if empty (lst) then t

else (hd (lst) = 0) ∧ zero-delta-ws (tl (lst)) endif Definition: concat (x, y) = if empty (x) then y

else cons (hd (x), concat (tl (x), y)) endif

Definition: length (x) = if empty (x) then 0

else 1 + length (tl (x)) endif

Theorem: length-0 (length (x) = 0) = empty (x)

Theorem: decompose-list-of-length-4 zero-delta-ws (lst) → ((length (lst) < 4) = (lst ≠ concat ('(0 0 0 0), cddddr (lst))))

Theorem: drift-to-0-in-4 good-statep (state) → (y (final-state-of-vehicle ('(0 0 0 0), state)) = 0)

Theorem: cancel-wind-in-4 good-statep (state) → (zplus (v (final-state-of-vehicle ('(0 0 0 0), state)),

w (final-state-of-vehicle ('(0 0 0 0), state))) = 0)

Theorem: once-0-always-0 (zero-delta-ws (lst) ∧ (y (state) = 0) ∧ (zplus (w (state), v (state)) = 0)) → ((y (final-state-of-vehicle (lst, state)) = 0)

∧ (zplus (v (final-state-of-vehicle (lst, state)),

w (final-state-of-vehicle (lst, state))) = 0))

Theorem: final-state-of-vehicle-concat final-state-of-vehicle (concat (a, b), state) = final-state-of-vehicle (b, final-state-of-vehicle (a, state))

Theorem: zero-delta-ws-concat zero-delta-ws (concat ('(0 0 0 0), v)) = zero-delta-ws (v)

Event: Disable concat.

Event: Disable next-state.

Theorem: good-statep-bounded-above good-statep (state) → (¬ zlessp (3, y (state)))

Theorem: good-statep-bounded-below good-statep (state) → (¬ zlessp (y (state), -3))

Event: Disable good-statep.

Theorem: zlessp-is-lessp ((x ∈ N) ∧ (y ∈ N)) → (zlessp (x, y) = (x < y))

Event: Disable zlessp.

Definition: fsv (d, s) = if empty (d) then s

else fsv (tl (d), next-state (hd (d), s)) endif

Theorem: all-good-states (random-delta-ws (lst) ∧ good-statep (state)) → good-statep (final-state-of-vehicle (lst, state))

Theorem: vehicle-stays-within-3-of-course (random-delta-ws (lst) ∧ (state = final-state-of-vehicle (lst, vehicle-state (0, 0, 0)))) → (zlesseqp (-3, y (state)) ∧ zlesseqp (y (state), 3))

Event: Disable final-state-of-vehicle.

Theorem: zero-delta-ws-cddddr zero-delta-ws (x) → zero-delta-ws (cddddr (x))

Theorem: good-states-find-and-stay-at-0 (good-statep (state) ∧ zero-delta-ws (lst2 ) ∧ (length (lst2 ) ≮ 4)) → (y (final-state-of-vehicle (lst2 , state)) = 0)

Theorem: vehicle-gets-on-course-in-steady-wind (random-delta-ws (lst1 ) ∧ zero-delta-ws (lst2 ) ∧ zgreatereqp (length (lst2 ), 4) ∧ (state = final-state-of-vehicle (concat (lst1 , lst2 ),

vehicle-state (0, 0, 0))))

→ (y (state) = 0)

Index

all-good-states, 5

cancel-wind-in-4, 4 concat, 4, 5 controller, 2, 3

decompose-list-of-length-4, 4 down-on-tl, 2 drift-to-0-in-4, 4

empty, 2–5

final-state-of-vehicle, 3–5 final-state-of-vehicle-concat, 4 fsv, 5

good-statep, 3–5 good-statep-bounded-above, 5 good-statep-bounded-below, 5 good-states-find-and-stay-at-0, 5

hd, 2–5

length, 4, 5 length-0, 4

next-good-state, 3 next-state, 3, 5

once-0-always-0, 4

random-delta-ws, 2, 5

sgn, 2, 3

tl, 2–5 tl-rewrite, 2

v, 3, 4 vehicle-gets-on-course-in-stead

y-wind, 5 vehicle-state, 2, 3, 5 vehicle-stays-within-3-of-course, 5 w, 3, 4

y, 3–5

zero-delta-ws, 3–5 zero-delta-ws-cddddr, 5 zero-delta-ws-concat, 4 zgreatereqp, 5 zlesseqp, 5 zlessp, 5 zlessp-is-lessp, 5 zplus, 1–4 zplus-assoc, 1 zplus-comm1, 1 zplus-comm2, 1 ztimes, 2