#|
Copyright (C) 1995 by Matthew Wilding and Computational Logic, Inc.
All Rights Reserved.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
Matthew Wilding and Computational Logic, Inc. PROVIDES 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 Matthew Wilding and Computational Logic, Inc. 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.
|#
;; This file contains the events that lead to the proof of the
;; optimality of an earliest-deadline-first scheduler on any set of
;; periodic tasks.  It is documented in CLI Technical Report #110.
;;
;; Report #110 will not be available for public dissemination until
;; December 1995 at the earliest, but the portion about this proof is
;; available as ftp://ftp.cli.com/home/wilding/scheduler-proof.ps
;;
;; Matt Wilding
;; September, 1995

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

Definition: tk-name (pt) = car (pt)

Definition: tk-period (pt) = cadr (pt)

Definition: tk-duration (pt) = caddr (pt)

; periodic task is a triple (name period duration)

Definition: periodic-taskp (pt) = (listp (pt)

∧ litatom (tk-name (pt)) ∧ (tk-name (pt) ≠ nil) ∧ (0 < tk-period (pt)) ∧ (0 < tk-duration (pt)) ∧ (nil = cdr (cdr (cdr (pt)))))

Definition: periodic-tasksp (pts) = if listp (pts)

then periodic-taskp (car (pts))

∧ (¬ assoc (tk-name (car (pts)), cdr (pts))) ∧ periodic-tasksp (cdr (pts))

else pts = nil endif

;; a task request has the form (name request-time deadline-time duration)
;; generate the requests for a periodic task during a time period

Definition: periodic-task-requests (pt, starting-time, ending-time) = if periodic-taskp (pt)

then if starting-time < ending-time then cons (list (tk-name (pt),

starting-time,

starting-time + tk-period (pt), tk-duration (pt)), periodic-task-requests (pt,

starting-time + tk-period (pt), ending-time))

else nil endif else nil endif

;; we generate a list of task request lists

Definition: periodic-tasks-requests (pts, starting-time, ending-time) = if periodic-tasksp (pts)

then if listp (pts) then append (periodic-task-requests (car (pts),

starting-time, ending-time),

periodic-tasks-requests (cdr (pts), starting-time, ending-time))

else nil endif else nil endif

Definition: repeat (n, val) = if n ≃ 0 then nil

else cons (val, repeat (n − 1, val)) endif

;; produce an "obvious" schedule of length c that consists of
;; (duration/period)*c calls of each task in a periodic task list

Definition: substring-schedule (pts, bigp) = if listp (pts)

then append (repeat ((bigp ∗ caddar (pts)) ÷ cadar (pts), caar (pts)), substring-schedule (cdr (pts), bigp))

else nil endif

Definition: make-length (length, list, fill) = if length ≃ 0 then nil

elseif listp (list)

then cons (car (list), make-length (length − 1, cdr (list), fill))

else cons (fill, make-length (length − 1, nil, fill)) endif

Definition: repeat-list (list, times) = if times ≃ 0 then nil

else append (list, repeat-list (list, times − 1)) endif

Definition: make-simple-schedule (pts, bigp, length) = repeat-list (make-length (bigp, substring-schedule (pts, bigp), nil),

length ÷ bigp)

Definition: firstn (n, list) = if n ≃ 0 then nil

else cons (car (list), firstn (n − 1, cdr (list))) endif Definition: nth (n, list) = if n ≃ 0 then car (list)

else nth (n − 1, cdr (list)) endif

Definition: nthcdr (n, list) = if n ≃ 0 then list

else nthcdr (n − 1, cdr (list)) endif

Definition: length (list) = if listp (list) then 1 + length (cdr (list))

else 0 endif

Theorem: length-append length (append (x, y)) = (length (x) + length (y))

Theorem: length-firstn length (firstn (n, list)) = fix (n)

Theorem: length-nthcdr length (nthcdr (n, list)) = (length (list) − n)

Theorem: equal-length-0 (length (x) = 0) = (¬ listp (x))

;; each task request period is a multiple of bigp, and bigp*duration
;; is a multiple of period

Definition: expanded-tasksp (ts, p) = if listp (ts)

then ((cadar (ts) mod p) ≃ 0) ∧ ((caddar (ts) mod p) ≃ 0) ∧ (((p ∗ caddar (ts)) mod cadar (ts)) ≃ 0) ∧ expanded-tasksp (cdr (ts), p)

else t endif

Definition: plist (list) = if listp (list) then cons (car (list), plist (cdr (list)))

else nil endif

Definition: name (r) = car (r)

Definition: request-time (r) = cadr (r)

Definition: deadline (r) = caddr (r)

Definition: duration (r) = cadddr (r)

Event: Let us define the theory task-abbr to consist of the following events: name, request-time, deadline, duration, tk-name, tk-duration, tk-period.

Definition: good-schedule (s, r) = if listp (r)

then (occurrences (name (car (r)),

firstn (deadline (car (r)) − request-time (car (r)), nthcdr (request-time (car (r)), s)))

= duration (car (r))) ∧ good-schedule (s, cdr (r))

else t endif

Definition: big-period (pts) = if listp (pts) then tk-period (car (pts)) ∗ big-period (cdr (pts))

else 1 endif

Definition: active-task-requests (time, r) = if listp (r)

then if (time < deadline (car (r)))

∧ (time ≮ request-time (car (r))) then cons (car (r), active-task-requests (time, cdr (r))) else active-task-requests (time, cdr (r)) endif

else nil endif

Definition: unfulfilled (time, s, r) = if listp (r)

then if occurrences (name (car (r)),

firstn (time − request-time (car (r)),

nthcdr (request-time (car (r)), s)))

= duration (car (r)) then unfulfilled (time, s, cdr (r)) else cons (car (r), unfulfilled (time, s, cdr (r))) endif

else nil endif

;; return a task request with least deadline

Definition: least-deadline (r) = if listp (r)

then if listp (cdr (r))

then if deadline (car (r)) < deadline (car (cdr (r))) then least-deadline (cons (car (r), cdr (cdr (r)))) else least-deadline (cdr (r)) endif

else car (r) endif else nil endif

;; return location of first instance of task in s no earlier than time

Definition: first-instance (time, task, s) = if time < length (s)

then if nth (time, s) = task then time

else first-instance (1 + time, task, s) endif else f endif

Definition: replace-nth (n, val, list) = if n ≃ 0 then cons (val, cdr (list))

else cons (car (list), replace-nth (n − 1, val, cdr (list))) endif

;; swap locations i and j in list

Definition: swap (i, j , list) = replace-nth (i, nth (j , list), replace-nth (j , nth (i, list), list))

Theorem: length-replace-nth length (replace-nth (i, val, list)) = if i < length (list) then length (list)

else 1 + i endif

Theorem: length-swap length (swap (i, j , list)) = if i < length (list)

then if j < length (list) then length (list)

else 1 + j endif elseif i < j then 1 + j else 1 + i endif

Definition: make-element-edf (s, r, time)

= let unfulfilled be unfulfilled (time, s, active-task-requests (time, r)) in let first be first-instance (time,

car (least-deadline (unfulfilled)), s)

in

if listp (unfulfilled) ∧ first then swap (time, first, s)

else s endif endlet endlet

Theorem: lessp-first-instance listp (s) → (first-instance (time, task, s) < length (s))

Theorem: length-make-element-edf (time < length (s)) → (length (make-element-edf (s, r, time)) = length (s))

Event: Disable make-element-edf.

Definition: make-schedule-edf (s, r, first) = if first < length (s)

then make-schedule-edf (make-element-edf (s, r, first), r, 1 + first) else s endif

Event: Enable make-element-edf.

;;;;;;;;

Theorem: plist-repeat-list plist (repeat-list (s, n)) = repeat-list (s, n)

Theorem: length-repeat-list length (repeat-list (s, n)) = (n ∗ length (s))

Theorem: append-nil append (list, nil) = plist (list)

Theorem: good-schedule-append good-schedule (s, append (r1 , r2 )) = (good-schedule (s, r1 ) ∧ good-schedule (s, r2 ))

;; introduce the useful notion of sublist

Definition: sublistp (a, b) = if listp (b)

then if listp (a)

then if car (a) = car (b) then sublistp (cdr (a), cdr (b))

else sublistp (a, cdr (b)) endif else t endif

else a ≃ nil endif

Definition: remove-until (v, l) = if listp (l)

then if v = car (l) then cdr (l)

else remove-until (v, cdr (l)) endif else l endif

Theorem: sublistp-cons-rewrite sublistp (cons (c, x), y) = ((c ∈ y) ∧ sublistp (x, remove-until (c, y)))

Theorem: listp-remove-until-means-listp listp (remove-until (a, z)) → listp (z)

Theorem: lessp-remove-until (length (remove-until (a, y)) < length (y)) = listp (y)

Theorem: remove-until-append remove-until (a, append (x, y)) = if a ∈ x then append (remove-until (a, x), y)

else remove-until (a, y) endif

Definition: list-until (v, l) = if listp (l)

then if v = car (l) then list (v)

else cons (car (l), list-until (v, cdr (l))) endif else l endif

Theorem: append-remove-until-list-until append (list-until (v, l), remove-until (v, l)) = l

;; amazingly complex - easier way? (took me ~3 hours to prove this little guy)

Definition: sublistp-append-induct (a, b, y, z) = if listp (a)

then sublistp-append-induct (cdr (a), b, append (y, list-until (car (a), z)), remove-until (car (a), z))

elseif b ≃ nil then t elseif listp (y) then if car (b) ∈ y

then sublistp-append-induct (list (car (b)), cdr (b), remove-until (car (b), y), z)

else t endif else t endif

Theorem: member-append (a ∈ append (x, y)) = ((a ∈ x) ∨ (a ∈ y))

Theorem: listp-bagint-with-singleton-implies-member listp (bagint (y, list (z))) → (z ∈ y)

Theorem: bagint-singleton bagint (x, list (y)) = if y ∈ x then list (y)

else nil endif

Theorem: transitivity-of-append append (append (a, b), c) = append (a, append (b, c))

Theorem: sublistp-append sublistp (append (a, b), z) → sublistp (b, append (y, z))

Theorem: sublistp-cdr1 sublistp (x, y) → sublistp (cdr (x), y)

Theorem: sublistp-cdr2 sublistp (x, cdr (y)) → sublistp (x, y)

Theorem: remainder-big-period-sublist (periodic-tasksp (y) ∧ sublistp (x, y)) → ((big-period (y) mod big-period (x)) = 0)

Theorem: remainder-big-period-cdr ((n mod big-period (pts)) = 0) → ((n mod big-period (cdr (pts))) = 0)

Theorem: repeat-list-plus repeat-list (l, a + b) = append (repeat-list (l, a), repeat-list (l, b))

Theorem: nthcdr-append nthcdr (n, append (l1 , l2 )) = if n < length (l1 ) then append (nthcdr (n, l1 ), l2 )

else nthcdr (n − length (l1 ), l2 ) endif

Theorem: firstn-append firstn (n, append (l1 , l2 )) = if length (l1 ) < n then append (l1 , firstn (n − length (l1 ), l2 ))

else firstn (n, l1 ) endif

Definition: nthcdr-repeat-list-induct (n1 , n2 , list) = if n1 ≃ 0 then t

else nthcdr-repeat-list-induct (n1 − 1, n2 − length (list), list) endif

Theorem: nthcdr-repeat-list (((n1 mod length (list)) = 0) ∧ ((n2 ∗ length (list)) ≮ n1 )) → (nthcdr (n1 , repeat-list (list, n2 ))

= repeat-list (list, n2 − (n1 ÷ length (list))))

Theorem: length-make-length length (make-length (n, list, fill)) = fix (n)

Theorem: member-expanded ((tk ∈ pts) ∧ expanded-tasksp (pts, bigp)) → ((cadr (tk) mod bigp) = 0)

Theorem: firstn-length-list firstn (length (x), x) = plist (x)

Theorem: firstn-repeat-list (((n1 mod length (list)) = 0) ∧ ((n2 ∗ length (list)) ≮ n1 )) → (firstn (n1 , repeat-list (list, n2 ))

= repeat-list (list, n1 ÷ length (list)))

Theorem: lessp-remainder-special (((x mod z) = 0) ∧ ((y mod z) = 0)) → ((y < (x + z)) = ((z ≄ 0) ∧ (x ≮ y)))

Theorem: lessp-difference-special (((x mod z) = 0) ∧ ((y mod z) = 0)) → (((x − y) < z) = ((z ≄ 0) ∧ (y ≮ x)))

Theorem: occurrences-append occurrences (a, append (x, y)) = (occurrences (a, x) + occurrences (a, y))

Theorem: occurrences-repeat-list occurrences (v, repeat-list (list, n)) = (n ∗ occurrences (v, list))

Theorem: occurrences-make-length occurrences (v, make-length (size, list, fill)) = if size < length (list) then occurrences (v, firstn (size, list))

elseif v = fill

then occurrences (v, list) + (size − length (list))

else occurrences (v, list) endif

Theorem: occurrences-repeat occurrences (x, repeat (n, y)) = if x = y then fix (n)

else 0 endif

Theorem: member-repeat (x ∈ repeat (n, v)) = ((0 < n) ∧ (x = v))

Theorem: member-substring-schedule (periodic-tasksp (z) ∧ expanded-tasksp (z, bigp) ∧ (v ≠ nil)) → ((v ∈ substring-schedule (z, bigp)) ↔ assoc (v, z))

Theorem: member-car-x-x (car (x) ∈ x) = listp (x)

Theorem: occurrences-substring-schedule ((tk ∈ pts) ∧ (0 < bigp) ∧ periodic-tasksp (pts) ∧ expanded-tasksp (pts, bigp)) → (occurrences (car (tk), substring-schedule (pts, bigp))

= ((bigp ∗ caddr (tk)) ÷ cadr (tk)))

Theorem: times-quotient-quotient-special (((x mod bigp) = 0) ∧ (((bigp ∗ y) mod x) = 0) ∧ (0 < bigp)) → (((x ÷ bigp) ∗ ((bigp ∗ y) ÷ x)) = fix (y))

Theorem: good-schedule-periodic-task-requests ((tk ∈ pts) ∧ periodic-tasksp (pts) ∧ expanded-tasksp (pts, bigp) ∧ (0 < bigp) ∧ (n2 ≮ n1 ) ∧ (n2 ∈ N) ∧ (n1 ∈ N)

∧ ((cadr (tk) mod bigp) ≃ 0) ∧ (((bigp ∗ caddr (tk)) mod cadr (tk)) ≃ 0) ∧ ((n1 mod bigp) ≃ 0) ∧ ((n1 mod cadr (tk)) ≃ 0) ∧ ((n2 mod bigp) ≃ 0) ∧ ((n2 mod big-period (pts)) ≃ 0) ∧ ((n2 mod cadr (tk)) ≃ 0) ∧ (bigp ≮ length (substring-schedule (pts, bigp)))) → good-schedule (repeat-list (make-length (bigp,

substring-schedule (pts, bigp), nil),

n2 ÷ bigp), periodic-task-requests (tk, n1 , n2 ))

Theorem: member-sublistp (sublistp (x, y) ∧ (e ∈ x)) → (e ∈ y)

Theorem: member-expanded-tasksp-means (expanded-tasksp (pts, bigp) ∧ (tk ∈ pts)) → (((cadr (tk) mod bigp) = 0)

∧ (((bigp ∗ caddr (tk)) mod cadr (tk)) = 0))

Theorem: remainder-period-if-remainder-big-period (periodic-tasksp (pts) ∧ (tk ∈ pts) ∧ ((n mod big-period (pts)) ≃ 0)) → ((n mod cadr (tk)) = 0)

Theorem: good-simple-schedule-sublist ((bigp ≮ length (substring-schedule (pts2 , bigp))) ∧ (n1 = 0) ∧ sublistp (pts1 , pts2 ) ∧ periodic-tasksp (pts2 ) ∧ expanded-tasksp (pts2 , bigp) ∧ (0 < bigp) ∧ (n2 ∈ N) ∧ ((n2 mod bigp) ≃ 0) ∧ ((n2 mod big-period (pts2 )) ≃ 0)) → good-schedule (make-simple-schedule (pts2 , bigp, n2 ),

periodic-tasks-requests (pts1 , n1 , n2 ))

Theorem: sublistp-x-x sublistp (x, x)

Theorem: periodic-tasks-requests-simple (n1 ≮ n2 ) → (periodic-tasks-requests (pts, n1 , n2 ) = nil)

;; big theorem

Theorem: good-simple-schedule ((bigp ≮ length (substring-schedule (pts, bigp))) ∧ periodic-tasksp (pts) ∧ expanded-tasksp (pts, bigp) ∧ (0 < bigp) ∧ ((n mod bigp) ≃ 0) ∧ ((n mod big-period (pts)) ≃ 0)) → good-schedule (make-simple-schedule (pts, bigp, n),

periodic-tasks-requests (pts, 0, n))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: expand-tasks (pts, bigp) = if listp (pts)

then cons (list (caar (pts), bigp ∗ cadar (pts), bigp ∗ caddar (pts)),

expand-tasks (cdr (pts), bigp))

else nil endif

;;;; expanded-tasksp identifies expand-tasks

Theorem: expanded-tasksp-expand-task-helper (((x mod big-period (pts1 )) = 0) ∧ (x ≄ 0)) → expanded-tasksp (expand-tasks (pts1 , x), x)

Theorem: zerop-big-period periodic-tasksp (pts) → (0 < big-period (pts))

Theorem: expanded-tasksp-expand-task periodic-tasksp (pts) → expanded-tasksp (expand-tasks (pts, big-period (pts)), big-period (pts))

Theorem: assoc-expand-tasks periodic-tasksp (x) → (assoc (v, expand-tasks (x, n)) ↔ assoc (v, x))

Theorem: periodic-tasksp-expand-tasks periodic-tasksp (pts) → (periodic-tasksp (expand-tasks (pts, n))

= ((n ≄ 0) ∨ (¬ listp (pts))))

Definition: non-overlapping-requests3 (request, request-list) = if listp (request-list)

then ((car (request) ≠ caar (request-list))

∨ (cadr (request) ≮ caddar (request-list))

∨ (cadar (request-list) ≮ caddr (request))

∨ (car (request-list) = request))

∧ non-overlapping-requests3 (request, cdr (request-list)) else t endif

Definition: non-overlapping-requests2 (r1 , r2 ) = if listp (r1 )

then non-overlapping-requests3 (car (r1 ), r2 )

∧ non-overlapping-requests2 (cdr (r1 ), r2 ) else t endif

Definition: non-overlapping-requests (r) = non-overlapping-requests2 (r, r)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: double-cdr-induction (a, b) = if listp (a) then double-cdr-induction (cdr (a), cdr (b))

else t endif

Theorem: plist-firstn plist (firstn (n, l)) = firstn (n, l)

Theorem: cons-nth-nthcdr (n < length (l)) → (cons (nth (n, l), nthcdr (n, cdr (l))) = nthcdr (n, l))

Theorem: equal-append (append (a, b) = y) = if y ≃ nil then (a ≃ nil) ∧ (b = y)

else (length (y) ≮ length (a)) ∧ (firstn (length (a), y) = plist (a)) ∧ (nthcdr (length (a), y) = b) endif

Theorem: replace-nth-replace-nth (fix (i) ≠ fix (j )) → (replace-nth (i, x, replace-nth (j , y, l))

= replace-nth (j , y, replace-nth (i, x, l)))

Theorem: replace-nth-idempotent (fix (i) = fix (j )) → (replace-nth (i, x, replace-nth (j , y, l)) = replace-nth (i, x, l))

Theorem: member-nth (n < length (list)) → (nth (n, list) ∈ list)

Theorem: swap-commutative swap (j , i, s) = swap (i, j , s)

Theorem: member-replace-nth (x ∉ l) → ((x ∈ replace-nth (i, v, l))

= ((x = v) ∨ ((x = 0) ∧ (length (l) < i))))

Theorem: occurrences-replace-nth occurrences (x, replace-nth (n, v, list)) = ((occurrences (x, list)

+ if v = x then 1 else 0 endif

+ if x = 0 then n − length (list)

else 0 endif) − if (x = nth (n, list)) ∧ (n < length (list)) then 1

else 0 endif)

Theorem: nthcdr-1 nthcdr (1, x) = cdr (x)

Theorem: nlistp-nthcdr (¬ listp (s)) → (nthcdr (n, s)

= if n ≃ 0 then s else 0 endif)

Theorem: nthcdr-firstn-plus (nthcdr (n, firstn (n + x, s)) = firstn (x, nthcdr (n, s))) ∧ (nthcdr (n, firstn (x + n, s)) = firstn (x, nthcdr (n, s)))

Theorem: cdr-nthcdr-cons cdr (nthcdr (x, cons (a, b))) = nthcdr (x, b)

Definition: add1-sub1-induct (a, b) = if b ≃ 0 then t

else add1-sub1-induct (1 + a, b − 1) endif

Theorem: nth-nthcdr nth (n1 , nthcdr (n2 , s)) = nth (n1 + n2 , s)

Theorem: nthcdr-nthcdr nthcdr (n1 , nthcdr (n2 , s)) = nthcdr (n1 + n2 , s)

Theorem: equal-append-a-append-a (append (a, x) = append (a, y)) = (x = y)

Theorem: nthcdr-replace-nth nthcdr (n, replace-nth (i, v, l)) = if i < n then nthcdr (n, l)

else replace-nth (i − n, v, nthcdr (n, l)) endif

Theorem: firstn-replace-nth firstn (n, replace-nth (i, v, l)) = if i < n then replace-nth (i, v, firstn (n, l))

else firstn (n, l) endif

Theorem: cdr-firstn-cons cdr (firstn (n, cons (a, b))) = if n ≃ 0 then 0

else firstn (n − 1, b) endif

Theorem: nth-firstn nth (n, firstn (n2 , s)) = if n < n2 then nth (n, s)

else 0 endif

Theorem: firstn-cons firstn (n, cons (a, b)) = if n ≃ 0 then nil

else cons (a, firstn (n − 1, b)) endif

Definition: double-sub1-induction (a, b) = if a ≃ 0 then t

else double-sub1-induction (a − 1, b − 1) endif

Theorem: equal-repeat-repeat (repeat (n, v) = repeat (n2 , v2 )) = ((fix (n) = fix (n2 )) ∧ ((v = v2 ) ∨ (n ≃ 0)))

Theorem: firstn-too-big (length (x) < n) → (firstn (n, x) = append (x, repeat (n − length (x), 0)))

Theorem: firstn-firstn firstn (a, firstn (b, x)) = if b < a then append (firstn (b, x), repeat (a − b, 0))

else firstn (a, x) endif

Theorem: plist-repeat plist (repeat (n, x)) = repeat (n, x)

Theorem: firstn-1 firstn (1, s) = list (car (s))

Theorem: nthcdr-cons-firstn nthcdr (w, cons (a, firstn (w + x, b))) = if w ≃ 0 then cons (a, firstn (x, b))

else nthcdr (w − 1, firstn (w + x, b)) endif

Theorem: nthcdr-sub1-firstn-plus (w ≄ 0) → (nthcdr (w − 1, firstn (w + x, b)) = firstn (1 + x, nthcdr (w − 1, b)))

Theorem: nthcdr-repeat nthcdr (n1 , repeat (n2 , x)) = if n2 < n1 then 0

else repeat (n2 − n1 , x) endif

Theorem: firstn-nlistp (l ≃ nil) → (firstn (n, l) = repeat (n, 0))

Definition: member-nth-firstn-induction (i, y, s) = if i ≃ 0 then t

else member-nth-firstn-induction (i − 1, y − 1, cdr (s)) endif

Theorem: member-nth-firstn (i < j ) → (nth (i, s) ∈ firstn (j , s))

Theorem: member-car-firstn (car (x) ∈ firstn (n, x)) = (n ≄ 0)

Theorem: member-nth-firstn-nthcdr ((i ≮ y) ∧ (i < (x + y))) → (nth (i, s) ∈ firstn (x, nthcdr (y, s)))

Theorem: non-overlapping-requests-means non-overlapping-requests (r) → non-overlapping-requests3 (car (r), cdr (r))

Theorem: non-overlapping-requests2-cdr non-overlapping-requests2 (r1 , r2 ) → non-overlapping-requests2 (cdr (r1 ), cdr (r2 ))

Theorem: non-overlapping-requests-cdr non-overlapping-requests (r) → non-overlapping-requests (cdr (r))

Theorem: member-firstn-only-if-member (x ∉ l) → ((x ∈ firstn (n, l)) = ((x = 0) ∧ (length (l) < n)))

Theorem: member-nthcdr-only-if-member (x ∉ l) → (x ∉ nthcdr (n, l))

Theorem: nth-replace-nth nth (i, replace-nth (j , v, l)) = if fix (i) = fix (j ) then v

else nth (i, l) endif

Theorem: member-x-firstn-cons-x (x ∈ firstn (n, cons (x, y))) = (0 < n)

Definition: cars-non-nil-litatoms (list) = if listp (list)

then litatom (caar (list)) ∧ (caar (list) ≠ nil) ∧ cars-non-nil-litatoms (cdr (list))

else t endif

Theorem: swap-preserves-good-schedule (non-overlapping-requests3 (task-request-a, r) ∧ non-overlapping-requests3 (task-request-b, r) ∧ cars-non-nil-litatoms (r) ∧ (i ≮ cadr (task-request-a)) ∧ (j ≮ cadr (task-request-a)) ∧ (i < caddr (task-request-a)) ∧ (j < caddr (task-request-a)) ∧ (i ≮ cadr (task-request-b)) ∧ (j ≮ cadr (task-request-b)) ∧ (i < caddr (task-request-b)) ∧ (j < caddr (task-request-b)) ∧ (nth (i, s) = car (task-request-a)) ∧ (nth (j , s) = car (task-request-b)) ∧ litatom (nth (i, s)) ∧ litatom (nth (j , s)) ∧ good-schedule (s, r)) → good-schedule (swap (i, j , s), r)

; return task request corresponding to task at time

Definition: corresponding-request (task, time, r) = if listp (r)

then if (caar (r) = task) ∧ (time ≮ cadar (r))

∧ (time < caddar (r)) then car (r) else corresponding-request (task, time, cdr (r)) endif

else f endif

Definition: all-non-nil-corresponding (s, r, time) = if time < length (s)

then (corresponding-request (nth (time, s), time, r) ∨ (nth (time, s) = nil)) ∧ all-non-nil-corresponding (s, r, 1 + time)

else t endif

Theorem: non-overlapping-requests2-member (non-overlapping-requests2 (r1 , r2 ) ∧ sublistp (r1 , r2 ) ∧ (e ∈ r1 )) → non-overlapping-requests3 (e, r2 )

Theorem: non-overlapping-requests3-member (non-overlapping-requests (r) ∧ (e ∈ r)) → non-overlapping-requests3 (e, r)

Theorem: member-corresponding-request-nth corresponding-request (task, time, r) → (corresponding-request (task, time, r) ∈ r)

Definition: all-litatoms (list) = if listp (list) then litatom (car (list)) ∧ all-litatoms (cdr (list))

else t endif

Theorem: litatom-nth all-litatoms (s) → (litatom (nth (i, s)) = (i < length (s)))

Theorem: lessp-first-instance-s (first-instance (time, task, s) < length (s)) = listp (s)

Theorem: member-nthcdr-from-cdr ((x ∉ nthcdr (n, cdr (s))) ∧ (n < length (s))) → ((x ∈ nthcdr (n, s)) = (x = nth (n, s)))

Theorem: listp-nthcdr listp (nthcdr (n, x)) = (n < length (x))

Theorem: car-nthcdr car (nthcdr (n, l)) = if n < length (l) then nth (n, l)

else 0 endif Theorem: nth-first-instance-simple (nth (first-instance (n, x, s), s) = x) = ((x ∈ nthcdr (n, s)) ∨ (car (s) = x))

Theorem: equal-occurrences-firstn-nthcdr (n1 < n2 ) → ((occurrences (x, firstn (n1 , nthcdr (n, list)))

= occurrences (x, firstn (n2 , nthcdr (n, list)))) = (x ∉ firstn (n2 − n1 , nthcdr (n + n1 , list))))

Theorem: member-firstn-lessp ((x ∈ firstn (n1 , l)) ∧ (n2 ≮ n1 )) → (x ∈ firstn (n2 , l))

Theorem: member-least-deadline (least-deadline (r) ∈ r) = listp (r)

Theorem: unfulfilled-task-later-in-good-schedule (good-schedule (s, r) ∧ all-litatoms (s) ∧ cars-non-nil-litatoms (r) ∧ (tr ∈ unfulfilled (element, s, active-task-requests (element, r)))) → (car (tr) ∈ nthcdr (element, s))

Theorem: car-corresponding-request corresponding-request (task, time, r) → (car (corresponding-request (task, time, r)) = task)

Theorem: active-task-has-later-deadline (tr ∈ active-task-requests (element, r)) → (element < caddr (tr))

Theorem: sublistp-unfulfilled sublistp (unfulfilled (e, s, r), r)

Theorem: least-deadline-has-later-deadline listp (unfulfilled (element, s, active-task-requests (element, r))) → ((element < caddr (least-deadline (unfulfilled (element,

s,

active-task-requests (element,

r)))))

= t)

Theorem: active-task-hasnt-earlier-start (tr ∈ active-task-requests (element, r)) → (element ≮ cadr (tr))

Theorem: lessp-corresponding-request-deadline corresponding-request (nth (element, s), element, r) → ((element < caddr (corresponding-request (nth (element, s), element, r)))

= t)

Theorem: least-deadline-hasnt-earlier-start listp (unfulfilled (element, s, active-task-requests (element, r))) → ((element < cadr (least-deadline (unfulfilled (element,

s,

active-task-requests (element,

r)))))

= f)

Theorem: lessp-corresponding-request-start corresponding-request (x, time, r) → (time ≮ cadr (corresponding-request (x, time, r)))

Theorem: lessp-corresponding-request-deadline-linear corresponding-request (x, time, r) → (time < caddr (corresponding-request (x, time, r)))

Theorem: sublistp-active-task-requests sublistp (active-task-requests (time, r), r)

Theorem: member-means-all-cars-not-litatoms ((x ∈ r) ∧ (¬ litatom (car (x)))) → (¬ cars-non-nil-litatoms (r))

Theorem: member-least-deadline-unfulfilled cars-non-nil-litatoms (r) → ((least-deadline (unfulfilled (element,

s,

active-task-requests (element, r)))

∈ r)

= listp (unfulfilled (element, s, active-task-requests (element, r))))

Theorem: not-numberp-corresponding (element ∉ N) → (corresponding-request (x, element, r) = corresponding-request (x, 0, r))

Theorem: member-firstn-means-lessp-first-instance (v ∈ firstn (n − time, nthcdr (time, s))) → ((first-instance (time, v, s) < n) = t)

Theorem: first-instance-member-unfulfilled-not-past-deadline (good-schedule (s, r) ∧ (tr ∈ unfulfilled (element, s, active-task-requests (element, r)))) → ((first-instance (element, car (tr), s) < caddr (tr)) = t)

Theorem: lessp-firstn-instance-time (time ≮ n) → ((first-instance (time, v, s) < n)

= ((v ∉ nthcdr (time, s)) ∧ (n ≄ 0)))

Theorem: first-instance-member-unfulfilled-not-before-start (good-schedule (s, r) ∧ cars-non-nil-litatoms (r) ∧ (tr ∈ unfulfilled (element, s, active-task-requests (element, r)))) → ((first-instance (element, car (tr), s) < cadr (tr)) = f)

Theorem: member-corresponding-request (good-schedule (s, r) ∧ corresponding-request (nth (element, s), element, r)) → (corresponding-request (nth (element, s), element, r)

∈ unfulfilled (element, s, active-task-requests (element, r)))

Definition: member-deadline-induct (x, l) = if listp (l)

then if listp (cdr (l))

then if caddar (l) < caddadr (l) then if x = cadr (l)

then member-deadline-induct (car (l),

cons (car (l), cddr (l)))

else member-deadline-induct (x,

cons (car (l), cddr (l))) endif

elseif x = car (l)

then member-deadline-induct (cadr (l), cons (cadr (l), cddr (l))) else member-deadline-induct (x, cons (cadr (l), cddr (l))) endif

else t endif else t endif

Theorem: member-deadline-not-less-than-least-deadline (x ∈ l) → ((caddr (x) < caddr (least-deadline (l))) = f)

Theorem: first-instance-member-unfulfilled-not-past-deadline-better (good-schedule (s, r) ∧ (tr ∈ unfulfilled (element, s, active-task-requests (element, r))) ∧ (caddr (tr2 ) ≮ caddr (tr))) → ((first-instance (element, car (tr), s) < caddr (tr2 )) = t)

Theorem: non-overlapping-requests3-simple (cars-non-nil-litatoms (r) ∧ (¬ listp (tr))) → non-overlapping-requests3 (tr, r)

Theorem: swap-preserves-good-schedule-simple (non-overlapping-requests3 (task-request, r) ∧ cars-non-nil-litatoms (r) ∧ (i ≮ cadr (task-request)) ∧ (j ≮ cadr (task-request))

∧ (i < caddr (task-request)) ∧ (j < caddr (task-request)) ∧ (nth (j , s) = car (task-request)) ∧ (nth (i, s) = nil) ∧ litatom (nth (j , s)) ∧ good-schedule (s, r)) → good-schedule (swap (i, j , s), r)

Theorem: nth-too-big (i ≮ length (s)) → (nth (i, s) = 0)

Theorem: not-corresponding-request-means-nil (all-non-nil-corresponding (s, r, n) ∧ (¬ corresponding-request (nth (i, s), i, r)) ∧ (i ≮ n)) → (nth (i, s)

= if i < length (s) then nil else 0 endif)

;; takes 1/2 hr without disable-theory t

Theorem: make-element-edf-preserves-good-schedule ((element < length (s)) ∧ non-overlapping-requests (r) ∧ cars-non-nil-litatoms (r) ∧ all-litatoms (s) ∧ all-non-nil-corresponding (s, r, 0) ∧ good-schedule (s, r)) → good-schedule (make-element-edf (s, r, element), r)

Theorem: all-litatoms-replace-nth all-litatoms (replace-nth (n, v, x)) = (litatom (v)

∧ (length (x) ≮ n)

∧ all-litatoms (firstn (n, x))

∧ all-litatoms (nthcdr (1 + n, x)))

Theorem: all-litatoms-nthcdr all-litatoms (s) → all-litatoms (nthcdr (n, s))

Theorem: all-litatoms-repeat all-litatoms (repeat (n, v)) = ((n ≃ 0) ∨ litatom (v))

Theorem: all-litatoms-firstn all-litatoms (s) → (all-litatoms (firstn (n, s)) = (length (s) ≮ n))

Theorem: make-element-edf-preserves-all-litatoms ((element < length (s)) ∧ non-overlapping-requests (r) ∧ cars-non-nil-litatoms (r) ∧ all-litatoms (s) ∧ all-non-nil-corresponding (s, r, 0) ∧ good-schedule (s, r)) → all-litatoms (make-element-edf (s, r, element))

Theorem: equal-lessp-sub1x-y-x-y (((x − 1) < y) = (x < y)) = ((x ≃ 0) ∨ (fix (x) ≠ fix (y)))

Theorem: all-non-nil-corresponding-replace-simple (all-non-nil-corresponding (s, r, n) ∧ (n1 < length (s))) → (all-non-nil-corresponding (replace-nth (n1 , v, s), r, n)

= (corresponding-request (v, n1 , r) ∨ (v = nil) ∨ (n1 < n)))

Theorem: car-replace-nth car (replace-nth (n, v, s)) = if n ≃ 0 then v

else car (s) endif

Theorem: not-corresponding-request-means ((¬ corresponding-request (v1 , n1 , r)) ∧ (v1 ≠ nil) ∧ (nth (n1 , s) = v1 ) ∧ (n1 < length (s)) ∧ (n1 ≮ n)) → (¬ all-non-nil-corresponding (s, r, n))

Theorem: all-non-nil-corresponding-cons all-non-nil-corresponding (cons (a, b), r, n) → (all-non-nil-corresponding (cons (x, b), r, n)

= ((x = nil) ∨ corresponding-request (x, 0, r) ∨ (n ≄ 0)))

Theorem: all-non-nil-corresponding-replace-replace (all-non-nil-corresponding (s, r, n) ∧ (n1 < length (s)) ∧ (n2 < length (s))) → (all-non-nil-corresponding (replace-nth (n2 , v2 , replace-nth (n1 , v1 , s)),

r, n)

= ((corresponding-request (v1 , n1 , r)

∨ (v1 = nil)

∨ (n1 < n)

∨ (fix (n1 ) = fix (n2 )))

∧ (corresponding-request (v2 , n2 , r) ∨ (v2 = nil)

∨ (n2 < n))))

Theorem: nth-first-instance (v ∈ nthcdr (time, s)) → (nth (first-instance (time, v, s), s) = v)

Theorem: car-corresponding-request-better car (corresponding-request (v, n, r)) = if corresponding-request (v, n, r) then v

else 0 endif

Theorem: equivalent-corresponding-requests (non-overlapping-requests3 (corresponding-request (v, n, r), r) ∧ (n1 ≮ cadr (corresponding-request (v, n, r))) ∧ (n1 < caddr (corresponding-request (v, n, r)))) → (corresponding-request (v, n1 , r) = corresponding-request (v, n, r))

Theorem: lessp-n-1 (n < 1) = (n ≃ 0)

Theorem: member-corresponding-request-simplify cars-non-nil-litatoms (r) → ((corresponding-request (v, n, r) ∈ r)

↔ corresponding-request (v, n, r))

Theorem: member-corresponding-request2 (all-non-nil-corresponding (s, r, n1 ) ∧ (n ≮ n1 ) ∧ (n < length (s)) ∧ cars-non-nil-litatoms (r) ∧ (nth (n, s) ≠ nil)) → (corresponding-request (nth (n, s), n, r) ∈ r)

;;; the best thereom would be about make-element-edf's preserving
;;; all-non-nil-corresponding.  But we'll punt on that for now,
;;; and use the fact that periodic request schedules are "full"
;;; and thus all reasonable schedules have corresponding requests

Definition: all-nils-or-cars (s, r) = if listp (s)

then ((car (s) = nil) ∨ assoc (car (s), r)) ∧ all-nils-or-cars (cdr (s), r)

else t endif Theorem: corresponding-request-append corresponding-request (v, n, append (r1 , r2 )) ↔ (corresponding-request (v, n, r1 ) ∨ corresponding-request (v, n, r2 ))

Theorem: corresponding-request-different-name (car (pt) ≠ tk) → (¬ corresponding-request (tk, n, periodic-task-requests (pt, n1 , n2 )))

Theorem: corresponding-request-periodic-task (periodic-taskp (pt) ∧ ((n1 mod cadr (pt)) = 0) ∧ (n < n2 ) ∧ (n ≮ n1 )) → (corresponding-request (tk, n, periodic-task-requests (pt, n1 , n2 ))

↔ (car (pt) = tk))

Theorem: all-nils-or-cars-nlistp (¬ listp (x)) → (all-nils-or-cars (l, x) = (plist (l) = repeat (length (l), nil)))

Theorem: assoc-nth-pts ((n < length (s)) ∧ all-nils-or-cars (s, pts) ∧ (nth (n, s) ≠ nil)) → assoc (nth (n, s), pts)

Theorem: corresponding-request-periodic-tasks (assoc (v, pts) ∧ periodic-tasksp (pts) ∧ ((n1 mod cadr (assoc (v, pts))) = 0) ∧ (n < n2 ) ∧ (n ≮ n1 )) → corresponding-request (v, n, periodic-tasks-requests (pts, n1 , n2 ))

Theorem: all-nils-or-cars-replace-nth (all-nils-or-cars (s, r) ∧ (n < length (s))) → (all-nils-or-cars (replace-nth (n, v, s), r)

= ((v = nil) ∨ assoc (v, r)))

Theorem: all-non-nil-corresponding-periodic-requests (all-nils-or-cars (s, pts) ∧ periodic-tasksp (pts) ∧ (fix (n1 ) = length (s))) → all-non-nil-corresponding (s, periodic-tasks-requests (pts, 0, n1 ), n)

Definition: double-sub1-cdr-induct (n1 , n2 , s) = if n2 ≃ 0 then t

else double-sub1-cdr-induct (n1 − 1, n2 − 1, cdr (s)) endif Theorem: all-nils-or-cars-replace-nth-replace-nth (all-nils-or-cars (s, r) ∧ (n < length (s)) ∧ (n2 < length (s))) → (all-nils-or-cars (replace-nth (n, v, replace-nth (n2 , v2 , s)), r)

= (((v = nil) ∨ assoc (v, r)) ∧ ((v2 = nil)

∨ assoc (v2 , r)

∨ (fix (n) = fix (n2 )))))

Theorem: lessp-0-length-means-listp (n < length (l)) → listp (l)

Theorem: all-nils-or-cars-make-element-edf (all-nils-or-cars (s, pts) ∧ listp (s) ∧ (n < length (s))) → all-nils-or-cars (make-element-edf (s, pts1 , n), pts)

Theorem: make-schedule-edf-preserves-good-schedule (non-overlapping-requests (r) ∧ cars-non-nil-litatoms (r) ∧ all-litatoms (s) ∧ all-non-nil-corresponding (s, r, 0) ∧ all-nils-or-cars (s, pts) ∧ good-schedule (s, r) ∧ (r = periodic-tasks-requests (pts, 0, length (s))) ∧ periodic-tasksp (pts)) → good-schedule (make-schedule-edf (s, r, n), r)

;;;;;;;;;;;

Theorem: non-overlapping-requests2-append non-overlapping-requests2 (append (a, b), r) = (non-overlapping-requests2 (a, r) ∧ non-overlapping-requests2 (b, r))

Theorem: all-nils-or-cars-plist all-nils-or-cars (plist (a), pts) = all-nils-or-cars (a, pts)

Theorem: all-nils-or-cars-append all-nils-or-cars (append (a, b), pts) = (all-nils-or-cars (a, pts) ∧ all-nils-or-cars (b, pts))

Theorem: all-nils-or-cars-repeat-list all-nils-or-cars (repeat-list (l, n), pts) = ((n ≃ 0) ∨ all-nils-or-cars (l, pts))

Theorem: all-nils-or-cars-make-length all-nils-or-cars (make-length (n, l, nil), pts) = if n < length (l) then all-nils-or-cars (firstn (n, l), pts)

else all-nils-or-cars (l, pts) endif Theorem: all-nils-or-cars-repeat all-nils-or-cars (repeat (n, v), pts) = ((v = nil) ∨ assoc (v, pts) ∨ (n ≃ 0))

Theorem: all-nils-or-cars-substring-schedule cars-non-nil-litatoms (pts) → all-nils-or-cars (substring-schedule (pts, n), pts)

Theorem: all-nils-or-cars-firstn (all-nils-or-cars (l, pts) ∧ (n < length (l))) → all-nils-or-cars (firstn (n, l), pts)

Theorem: all-nils-or-cars-make-simple-schedule cars-non-nil-litatoms (pts) → all-nils-or-cars (make-simple-schedule (pts, bigp, n), pts)

Theorem: length-make-simple-schedule ((n mod bigp) = 0) → (length (make-simple-schedule (pts, bigp, n)) = fix (n))

Theorem: periodic-tasksp-means-cars-non-nil-litatoms periodic-tasksp (pts) → cars-non-nil-litatoms (pts)

Theorem: all-litatoms-append all-litatoms (append (a, b)) = (all-litatoms (a) ∧ all-litatoms (b))

Theorem: all-litatoms-repeat-list all-litatoms (repeat-list (l, n)) = ((n ≃ 0) ∨ all-litatoms (l))

Theorem: all-litatoms-make-length all-litatoms (make-length (n, l, v)) = if length (l) < n then all-litatoms (l) ∧ litatom (v)

else all-litatoms (firstn (n, l)) endif

Theorem: all-litatoms-substring-schedule cars-non-nil-litatoms (pts) → all-litatoms (substring-schedule (pts, bigp))

Theorem: all-litatoms-make-simple-schedule cars-non-nil-litatoms (pts) → all-litatoms (make-simple-schedule (pts, bigp, n))

Theorem: cars-non-nil-litatoms-periodic-tasks cars-non-nil-litatoms (pts) → cars-non-nil-litatoms (periodic-tasks-requests (pts, n1 , n2 ))

Definition: value-all-cars (v, list) = if listp (list)

then (caar (list) = v) ∧ value-all-cars (v, cdr (list))

else t endif

Theorem: non-overlapping-requests3-append non-overlapping-requests3 (v, append (r1 , r2 )) = (non-overlapping-requests3 (v, r1 ) ∧ non-overlapping-requests3 (v, r2 ))

Theorem: value-all-cars-periodic-task-requests value-all-cars (x, periodic-task-requests (req, n1 , n2 )) = ((¬ listp (periodic-task-requests (req, n1 , n2 ))) ∨ (x = car (req)))

Theorem: non-overlapping-requests2-value-all-cars (value-all-cars (v, list) ∧ (¬ assoc (v, r)) ∧ cars-non-nil-litatoms (r)) → (non-overlapping-requests2 (r, append (list, r2 ))

= non-overlapping-requests2 (r, r2 ))

Theorem: assoc-append (v ≠ 0) → (assoc (v, append (x, y)) ↔ (assoc (v, x) ∨ assoc (v, y)))

Theorem: assoc-periodic-task-requests (v ≠ car (req)) → (¬ assoc (v, periodic-task-requests (req, n1 , n2 )))

Theorem: assoc-periodic-tasks-requests ((v ≠ 0) ∧ (¬ assoc (v, list))) → (¬ assoc (v, periodic-tasks-requests (list, n1 , n2 )))

Theorem: non-overlapping-requests2-append-arg2 ((¬ assoc (car (req), list)) ∧ (car (req) ≠ 0) ∧ cars-non-nil-litatoms (list)) → (non-overlapping-requests2 (periodic-tasks-requests (list, n1 , n2 ),

append (periodic-task-requests (req, n3 , n4 ), y))

= non-overlapping-requests2 (periodic-tasks-requests (list, n1 , n2 ), y))

Theorem: non-overlapping-requests3-periodic-task (n1 ≮ end) → non-overlapping-requests3 (list (tk, start, end, duration),

periodic-task-requests (pt, n1 , n2 ))

Theorem: non-overlapping-requests3-task-name-difference (car (pt) ≠ car (req)) → non-overlapping-requests3 (req, periodic-task-requests (pt, n1 , n2 ))

Theorem: non-overlapping-requests3-name-difference (litatom (car (req)) ∧ (¬ assoc (car (req), list))) → non-overlapping-requests3 (req, periodic-tasks-requests (list, n1 , n2 ))

Theorem: non-overlapping-requests2-cons-too-big (n1 ≮ caddr (req)) → (non-overlapping-requests2 (periodic-task-requests (tr, n1 , n2 ),

cons (req, r)) = non-overlapping-requests2 (periodic-task-requests (tr, n1 , n2 ), r))

Theorem: non-overlapping-requests2-periodic-task (¬ assoc (car (req), x)) → non-overlapping-requests2 (periodic-task-requests (req, n1 , n2 ),

append (periodic-task-requests (req, n1 , n2 ), periodic-tasks-requests (x, n3 , n4 )))

Theorem: non-overlapping-requests2-periodic-tasks periodic-tasksp (pts) → non-overlapping-requests2 (periodic-tasks-requests (pts, 0, n),

periodic-tasks-requests (pts, 0, n))

Theorem: non-overlapping-requests-periodic-tasks-requests periodic-tasksp (pts) → non-overlapping-requests (periodic-tasks-requests (pts, 0, n))

;;;; major lemma

Theorem: edf-schedule-good-for-expanded ((bigp ≮ length (substring-schedule (pts, bigp))) ∧ periodic-tasksp (pts) ∧ expanded-tasksp (pts, bigp) ∧ (0 < bigp) ∧ ((n mod bigp) ≃ 0) ∧ ((n mod big-period (pts)) ≃ 0)) → good-schedule (make-schedule-edf (make-simple-schedule (pts, bigp, n),

periodic-tasks-requests (pts, 0, n), 0),

periodic-tasks-requests (pts, 0, n))

;;;;;;;;;;;;;;;

Definition: every-nth (n, list) = if n ≃ 0 then nil

elseif listp (list) then cons (car (list), every-nth (n, nthcdr (n, list))) else nil endif Definition: expand-tasks-requests (tasks-requests, n) = if listp (tasks-requests)

then cons (list (caar (tasks-requests), n ∗ cadar (tasks-requests), n ∗ caddar (tasks-requests), n ∗ cadddar (tasks-requests)),

expand-tasks-requests (cdr (tasks-requests), n))

else nil endif

Theorem: expand-tasks-requests-append expand-tasks-requests (append (a, b), n) = append (expand-tasks-requests (a, n), expand-tasks-requests (b, n))

Theorem: listp-append listp (append (a, b)) = (listp (a) ∨ listp (b))

Theorem: listp-expand-tasks-requests listp (expand-tasks-requests (l, n)) = listp (l)

Theorem: listp-task-requests listp (periodic-task-requests (task, n1 , n2 )) = ((n1 < n2 ) ∧ periodic-taskp (task))

Theorem: length-expand-tasks-requests length (expand-tasks-requests (l, n)) = length (l)

Theorem: different-lengths-mean-different (x = y) → (length (x) = length (y))

Theorem: equal-nthcdr-x-x (nthcdr (n, x) = x) = ((n ≃ 0) ∨ (x = 0))

Definition: length-periodic-task-request-induct (n1 , period, bigp, n2 ) = if 0 < (bigp ∗ period)

then if n1 < n2

then length-periodic-task-request-induct (n1 + (bigp ∗ period), period, bigp, n2 )

else t endif else t endif Theorem: length-periodic-task-requests ((0 < bigp) ∧ (0 < period) ∧ ((n1 mod bigp) = 0) ∧ ((n2 mod bigp) = 0)) → (length (periodic-task-requests (list (name, bigp ∗ period, duration),

n1 , n2 )) = length (periodic-task-requests (list (name, period, duration),

n1 ÷ bigp,

n2 ÷ bigp)))

Theorem: plist-expand-tasks-requests plist (expand-tasks-requests (task, n)) = expand-tasks-requests (task, n)

Theorem: equal-plist-nil (plist (l) = nil) = (l ≃ nil)

Theorem: length-cons length (cons (a, b)) = (1 + length (b))

Theorem: cons-append-hack cons (a, append (b, c)) ≠ c

Theorem: equal-append-b-append-b (append (x, b) = append (y, b)) = (plist (x) = plist (y))

Theorem: plist-periodic-task-requests plist (periodic-task-requests (task, n1 , n2 )) = periodic-task-requests (task, n1 , n2 )

Theorem: lessp-equal-times-x-a-x ((a ∗ b) < a) = ((a ≄ 0) ∧ (b ≃ 0))

Theorem: periodic-task-requests-expand (periodic-taskp (pt) ∧ ((n1 mod bigp) = 0) ∧ ((n2 mod bigp) = 0) ∧ ((cadr (pt) mod bigp) = 0) ∧ ((caddr (pt) mod bigp) = 0) ∧ (n1 ∈ N)) → (periodic-task-requests (pt, n1 , n2 )

= expand-tasks-requests (periodic-task-requests (cons (car (pt),

cons (cadr (pt) ÷ bigp, cons (caddr (pt) ÷ bigp, cdddr (pt)))),

n1 ÷ bigp,

n2 ÷ bigp),

bigp))

Theorem: periodic-tasks-requests-expand (((n1 mod bigp) = 0) ∧ ((n2 mod bigp) = 0) ∧ periodic-tasksp (pts) ∧ (n1 ∈ N)) → (periodic-tasks-requests (expand-tasks (pts, bigp), n1 , n2 )

= expand-tasks-requests (periodic-tasks-requests (pts, n1 ÷ bigp,

n2 ÷ bigp),

bigp))

;;;;;

Definition: edf (lengthschedule, r) = if lengthschedule ≃ 0 then nil

else let s be edf (lengthschedule − 1, r) in let unfulfilled be unfulfilled (lengthschedule − 1,

s,

active-task-requests (lengthschedule − 1, r))

in

if listp (unfulfilled) then append (s,

list (name (least-deadline (unfulfilled))))

else append (s, list (nil)) endif endlet endlet endif

Theorem: length-edf-simple length (edf (n, r)) = fix (n)

Definition: valid-requests (reqs) = if listp (reqs)

then litatom (caar (reqs))

∧ (caar (reqs) ≠ nil) ∧ (cadar (reqs) ∈ N)

∧ (caddar (reqs) ∈ N) ∧ (0 < cadddar (reqs)) ∧ (cddddar (reqs) = nil) ∧ valid-requests (cdr (reqs))

else reqs = nil endif

Theorem: valid-requests-periodic-task valid-requests (periodic-task-requests (pt, n1 , n2 )) = ((n1 ∈ N) ∨ (n1 ≮ n2 ) ∨ (¬ periodic-taskp (pt)))

Theorem: valid-requests-append (plist (a) = a) → (valid-requests (append (a, b))

= (valid-requests (a) ∧ valid-requests (b)))

Theorem: valid-requests-periodic-tasks valid-requests (periodic-tasks-requests (pts, n1 , n2 )) = ((n1 ∈ N)

∨ (n1 ≮ n2 )

∨ (¬ periodic-tasksp (pts))

∨ (¬ listp (pts)))

Theorem: listp-active-task-requests-0 (n < n2 ) → (listp (active-task-requests (n, periodic-task-requests (pt, n1 , n2 )))

= (periodic-taskp (pt) ∧ (n ≮ n1 )))

Theorem: active-task-requests-append active-task-requests (n, append (r1 , r2 )) = append (active-task-requests (n, r1 ), active-task-requests (n, r2 ))

Theorem: listp-active-task-requests-0-multiple (n < n2 ) → (listp (active-task-requests (n, periodic-tasks-requests (pts, n1 , n2 )))

= (periodic-tasksp (pts) ∧ (n ≮ n1 ) ∧ listp (pts)))

Theorem: unfulfilled-0 valid-requests (r) → (unfulfilled (0, s, r) = r)

Theorem: valid-requests-active-task-requests valid-requests (r) → valid-requests (active-task-requests (n, r))

Theorem: lessp-0-length-means (0 < length (l)) = listp (l)

Theorem: listp-repeat listp (repeat (n, v)) = (n ≄ 0)

Theorem: length-repeat length (repeat (n, v)) = fix (n)

Theorem: plist-append plist (append (x, y)) = append (x, plist (y))

Theorem: length-plist length (plist (x)) = length (x)

Theorem: listp-plist listp (plist (x)) = listp (x)

Theorem: plist-edf-simple plist (edf (n, r)) = edf (n, r)

Theorem: firstn-repeat firstn (n1 , repeat (n2 , v)) = if n2 < n1 then append (repeat (n2 , v), repeat (n1 − n2 , 0))

else repeat (n1 , v) endif

Theorem: edf-simple-nlistp (¬ listp (r)) → (edf (n, r) = repeat (n, nil))

Theorem: make-schedule-edf-nlistp (¬ listp (r)) → (make-schedule-edf (s, r, n) = s)

Theorem: replace-nth-nlistp (l ≃ nil) → (replace-nth (n, v, l) = append (repeat (n, 0), cons (v, 0)))

Theorem: plist-replace-nth2 (plist (replace-nth (n, v, s)) = replace-nth (n, v, s)) = ((plist (s) = s) ∧ (n < length (s)))

Theorem: plist-swap (plist (swap (n1 , n2 , s)) = swap (n1 , n2 , s)) = ((plist (s) = s) ∧ (n1 < length (s)) ∧ (n2 < length (s)))

Theorem: plist-make-element-edf (plist (s) = s) → (plist (make-element-edf (s, r, n)) = make-element-edf (s, r, n))

Theorem: length-make-schedule-edf length (make-schedule-edf (s, r, n)) = length (s)

Theorem: equal-nthcdr-nthcdr-from-nthcdr-plus1 ((n < length (s1 )) ∧ (n < length (s2 )) ∧ (nthcdr (n, cdr (s1 )) = nthcdr (n, cdr (s2 )))) → ((nthcdr (n, s1 ) = nthcdr (n, s2 )) = (nth (n, s1 ) = nth (n, s2 )))

Theorem: lessp-first-instance2 first-instance (n2 , v, l) → (first-instance (n2 , v, l) ≮ n2 )

Theorem: nth-make-schedule-edf-simple (n1 < n2 ) → (nth (n1 , make-schedule-edf (s, r, n2 )) = nth (n1 , s))

Theorem: car-append car (append (x, y)) = if listp (x) then car (x)

else car (y) endif

Theorem: listp-edf-simple listp (edf (n, r)) = (n ≄ 0)

Theorem: unfulfilled-schedule-first-part-only (n < length (s)) → (unfulfilled (n, s, r) = unfulfilled (n, firstn (n, s), r))

Theorem: firstn-n-edf-simple-n (fix (n1 ) = fix (n2 )) → (firstn (n1 , edf (n2 , r)) = edf (n2 , r))

Theorem: firstn-edf-simple-regular (n1 < n2 ) → (firstn (n1 , edf (n2 , r)) = edf (n1 , r))

Theorem: firstn-edf-simple-help (n2 ≮ n1 ) → (firstn (n1 , edf (n2 , r)) = edf (n1 , r))

Theorem: firstn-edf-simple firstn (n1 , edf (n2 , r)) = if n2 < n1 then append (edf (n2 , r), repeat (n1 − n2 , 0))

else edf (n1 , r) endif

Theorem: nth-append nth (n, append (x, y)) = if n < length (x) then nth (n, x)

else nth (n − length (x), y) endif

; dangerous - must use in special rules

Theorem: nth-edf-simple-simpler (n < n2 ) → (nth (n, edf (n2 , r)) = nth (n, edf (1 + n, r)))

Theorem: active-task-requests-nnumberp (n ∉ N) → (active-task-requests (n, r) = active-task-requests (0, r))

Theorem: unfulfilled-nnumberp (n ∉ N) → (unfulfilled (n, s, r) = unfulfilled (0, s, r))

Theorem: nth-edf-simple nth (n, edf (n2 , r)) = if n < n2

then if listp (unfulfilled (n, edf (n, r), active-task-requests (n, r)))

then car (least-deadline (unfulfilled (n, edf (n, r), active-task-requests (n, r))))

else nil endif else 0 endif

Theorem: equal-cdr-cdr-means ((cdr (x) = cdr (y)) ∧ listp (x) ∧ listp (y)) → ((x = y) = (car (x) = car (y)))

Event: Disable equal-cdr-cdr-means.

Theorem: first-instance-same-as-member n → (first-instance (n, v, s) ↔ (v ∈ nthcdr (n, s)))

Theorem: nth-make-element-edf n → (nth (n, make-element-edf (s, r, n))

= if listp (unfulfilled (n, s, active-task-requests (n, r)))

∧ first-instance (n,

car (least-deadline (unfulfilled (n, s, active-task-requests (n,

r)))),

s) then car (least-deadline (unfulfilled (n,

s,

active-task-requests (n, r))))

else nth (n, s) endif)

Theorem: unfulfilled-append unfulfilled (n, s, append (r1 , r2 )) = append (unfulfilled (n, s, r1 ), unfulfilled (n, s, r2 ))

Definition: no-unfulfilled-active-task-induct (pts, oldpts) = if pts ≃ nil then t

else no-unfulfilled-active-task-induct (cdr (pts),

append (oldpts, list (car (pts)))) endif Theorem: periodic-tasksp-append-car (periodic-tasksp (append (x, y)) ∧ listp (y)) → periodic-tasksp (append (x, list (car (y))))

Theorem: assoc-plist assoc (v, plist (l)) = assoc (v, l)

Theorem: all-nils-or-cars-plist2 all-nils-or-cars (l1 , plist (l2 )) = all-nils-or-cars (l1 , l2 )

;; bad bad bad

Theorem: assoc-append-simple ((¬ assoc (v, l)) ∧ periodic-tasksp (l)) → (assoc (v, append (l, l2 )) = assoc (v, l2 ))

Theorem: listp-unfulfilled-if-schedule-contains (periodic-taskp (pt) ∧ good-schedule (s, periodic-task-requests (pt, n1 , n2 )) ∧ (nth (n, s) = car (pt)) ∧ (n < n2 ) ∧ (n ≮ n1 )) → listp (unfulfilled (n,

firstn (n, s),

active-task-requests (n,

periodic-task-requests (pt, n1 , n2 ))))

Theorem: no-unfulfilled-active-task-if-nil-help ((nth (n, s) ≠ nil) ∧ periodic-tasksp (append (oldpts, pts)) ∧ periodic-tasksp (oldpts) ∧ periodic-tasksp (pts) ∧ good-schedule (s, periodic-tasks-requests (pts, n1 , n2 )) ∧ all-nils-or-cars (s, append (oldpts, pts)) ∧ (n < n2 ) ∧ (n < length (s)) ∧ (n ≮ n1 )) → (listp (unfulfilled (n,

firstn (n, s),

active-task-requests (n,

periodic-tasks-requests (pts, n1 , n2 ))))

∨ assoc (nth (n, s), oldpts))

Theorem: no-unfulfilled-active-task-if-nil ((nth (n, s) ≠ nil) ∧ periodic-tasksp (pts) ∧ good-schedule (s, periodic-tasks-requests (pts, n1 , n2 )) ∧ all-nils-or-cars (s, pts) ∧ (n < n2 ) ∧ (n < length (s)) ∧ (n ≮ n1 )) → listp (unfulfilled (n,

firstn (n, s),

active-task-requests (n,

periodic-tasks-requests (pts, n1 , n2 ))))

Theorem: replace-nth-first-instance-nnumberp (n ∉ N) → (replace-nth (first-instance (n, v, s), v2 , l)

= replace-nth (first-instance (0, v, s), v2 , l))

Theorem: make-element-nnumberp (n ∉ N) → (make-element-edf (s, r, n) = make-element-edf (s, r, 0))

;; versions of nth- theorems with n = 0

Theorem: car-make-schedule-edf-simple (0 < n2 ) → (car (make-schedule-edf (s, r, n2 )) = car (s))

Theorem: car-edf-simple car (edf (n2 , r)) = if 0 < n2

then if listp (unfulfilled (0, edf (0, r), active-task-requests (0, r)))

then car (least-deadline (unfulfilled (0, edf (0, r), active-task-requests (0, r))))

else nil endif else 0 endif

Theorem: car-repeat car (repeat (n, v)) = if n ≃ 0 then 0

else v endif

Theorem: numberp-first-instance (n ∈ N) → ((first-instance (n, v, l) ∈ N) = (v ∈ nthcdr (n, l)))

Theorem: nth-make-element-simple (n1 < n2 ) → (nth (n1 , make-element-edf (s, r, n2 )) = nth (n1 , s))

Theorem: car-make-element-simple (n ≄ 0) → (car (make-element-edf (s, r, n)) = car (s))

Theorem: car-make-element-edf car (make-element-edf (s, r, n)) = if (n ≃ 0)

∧ listp (unfulfilled (0, s, active-task-requests (0, r)))

∧ first-instance (0,

car (least-deadline (unfulfilled (0, s, active-task-requests (0,

r)))),

s)

then car (least-deadline (unfulfilled (0, s, active-task-requests (0, r)))) else car (s) endif

Theorem: firstn-make-element-simple (n2 ≮ n1 ) → (firstn (n1 , make-element-edf (s, r, n2 )) = firstn (n1 , s))

Theorem: firstn-sub1-cdr-make-element (n ≄ 0) → (firstn (n − 1, cdr (make-element-edf (s, r, n))) = firstn (n − 1, cdr (s)))

Theorem: nthcdr-n-cons-firstn-n nthcdr (n, cons (a, firstn (n, l))) = if n ≃ 0 then list (a)

else list (nth (n − 1, l)) endif

Theorem: nth-make-element-edf-sub1 (n ≄ 0) → (nth (n − 1, cdr (make-element-edf (s, r, n)))

= if listp (unfulfilled (n, s, active-task-requests (n, r)))

∧ first-instance (n,

car (least-deadline (unfulfilled (n, s, active-task-requests (n,

r)))),

s) then car (least-deadline (unfulfilled (n,

s,

active-task-requests (n, r))))

else nth (n, s) endif)

Theorem: equal-repeat-when-nil-not (car (s) ≠ v) → ((s = repeat (length (s), v)) = (s = nil))

Theorem: member-car-schedule (good-schedule (s, rs) ∧ valid-requests (rs) ∧ (r ∈ rs)) → (car (r) ∈ s)

Theorem: sublistp-remove-until sublistp (x, remove-until (v, y)) → sublistp (x, y)

Theorem: member-nil-periodic-task-requests nil ∉ periodic-task-requests (pt, n1 , n2 )

Theorem: member-nil-periodic-tasks-requests nil ∉ periodic-tasks-requests (pts, n1 , n2 )

Theorem: member-least-deadline-better (sublistp (r1 , r2 ) ∧ (nil ∉ r2 )) → ((least-deadline (r1 ) ∈ r2 ) = listp (r1 ))

Theorem: make-schedule-edf-is-edf-simple (non-overlapping-requests (r) ∧ cars-non-nil-litatoms (r) ∧ all-litatoms (s) ∧ good-schedule (s, r) ∧ (plist (s) = s) ∧ all-non-nil-corresponding (s, r, 0) ∧ (r = periodic-tasks-requests (pts, 0, length (s))) ∧ all-nils-or-cars (s, pts) ∧ periodic-tasksp (pts) ∧ (edf (n, r) = firstn (n, s)) ∧ (length (s) ≮ n)) → (nthcdr (n, make-schedule-edf (s, r, n)) = nthcdr (n, edf (length (s), r)))

;;; big lemma

Theorem: make-schedule-edf-is-edf (periodic-tasksp (pts) ∧ cars-non-nil-litatoms (periodic-tasks-requests (pts, 0, length (s))) ∧ all-litatoms (s) ∧ good-schedule (s, periodic-tasks-requests (pts, 0, length (s))) ∧ (plist (s) = s) ∧ all-non-nil-corresponding (s,

periodic-tasks-requests (pts, 0, length (s)),

                         0)

∧ all-nils-or-cars (s, pts) ∧ periodic-tasksp (pts) ∧ (n = length (s))) → (make-schedule-edf (s, periodic-tasks-requests (pts, 0, n), 0)

= edf (length (s), periodic-tasks-requests (pts, 0, length (s))))

Theorem: plist-make-simple-schedule plist (make-simple-schedule (pts, bigp, length)) = make-simple-schedule (pts, bigp, length)

Definition: cpu-utilization (pts, bigp) = if listp (pts)

then ((bigp ∗ tk-duration (car (pts))) ÷ tk-period (car (pts)))

+ cpu-utilization (cdr (pts), bigp) else 0 endif

Theorem: length-substring-schedule (expanded-tasksp (pts, bigp) ∧ periodic-tasksp (pts)) → (length (substring-schedule (pts, bigp)) = cpu-utilization (pts, bigp))

;; combine big lemmas

Theorem: good-edf-for-expanded (expanded-tasksp (pts, bigp) ∧ (bigp ≮ cpu-utilization (pts, bigp)) ∧ periodic-tasksp (pts) ∧ ((n mod bigp) = 0) ∧ ((n mod big-period (pts)) = 0)) → good-schedule (edf (n, periodic-tasks-requests (pts, 0, n)),

periodic-tasks-requests (pts, 0, n))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: expand-list (n, list) = if listp (list)

then append (repeat (n, car (list)), expand-list (n, cdr (list)))

else nil endif

Theorem: expand-list-append expand-list (n, append (l1 , l2 )) = append (expand-list (n, l1 ), expand-list (n, l2 ))

Theorem: listp-expand-list listp (expand-list (n, list)) = ((n ≄ 0) ∧ listp (list))

Theorem: length-expand-list length (expand-list (n, list)) = (n ∗ length (list))

Theorem: plist-expand-list plist (expand-list (n, list)) = expand-list (n, list)

Theorem: nthcdr-is-nil (nthcdr (n, l) = nil) = ((length (l) = fix (n)) ∧ (plist (l) = l))

Theorem: active-task-requests-expand-tasks-requests (bigp ≄ 0) → (active-task-requests (n, expand-tasks-requests (r, bigp))

= expand-tasks-requests (active-task-requests (n ÷ bigp, r), bigp))

Theorem: repeat-1 repeat (1, v) = list (v)

Event: Disable lessp-difference-special.

Theorem: quotient-add1-plus-special ((1 + (z + (bigp ∗ v))) ÷ bigp) = if bigp ≃ 0 then 0

else v + ((1 + z) ÷ bigp) endif

Theorem: remainder-add1-plus-special ((1 + (z + (bigp ∗ v))) mod bigp) = if bigp ≃ 0 then 1 + z

else (1 + z) mod bigp endif

Theorem: plist-nthcdr ((length (l) ≮ n) ∧ (plist (l) = l)) → (plist (nthcdr (n, l)) = nthcdr (n, l))

Theorem: remainder-plus-add1-hack (((z + (v ∗ z)) mod (1 + v)) = 0) ∧ (((z + (z ∗ v)) mod (1 + v)) = 0)

Theorem: quotient-plus-add1-hack (((z + (v ∗ z)) ÷ (1 + v)) = fix (z)) ∧ (((z + (z ∗ v)) ÷ (1 + v)) = fix (z))

Theorem: equal-remainder-sub1-0 ((x mod y) = 0) → (((x − 1) mod y)

= if x ≃ 0 then 0 elseif y ≃ 0 then x − 1 elseif y = 1 then 0 else y − 1 endif)

Theorem: lessp-round-means ((bigp ∗ (n ÷ bigp)) < n) = (((n mod bigp) ≠ 0) ∨ ((bigp ≃ 0) ∧ (n ≄ 0)))

Theorem: equal-repeat-nil (repeat (n, v) = nil) = (n ≃ 0)

Theorem: times-1-arg2 (x ∗ 1) = fix (x)

Theorem: firstn-0 firstn (0, l) = nil

Theorem: lessp-times-sub1-sub1 ((bigp ∗ ((n ÷ bigp) − 1)) < (n − 1)) = ((1 < n) ∧ (bigp ≠ 1))

Theorem: equal-cons-repeat (cons (a, b) = repeat (n, v)) = ((a = v) ∧ (n ≄ 0) ∧ (b = repeat (n − 1, v)))

Theorem: lessp-1-means (1 < x) = ((x ≄ 0) ∧ (x ≠ 1))

Theorem: lessp-sub1-plus-hack (n1 < ((n2 + n1 ) − 1)) = (1 < n2 )

;; backwards

Theorem: firstn-nthcdr firstn (x, nthcdr (n, s)) = nthcdr (n, firstn (n + x, s))

Event: Disable firstn-nthcdr.

Theorem: nthcdr-x-firstn-x nthcdr (n, firstn (n, l)) = nil

Theorem: nthcdr-x-edf-x nthcdr (n, edf (n, r)) = nil

Theorem: nth-cons nth (n, cons (a, b)) = if n ≃ 0 then a

else nth (n − 1, b) endif Theorem: firstn-nthcdr-too-big (n < length (l)) → (firstn (n − z, nthcdr (z, l))

= if n < z then nil else nthcdr (z, firstn (n, l)) endif)

Theorem: firstn-nthcdr-edf-plus firstn (n1 − n2 , nthcdr (n2 , edf (z + n1 , r))) = firstn (n1 − n2 , nthcdr (n2 , edf (n1 , r)))

Definition: nthcdr-expand-induct (n, b, l) = if listp (l)

then if b < n then nthcdr-expand-induct (n − b, b, cdr (l))

else t endif else t endif

Theorem: nthcdr-expand-list ((n mod b) = 0) → (nthcdr (n, expand-list (b, l))

= if (b ∗ length (l)) < n then 0 else expand-list (b, nthcdr (n ÷ b, l)) endif)

Theorem: expand-list-repeat expand-list (b, repeat (n, v)) = repeat (n ∗ b, v)

Theorem: firstn-expand-list ((n mod b) = 0) → (firstn (n, expand-list (b, l)) = expand-list (b, firstn (n ÷ b, l)))

Theorem: occurrences-expand-list occurrences (v, expand-list (bigp, l)) = (bigp ∗ occurrences (v, l))

Theorem: expand-list-0 (n ≃ 0) → (expand-list (n, l) = nil)

Theorem: listp-firstn listp (firstn (n, l)) = (n ≄ 0)

Theorem: equal-nil-firstn (nil = firstn (n, l)) = (n ≃ 0)

Theorem: firstn-difference-plus-nthcdr ((length (l) ≮ (a + b)) ∧ (b ≮ c)) → (firstn ((a + b) − c, nthcdr (c, l))

= append (firstn (b − c, nthcdr (c, l)), firstn (a, nthcdr (b, l))))

Theorem: lessp-occurrences-firstn n ≮ occurrences (v, firstn (n, l))

Event: Disable lessp-occurrences-firstn.

Theorem: lessp-occurrences-edf n ≮ occurrences (v, edf (n, r))

Theorem: equal-times-hack (a < b) → ((a = (b ∗ n)) = ((a = 0) ∧ (b ≄ 0) ∧ (n ≃ 0)))

Theorem: equal-occurrences-firstn-times (z < b) → ((occurrences (v, firstn (z, l)) = (b ∗ n))

= ((n ≃ 0) ∧ (occurrences (v, firstn (z, l)) ≃ 0)))

Theorem: firstn-plus firstn (a + b, l) = append (firstn (b, l), firstn (a, nthcdr (b, l)))

Theorem: equal-plus-times (z < b) → ((((b ∗ n) + z) = (b ∗ v))

= ((z ≃ 0) ∧ (fix (n) = fix (v))))

Theorem: firstn-noop (length (l) = fix (n)) → (firstn (n, l) = plist (l))

Theorem: lessp-x-x (x < x) = f

Theorem: overlapping-non-overlapping3-means (non-overlapping-requests3 (r, r2 ) ∧ (x ≮ cadr (r)) ∧ (car (req) = car (r)) ∧ (x ≮ cadr (req)) ∧ (x < caddr (r)) ∧ (req ∈ r2 )) → ((x < caddr (req)) = (r = req))

Theorem: assoc-unfulfilled-expanded-non-overlapping ((r ∉ r2 ) ∧ non-overlapping-requests3 (r, r2 ) ∧ (z < b) ∧ (x < caddr (r)) ∧ (x ≮ cadr (r)))

→ (¬ assoc (car (r),

unfulfilled (z + (b ∗ x), s, expand-tasks-requests (active-task-requests (x,

r2 ),

b))))

Theorem: not-assoc-car-req (valid-requests (r2 ) ∧ (req ∈ r2 ) ∧ (x < caddr (req)) ∧ (x ≮ cadr (req)) ∧ non-overlapping-requests (r2 ) ∧ (z < b) ∧ (occurrences (car (req),

firstn ((z + (b ∗ x)) − (b ∗ cadr (req)), nthcdr (b ∗ cadr (req), s)))

= (b ∗ cadddr (req)))) → (¬ assoc (car (req),

unfulfilled (z + (b ∗ x), s, expand-tasks-requests (active-task-requests (x,

r2 ),

b))))

Theorem: equal-car-car-hack ((e1 ∈ l) ∧ (¬ assoc (car (e2 ), l)) ∧ valid-requests (l) ∧ listp (e1 ) ∧ listp (e2 )) → (car (e1 ) ≠ car (e2 ))

Theorem: not-member-nthcdr-add1 (v ∉ nthcdr (1 + x, s)) → ((v ∈ nthcdr (x, s)) = ((x < length (s)) ∧ (v = nth (x, s))))

Theorem: occurrences-hack ((v ∉ nthcdr (n, s)) ∧ (n ≮ b) ∧ litatom (v)) → (occurrences (v, firstn ((a + n) − b, nthcdr (b, s)))

= occurrences (v, firstn (n − b, nthcdr (b, s))))

Theorem: occurrences-hack2 ((v ∉ nthcdr (n, l)) ∧ (n < length (l))) → (occurrences (v, nthcdr (n1 , l))

= occurrences (v, nthcdr (n1 , firstn (n, l))))

Theorem: valid-requests-unfulfilled valid-requests (r) → valid-requests (unfulfilled (n, s, r))

Theorem: valid-requests-expand-tasks-requests valid-requests (r) → (valid-requests (expand-tasks-requests (r, b))

= ((b ≄ 0) ∨ (¬ listp (r))))

Theorem: litatom-caar valid-requests (r) → (litatom (caar (r)) = listp (r))

Event: Disable litatom-caar.

Theorem: numberp-cadar valid-requests (r) → (cadar (r) ∈ N)

Event: Disable numberp-cadar.

Theorem: not-equal-car-least-deadline (valid-requests (r2 ) ∧ (req ∈ r2 ) ∧ (x < caddr (req)) ∧ (x ≮ cadr (req)) ∧ non-overlapping-requests (r2 ) ∧ (z < b) ∧ (b ≄ 0) ∧ litatom (car (req)) ∧ (occurrences (car (req),

firstn ((z + (b ∗ x)) − (b ∗ cadr (req)), nthcdr (b ∗ cadr (req), s)))

= (b ∗ cadddr (req)))) → (car (req)

≠ car (least-deadline (unfulfilled (z + (b ∗ x), s, expand-tasks-requests (active-task-requests (x,

r2 ),

b)))))

Theorem: not-equal-car-least-deadline-special (valid-requests (r2 ) ∧ (req ∈ r2 ) ∧ (x < caddr (req)) ∧ (x ≮ cadr (req)) ∧ non-overlapping-requests (r2 )

∧ (b ≄ 0) ∧ litatom (car (req)) ∧ (occurrences (car (req),

firstn ((b ∗ x) − (b ∗ cadr (req)),

nthcdr (b ∗ cadr (req), s)))

= (b ∗ cadddr (req)))) → (car (req)

≠ car (least-deadline (unfulfilled (b ∗ x, s, expand-tasks-requests (active-task-requests (x,

r2 ),

b)))))

Theorem: occurrences-edf-satisfied (listp (r) ∧ (x < caddar (r)) ∧ (x ≮ cadar (r)) ∧ (z < b) ∧ (expand-list (b, edf (x, r2 ))

= edf (b ∗ x, expand-tasks-requests (r2 , b))) ∧ valid-requests (r2 ) ∧ valid-requests (r) ∧ non-overlapping-requests (r2 ) ∧ sublistp (r, r2 ) ∧ (b ≠ 0) ∧ (b ∈ N) ∧ (x ∈ N) ∧ (occurrences (caar (r),

firstn (x − cadar (r), nthcdr (cadar (r), edf (x, r2 ))))

= cadddar (r))) → (occurrences (caar (r),

firstn (z,

nthcdr (b ∗ x,

edf (z + (b ∗ x),

expand-tasks-requests (r2 , b)))))

= 0)

Theorem: unfulfilled-expanded-on-line ((z < b) ∧ (expand-list (b, edf (x, r2 ))

= edf (x ∗ b, expand-tasks-requests (r2 , b))) ∧ valid-requests (r2 ) ∧ valid-requests (r) ∧ non-overlapping-requests (r2 )

∧ sublistp (r, r2 )) → (unfulfilled (z + (x ∗ b),

edf (z + (x ∗ b), expand-tasks-requests (r2 , b)), expand-tasks-requests (active-task-requests (x, r), b))

= unfulfilled (x ∗ b, edf (z + (x ∗ b), expand-tasks-requests (r2 , b)), expand-tasks-requests (active-task-requests (x, r), b)))

Theorem: unfulfilled-expand-list (valid-requests (r) ∧ ((n mod b) = 0) ∧ (b ≄ 0)) → (unfulfilled (n, expand-list (b, s), expand-tasks-requests (r, b))

= expand-tasks-requests (unfulfilled (n ÷ b, s, r), b))

Theorem: equal-nil-expand-list (nil = expand-list (b, l)) = ((b ≃ 0) ∨ (l ≃ nil))

Theorem: valid-requests-sublistp (sublistp (x, y) ∧ (plist (x) = x) ∧ valid-requests (y)) → valid-requests (x)

Theorem: unfulfilled-sub1-expanded-on-line ((a ≄ 0) ∧ (a < b) ∧ (expand-list (b, edf (x, r2 ))

= edf (x ∗ b, expand-tasks-requests (r2 , b))) ∧ non-overlapping-requests (r2 ) ∧ valid-requests (r2 ) ∧ valid-requests (r) ∧ sublistp (r, r2 )) → (unfulfilled ((a + (b ∗ x)) − 1,

edf ((a + (b ∗ x)) − 1, expand-tasks-requests (r2 , b)), expand-tasks-requests (active-task-requests (x, r), b))

= unfulfilled (x ∗ b,

edf ((a + (x ∗ b)) − 1,

expand-tasks-requests (r2 , b)), expand-tasks-requests (active-task-requests (x, r), b)))

Theorem: firstn-only-helper (firstn (n, a) = firstn (n, b)) → (firstn (n − c, nthcdr (c, a)) = firstn (n − c, nthcdr (c, b)))

Theorem: firstn-nthcdr-edf-plus-simple firstn (n − a, nthcdr (a, edf (b + n, r))) = firstn (n − a, nthcdr (a, edf (n, r)))

Theorem: unfulfilled-too-big unfulfilled (n, edf (a + n, r1 ), r2 ) = unfulfilled (n, edf (n, r1 ), r2 )

Theorem: unfulfilled-too-big-sub1 (a ≄ 0) → (unfulfilled (n, edf ((a + n) − 1, r1 ), r2 )

= unfulfilled (n, edf (n, r1 ), r2 ))

Theorem: car-least-deadline-expand-tasks-requests (b ≄ 0) → (car (least-deadline (expand-tasks-requests (r, b)))

= car (least-deadline (r)))

Theorem: remainder-hack ((n mod p) = 0) → ((((x + n) − 1) mod p)

= if x ≃ 0 then (n − 1) mod p else (x − 1) mod p endif)

Theorem: equal-car-least-deadline-nil valid-requests (r) → (car (least-deadline (r)) ≠ nil)

Theorem: unfulfilled-0-expand-tasks-requests (valid-requests (r) ∧ (b ≄ 0)) → (unfulfilled (0, s, expand-tasks-requests (r, b))

= expand-tasks-requests (unfulfilled (0, s, r), b))

Theorem: unfulfilled-0-edf unfulfilled (0, edf (n, r), r2 ) = unfulfilled (0, nil, r2 )

Theorem: unfulfilled-expanded-on-line-beginning ((z < b) ∧ non-overlapping-requests (r2 ) ∧ (z ≠ 0) ∧ sublistp (r, r2 ) ∧ valid-requests (r) ∧ valid-requests (r2 )) → (unfulfilled (z,

edf (z, expand-tasks-requests (r2 , b)),

expand-tasks-requests (active-task-requests (0, r), b))

= unfulfilled (0, edf (z, expand-tasks-requests (r2 , b)), expand-tasks-requests (active-task-requests (0, r), b)))

;(prove-lemma edf-simple-expand-tasks-requests (rewrite)
;  (implies
;   (and
;    (lessp 1 bigp)
;    (non-overlapping-requests r)
;    (valid-requests r))
;  (equal
;   (edf n (expand-tasks-requests r bigp))
;   (append
;    (expand-list bigp (edf (quotient n bigp) r))
;    (repeat (remainder n bigp)
;            (if (listp (unfulfilled
;                        (quotient n bigp)
;                        (edf (quotient n bigp) r)
;                        (active-task-requests (quotient n bigp) r)))
;                (car (least-deadline
;                      (unfulfilled
;                       (quotient n bigp)
;                       (edf (quotient n bigp) r)
;                       (active-task-requests (quotient n bigp) r))))
;              nil)))))
;  ((induct (plus n bigp))
;   (disable-theory t)
;   (enable-theory naturals ground-zero task-abbr)
;   (disable times-add1)
;   (enable edf expand-list listp-edf-simple listp-expand-list
;           valid-requests-unfulfilled unfulfilled-expanded-on-line-beginning
;           equal-car-least-deadline-nil
;           length-edf-simple length-expand-list plist-expand-list
;           firstn-edf-simple equal-append equal-repeat-repeat
;           equal-cons-repeat lessp-1-means remainder-add1-plus-special
;           equal-repeat-nil  firstn-0 lessp-times-sub1-sub1 firstn
;           unfulfilled-sub1-expanded-on-line   unfulfilled-expanded-on-line
;           sublistp-x-x unfulfilled-too-big
;           car-least-deadline-expand-tasks-requests
;           nthcdr-expand-list listp-expand-tasks-requests
;           valid-requests-active-task-requests
;           expand-list-repeat unfulfilled-too-big-sub1
;           firstn-expand-list unfulfilled-0-edf
;           remainder-hack unfulfilled-0-expand-tasks-requests
;           occurrences-expand-list
;           unfulfilled-expand-list
;           equal-remainder-sub1-0 lessp-sub1-plus-hack
;           active-task-requests-expand-tasks-requests append-nil

;           remainder-plus-add1-hack quotient-plus-add1-hack
;           firstn-append firstn-edf-simple length-nthcdr plist-repeat
;           plist-edf-simple listp-edf-simple lessp-round-means
;           firstn-repeat length-repeat nthcdr-repeat length
;           plist-expand-list quotient-add1-plus-special repeat-1
;           plist-nthcdr nthcdr-is-nil length-append expand-list-append
;           nlistp-nthcdr listp-nthcdr nthcdr-append nthcdr listp-repeat
;           equal-nil-expand-list
;           times-1-arg2
;           repeat expand-list)))

Theorem: edf-simple-expand-tasks-requests ((1 < bigp) ∧ non-overlapping-requests (r) ∧ valid-requests (r)) → (edf (n, expand-tasks-requests (r, bigp))

= append (expand-list (bigp, edf (n ÷ bigp, r)),

let undone be unfulfilled (n ÷ bigp, edf (n ÷ bigp, r), active-task-requests (n ÷ bigp,

r))

in

repeat (n mod bigp, if listp (undone) then car (least-deadline (undone)) else nil endif) endlet))

Theorem: quotient-difference-special (((a ∗ b) − (a ∗ c)) ÷ a) = if a ≃ 0 then 0

else b − c endif

Theorem: good-schedule-expand-tasks-reduces ((1 < bigp) ∧ non-overlapping-requests (r1 ) ∧ sublistp (r2 , r1 ) ∧ valid-requests (r1 ) ∧ valid-requests (r2 ) ∧ ((n mod bigp) = 0) ∧ good-schedule (edf (n, expand-tasks-requests (r1 , bigp)),

expand-tasks-requests (r2 , bigp)))

→ good-schedule (edf (n ÷ bigp, r1 ), r2 )

Theorem: expand-tasks-1 periodic-tasksp (pts) → (expand-tasks (pts, 1) = pts)

Theorem: cpu-utilization-expand-tasks periodic-tasksp (pts) → (cpu-utilization (expand-tasks (pts, n), n2 )

= if n ≃ 0 then 0 else cpu-utilization (pts, n2 ) endif)

Theorem: big-period-expand-tasks big-period (expand-tasks (pts, n)) = (exp (n, length (pts)) ∗ big-period (pts))

Theorem: remainder-from-exp (((n mod exp (x, y)) = 0) ∧ (y ≄ 0)) → ((n mod x) = 0)

Theorem: good-edf-help ((big-period (pts) ≮ cpu-utilization (pts, big-period (pts))) ∧ periodic-tasksp (pts) ∧ listp (pts) ∧ (1 < big-period (pts)) ∧ ((n mod exp (big-period (pts), length (pts))) = 0)) → good-schedule (edf (n, periodic-tasks-requests (pts, 0, n)),

periodic-tasks-requests (pts, 0, n))

Theorem: good-edf-with-remainder ((big-period (pts) ≮ cpu-utilization (pts, big-period (pts))) ∧ periodic-tasksp (pts) ∧ (1 < big-period (pts)) ∧ ((n mod exp (big-period (pts), length (pts))) = 0)) → good-schedule (edf (n, periodic-tasks-requests (pts, 0, n)),

periodic-tasks-requests (pts, 0, n))

Definition: requests-deadlines-not-greater (r, time) = if listp (r)

then if time < caddar (r)

then requests-deadlines-not-greater (cdr (r), time) else cons (car (r),

requests-deadlines-not-greater (cdr (r), time)) endif

else nil endif

Definition: firstn-nthcdr-firstn-induct (a, b, n, l) = if a ≃ 0 then t

else firstn-nthcdr-firstn-induct (a − 1, b − 1, n − 1, l) endif

Theorem: firstn-nthcdr-firstn-simple (n ≮ (a + b)) → (firstn (a, nthcdr (b, firstn (n, l))) = firstn (a, nthcdr (b, l)))

Theorem: good-schedule-requests-not-greater (good-schedule (s, r) ∧ valid-requests (r)) → good-schedule (firstn (n, s), requests-deadlines-not-greater (r, n))

Theorem: requests-deadlines-append requests-deadlines-not-greater (append (a, b), time) = append (requests-deadlines-not-greater (a, time),

requests-deadlines-not-greater (b, time))

Theorem: plist-requests-deadlines plist (requests-deadlines-not-greater (a, time)) = requests-deadlines-not-greater (a, time)

Theorem: requests-deadlines-periodic-task-simple (n1 ≮ n2 ) → (requests-deadlines-not-greater (periodic-task-requests (pt, n1 , n), n2 )

= nil)

Theorem: equal-nil-periodic-task-requests (periodic-task-requests (pt, n1 , n2 ) = nil) = ((¬ periodic-taskp (pt)) ∨ (n1 ≮ n2 ))

Theorem: requests-deadlines-not-greater-periodic-task (((n mod cadr (pt)) = 0) ∧ ((n2 mod cadr (pt)) = 0) ∧ ((n1 mod cadr (pt)) = 0)) → (requests-deadlines-not-greater (periodic-task-requests (pt, n1 , n2 ), n)

= if n < n2 then periodic-task-requests (pt, n1 , n) else periodic-task-requests (pt, n1 , n2 ) endif)

Theorem: equal-remainder-big-period (e ∈ l) → ((big-period (l) mod cadr (e)) = 0)

Theorem: remainder-period-0-if-big-period (periodic-tasksp (pts) ∧ ((n mod big-period (pts)) = 0) ∧ (pt ∈ pts)) → ((n mod cadr (pt)) = 0)

Theorem: equal-nil-periodic-tasks-requests (nil = periodic-tasks-requests (pts, n1 , n2 )) = ((pts ≃ nil) ∨ (¬ periodic-tasksp (pts)) ∨ (n1 ≮ n2 ))

Theorem: requests-deadlines-not-greater-periodic-help (periodic-tasksp (pts2 ) ∧ sublistp (pts1 , pts2 ) ∧ (n1 = 0) ∧ (n2 ≮ n3 )

∧ ((n2 mod big-period (pts2 )) = 0) ∧ ((n3 mod big-period (pts2 )) = 0)) → (requests-deadlines-not-greater (periodic-tasks-requests (pts1 , n1 , n2 ),

n3 )

= periodic-tasks-requests (pts1 , n1 , n3 ))

Theorem: requests-deadlines-not-greater-periodic-rewrite (periodic-tasksp (pts) ∧ (n1 = 0) ∧ (n2 ≮ n3 ) ∧ ((n2 mod big-period (pts)) = 0) ∧ ((n3 mod big-period (pts)) = 0)) → (requests-deadlines-not-greater (periodic-tasks-requests (pts, n1 , n2 ), n3 )

= periodic-tasks-requests (pts, n1 , n3 ))

Theorem: plist-active-task-requests plist (active-task-requests (n, r)) = active-task-requests (n, r)

Theorem: lessp-plus-times-hack ((x + (x ∗ y)) < (x ∗ z)) = ((x ≄ 0) ∧ ((1 + y) < z))

Theorem: periodic-task-requests-simple (n1 ≮ n2 ) → (periodic-task-requests (pt, n1 , n2 ) = nil)

Theorem: active-task-requests-periodic-task-requests-simple (n < n1 ) → (active-task-requests (n, periodic-task-requests (pt, n1 , n2 )) = nil)

Theorem: active-task-requests-periodic-task-requests (((n1 mod cadr (pt)) = 0) ∧ ((n2 mod cadr (pt)) = 0) ∧ ((n mod cadr (pt)) = 0) ∧ (n1 ∈ N)) → (active-task-requests (n, periodic-task-requests (pt, n1 , n2 ))

= if (¬ periodic-taskp (pt)) ∨ (n < n1 ) ∨ (n ≮ n2 ) then nil else list (list (car (pt),

cadr (pt) ∗ (n ÷ cadr (pt)),

cadr (pt)

+ (cadr (pt) ∗ (n ÷ cadr (pt))), caddr (pt))) endif)

Theorem: active-task-requests-not-greater active-task-requests (n1 , requests-deadlines-not-greater (r, n2 )) = requests-deadlines-not-greater (active-task-requests (n1 , r), n2 )

Definition: requests-starts-earlier (r, time) = if listp (r)

then if cadar (r) < time then cons (car (r), requests-starts-earlier (cdr (r), time)) else requests-starts-earlier (cdr (r), time) endif

else nil endif

Theorem: requests-starts-earlier-append requests-starts-earlier (append (a, b), n) = append (requests-starts-earlier (a, n), requests-starts-earlier (b, n))

Theorem: active-task-requests-requests-starts-earlier (n < n1 ) → (active-task-requests (n, requests-starts-earlier (r, n1 ))

= active-task-requests (n, r))

Theorem: edf-requests-starts-earlier (n1 ≮ n) → (edf (n, requests-starts-earlier (r, n1 )) = edf (n, r))

Theorem: plist-requests-starts-earlier plist (requests-starts-earlier (r, n)) = requests-starts-earlier (r, n)

Theorem: requests-starts-earlier-periodic-task (((n mod cadr (pt)) = 0) ∧ ((n1 mod cadr (pt)) = 0) ∧ ((n2 mod cadr (pt)) = 0)) → (requests-starts-earlier (periodic-task-requests (pt, n1 , n2 ), n)

= periodic-task-requests (pt, n1 , if n < n2 then n else n2 endif))

Theorem: requests-starts-earlier-periodic-tasks (((n mod big-period (pts2 )) = 0) ∧ ((n1 mod big-period (pts2 )) = 0) ∧ ((n2 mod big-period (pts2 )) = 0) ∧ sublistp (pts1 , pts2 ) ∧ periodic-tasksp (pts2 )) → (requests-starts-earlier (periodic-tasks-requests (pts1 , n1 , n2 ), n)

= periodic-tasks-requests (pts1 , n1 , if n < n2 then n else n2 endif))

Theorem: good-edf-almost ((big-period (pts) ≮ cpu-utilization (pts, big-period (pts))) ∧ periodic-tasksp (pts) ∧ (1 < big-period (pts)) ∧ ((n mod big-period (pts)) = 0)) → good-schedule (edf (n, periodic-tasks-requests (pts, 0, n)),

periodic-tasks-requests (pts, 0, n))

Theorem: equal-plus-1 ((a + b) = 1) = (((a ≃ 0) ∧ (b = 1)) ∨ ((b ≃ 0) ∧ (a = 1)))

Theorem: equal-cpu-utilization-0 (((n mod big-period (x)) = 0) ∧ (n ≄ 0) ∧ periodic-tasksp (x)) → ((cpu-utilization (x, n) = 0) = (x = nil))

Theorem: equal-1-big-period ((big-period (pts) ≮ cpu-utilization (pts, big-period (pts))) ∧ (big-period (pts) = 1)) → (periodic-tasksp (pts)

= ((pts = nil)

∨ ((plist (pts) = pts) ∧ (length (pts) = 1) ∧ periodic-taskp (car (pts)) ∧ (cadar (pts) = 1) ∧ (caddar (pts) = 1))))

Definition: simple-requests (v, n1 , n2 ) = if n1 < n2

then cons (list (v, n1 , 1 + n1 , 1), simple-requests (v, 1 + n1 , n2 )) else nil endif

Theorem: periodic-task-requests-as-simple-requests periodic-task-requests (list (v, 1, 1), n1 , n2 ) = if (¬ litatom (v)) ∨ (v = nil) then nil

else simple-requests (v, n1 , n2 ) endif

Theorem: active-task-requests-simple-requests ((n1 ∈ N) ∧ (n ∈ N)) → (active-task-requests (n, simple-requests (v, n1 , n2 ))

= if n < n1 then nil elseif n < n2 then list (list (v, n, 1 + n, 1)) else nil endif)

Theorem: nthcdr-cons-cons-repeat nthcdr (n, cons (a, cons (a, repeat (m, a)))) = if (2 + m) < n then 0

else repeat ((2 + m) − n, a) endif

Theorem: requests-starts-earlier-simple-requests requests-starts-earlier (simple-requests (v, n1 , n2 ), n) = if n < n2 then simple-requests (v, n1 , n)

else simple-requests (v, n1 , n2 ) endif

Theorem: edf-simple-requests-too-big (z < n2 ) → (edf (z, simple-requests (v, n1 , n2 )) = edf (z, simple-requests (v, n1 , z)))

Theorem: edf-n-simple-requests edf (n, simple-requests (v, 0, n)) = repeat (n, v)

Theorem: good-schedule-repeat-simple good-schedule (repeat (n, v), simple-requests (v, n1 , n))

Theorem: plist-simple-requests plist (simple-requests (v, n1 , n2 )) = simple-requests (v, n1 , n2 )

Theorem: good-edf-bigp-1 ((big-period (pts) ≮ cpu-utilization (pts, big-period (pts))) ∧ periodic-tasksp (pts) ∧ (big-period (pts) = 1) ∧ ((n mod big-period (pts)) = 0)) → good-schedule (edf (n, periodic-tasks-requests (pts, 0, n)),

periodic-tasks-requests (pts, 0, n))

Theorem: good-edf-periodic ((big-period (pts) ≮ cpu-utilization (pts, big-period (pts))) ∧ periodic-tasksp (pts) ∧ ((n mod big-period (pts)) = 0)) → good-schedule (edf (n, periodic-tasks-requests (pts, 0, n)),

periodic-tasks-requests (pts, 0, n))

Event: Make the library "scheduler" and compile it.

Index

active-task-has-later-deadline, 20 active-task-hasnt-earlier-start, 20 active-task-requests, 5, 7, 20–22, 33,

34, 36–40, 43, 47–51, 53, 56–58

active-task-requests-append, 34 active-task-requests-expand-tas

ks-requests, 43 active-task-requests-nnumberp, 36 active-task-requests-not-greate

r, 56 active-task-requests-periodic-t

ask-requests, 56

ask-requests-simple, 56 active-task-requests-requests-st

arts-earlier, 57 active-task-requests-simple-req

uests, 58 add1-sub1-induct, 15 all-litatoms, 19, 20, 23, 24, 27, 28,

41 all-litatoms-append, 28 all-litatoms-firstn, 23 all-litatoms-make-length, 28 all-litatoms-make-simple-schedu

le, 28 all-litatoms-nthcdr, 23 all-litatoms-repeat, 23 all-litatoms-repeat-list, 28 all-litatoms-replace-nth, 23 all-litatoms-substring-schedule, 28 all-nils-or-cars, 25–28, 38, 39, 41, 42 all-nils-or-cars-append, 27 all-nils-or-cars-firstn, 28 all-nils-or-cars-make-element-e

df, 27 all-nils-or-cars-make-length, 27 all-nils-or-cars-make-simple-sc

hedule, 28 all-nils-or-cars-nlistp, 26 all-nils-or-cars-plist, 27 all-nils-or-cars-plist2, 38 all-nils-or-cars-repeat, 28 all-nils-or-cars-repeat-list, 27 all-nils-or-cars-replace-nth, 26 all-nils-or-cars-replace-nth-rep

lace-nth, 27 all-nils-or-cars-substring-sche

dule, 28 all-non-nil-corresponding, 19, 23–27,

41 all-non-nil-corresponding-cons, 24 all-non-nil-corresponding-perio

dic-requests, 26 all-non-nil-corresponding-repla

ce-replace, 24 ce-simple, 24

append-nil, 7

append-remove-until-list-until, 8 assoc-append, 29 assoc-append-simple, 38 assoc-expand-tasks, 13 assoc-nth-pts, 26 assoc-periodic-task-requests, 29 assoc-periodic-tasks-requests, 29 assoc-plist, 38 assoc-unfulfilled-expanded-non-

overlapping, 46

bagint, 9

bagint-singleton, 9

big-period, 5, 9, 12, 13, 30, 42, 54–

59 big-period-expand-tasks, 54

car-append, 36

car-corresponding-request, 20 car-corresponding-request-bette

r, 25 car-edf-simple, 39 car-least-deadline-expand-tasks

-requests, 51 car-make-element-edf, 40 car-make-element-simple, 40 car-make-schedule-edf-simple, 39 car-nthcdr, 19 car-repeat, 39 car-replace-nth, 24 cars-non-nil-litatoms, 18, 20–25, 27–

29, 41 cars-non-nil-litatoms-periodic-t

asks, 28 cdr-firstn-cons, 16 cdr-nthcdr-cons, 15 cons-append-hack, 32 cons-nth-nthcdr, 14 corresponding-request, 18–26 corresponding-request-append, 26 corresponding-request-different

-name, 26 corresponding-request-periodic-t

ask, 26 asks, 26

cpu-utilization, 42, 54, 58, 59 cpu-utilization-expand-tasks, 54

deadline, 5, 6 different-lengths-mean-different, 31 double-cdr-induction, 14 double-sub1-cdr-induct, 26 double-sub1-induction, 16 duration, 5

edf, 33, 35–37, 39, 41, 42, 44–46,

49–51, 53, 54, 57–59 edf-n-simple-requests, 59 edf-requests-starts-earlier, 57 edf-schedule-good-for-expanded, 30 edf-simple-expand-tasks-request

s, 53 edf-simple-nlistp, 35 edf-simple-requests-too-big, 59 equal-1-big-period, 58 equal-append, 14 equal-append-a-append-a, 15 equal-append-b-append-b, 32 equal-car-car-hack, 47 equal-car-least-deadline-nil, 51 equal-cdr-cdr-means, 37 equal-cons-repeat, 44 equal-cpu-utilization-0, 58 equal-length-0, 4 equal-lessp-sub1x-y-x-y, 24 equal-nil-expand-list, 50 equal-nil-firstn, 45 equal-nil-periodic-task-request

s, 55 equal-nil-periodic-tasks-request

s, 55 equal-nthcdr-nthcdr-from-nthcdr

-plus1, 35 equal-nthcdr-x-x, 31 equal-occurrences-firstn-nthcdr, 20 equal-occurrences-firstn-times, 46 equal-plist-nil, 32 equal-plus-1, 58 equal-plus-times, 46 equal-remainder-big-period, 55 equal-remainder-sub1-0, 43 equal-repeat-nil, 44 equal-repeat-repeat, 16 equal-repeat-when-nil-not, 41 equal-times-hack, 46 equivalent-corresponding-request

s, 25 every-nth, 30 exp, 54 expand-list, 42, 43, 45, 49, 50, 53 expand-list-0, 45 expand-list-append, 42 expand-list-repeat, 45 expand-tasks, 13, 33, 53, 54 expand-tasks-1, 53 expand-tasks-requests, 31–33, 43, 47–

51, 53 expand-tasks-requests-append, 31 expanded-tasksp, 4, 10–13, 30, 42 expanded-tasksp-expand-task, 13 expanded-tasksp-expand-task-helpe

r, 13 first-instance, 6, 7, 19–22, 25, 36,

37, 39, 40 first-instance-member-unfulfille

d-not-before-start, 22 d-not-past-deadline, 21 d-not-past-deadline-better, 22

first-instance-same-as-member, 37 firstn, 3–5, 10, 11, 14–18, 20, 21, 23,

27, 28, 35, 36, 38–41, 44– 50, 54, 55

firstn-0, 44 firstn-1, 17 firstn-append, 10 firstn-cons, 16 firstn-difference-plus-nthcdr, 45 firstn-edf-simple, 36 firstn-edf-simple-help, 36 firstn-edf-simple-regular, 36 firstn-expand-list, 45 firstn-firstn, 16 firstn-length-list, 10 firstn-make-element-simple, 40 firstn-n-edf-simple-n, 36 firstn-nlistp, 17 firstn-noop, 46 firstn-nthcdr, 44 firstn-nthcdr-edf-plus, 45 firstn-nthcdr-edf-plus-simple, 50 firstn-nthcdr-firstn-induct, 54 firstn-nthcdr-firstn-simple, 54 firstn-nthcdr-too-big, 45 firstn-only-helper, 50 firstn-plus, 46 firstn-repeat, 35 firstn-repeat-list, 10 firstn-replace-nth, 16 firstn-sub1-cdr-make-element, 40 firstn-too-big, 16

good-edf-almost, 58 good-edf-bigp-1, 59 good-edf-for-expanded, 42 good-edf-help, 54 good-edf-periodic, 59 good-edf-with-remainder, 54 good-schedule, 5, 7, 12, 13, 18, 20–

24, 27, 30, 38, 39, 41, 42, 53–55, 58, 59

good-schedule-append, 7

good-schedule-expand-tasks-redu

ces, 53 good-schedule-periodic-task-req

uests, 11 good-schedule-repeat-simple, 59 good-schedule-requests-not-greate

r, 55 good-simple-schedule, 13 good-simple-schedule-sublist, 12

least-deadline, 6, 7, 20–22, 33, 37, 39–41, 48, 49, 51, 53

least-deadline-has-later-deadli

ne, 20 least-deadline-hasnt-earlier-st

art, 21 length, 4, 6–8, 10–17, 19, 23–28, 30–

36, 38, 39, 41–43, 45–47, 54, 58

length-append, 4 length-cons, 32 length-edf-simple, 33 length-expand-list, 43 length-expand-tasks-requests, 31 length-firstn, 4 length-make-element-edf, 7 length-make-length, 10 length-make-schedule-edf, 35 length-make-simple-schedule, 28 length-nthcdr, 4 length-periodic-task-request-in

duct, 31 length-periodic-task-requests, 32 length-plist, 35 length-repeat, 35 length-repeat-list, 7 length-replace-nth, 6 length-substring-schedule, 42 length-swap, 6 lessp-0-length-means, 34 lessp-0-length-means-listp, 27 lessp-1-means, 44 lessp-corresponding-request-dea

dline, 20

dline-linear, 21 lessp-corresponding-request-sta

rt, 21 lessp-difference-special, 10 lessp-equal-times-x-a-x, 32 lessp-first-instance, 7 lessp-first-instance-s, 19 lessp-first-instance2, 36 lessp-firstn-instance-time, 21 lessp-n-1, 25 lessp-occurrences-edf, 46 lessp-occurrences-firstn, 46 lessp-plus-times-hack, 56 lessp-remainder-special, 10 lessp-remove-until, 8 lessp-round-means, 44 lessp-sub1-plus-hack, 44 lessp-times-sub1-sub1, 44 lessp-x-x, 46 list-until, 8, 9 listp-active-task-requests-0, 34 listp-active-task-requests-0-mu

ltiple, 34 listp-append, 31 listp-bagint-with-singleton-imp

lies-member, 9 listp-edf-simple, 36 listp-expand-list, 42 listp-expand-tasks-requests, 31 listp-firstn, 45 listp-nthcdr, 19 listp-plist, 35 listp-remove-until-means-listp, 8 listp-repeat, 34 listp-task-requests, 31 listp-unfulfilled-if-schedule-c

ontains, 38 litatom-caar, 48 litatom-nth, 19 make-element-edf, 6, 7, 23, 24, 27, 35, 37, 39, 40 make-element-edf-preserves-all-

litatoms, 24 make-element-edf-preserves-good

-schedule, 23 make-element-nnumberp, 39 make-length, 3, 10–12, 27, 28 make-schedule-edf, 7, 27, 30, 35, 36,

39, 41, 42 make-schedule-edf-is-edf, 41 make-schedule-edf-is-edf-simple, 41 make-schedule-edf-nlistp, 35 make-schedule-edf-preserves-goo

d-schedule, 27 make-simple-schedule, 3, 12, 13, 28,

30, 42 member-append, 9 member-car-firstn, 17 member-car-schedule, 41 member-car-x-x, 11 member-corresponding-request, 22 member-corresponding-request-nt

h, 19 member-corresponding-request-si

mplify, 25 member-corresponding-request2, 25 member-deadline-induct, 22 member-deadline-not-less-than-le

ast-deadline, 22 member-expanded, 10 member-expanded-tasksp-means, 12 member-firstn-lessp, 20 member-firstn-means-lessp-first

-instance, 21 member-firstn-only-if-member, 17 member-least-deadline, 20 member-least-deadline-better, 41 member-least-deadline-unfulfille

d, 21 member-means-all-cars-not-litat

oms, 21 member-nil-periodic-task-request

s, 41 member-nil-periodic-tasks-reque

sts, 41 member-nth, 14 member-nth-firstn, 17 member-nth-firstn-induction, 17 member-nth-firstn-nthcdr, 17 member-nthcdr-from-cdr, 19 member-nthcdr-only-if-member, 18 member-repeat, 11 member-replace-nth, 15 member-sublistp, 12 member-substring-schedule, 11 member-x-firstn-cons-x, 18

name, 4, 5, 33 nlistp-nthcdr, 15 no-unfulfilled-active-task-if-ni

l, 39 l-help, 38

no-unfulfilled-active-task-indu

ct, 37 non-overlapping-requests, 14, 17, 19,

23, 24, 27, 30, 41, 47–51, 53

non-overlapping-requests-cdr, 17 non-overlapping-requests-means, 17 non-overlapping-requests-periodi

c-tasks-requests, 30 non-overlapping-requests2, 14, 17, 19,

27, 29, 30 non-overlapping-requests2-appen

d, 27 d-arg2, 29

non-overlapping-requests2-cdr, 17 non-overlapping-requests2-cons-t

oo-big, 30 non-overlapping-requests2-membe

r, 19 non-overlapping-requests2-perio

dic-task, 30 dic-tasks, 30

non-overlapping-requests2-value -all-cars, 29 non-overlapping-requests3, 13, 14, 17–

19, 22, 25, 29, 30, 46 non-overlapping-requests3-appen

d, 29 non-overlapping-requests3-membe

r, 19 non-overlapping-requests3-name-

difference, 30 non-overlapping-requests3-perio

dic-task, 29 non-overlapping-requests3-simple, 22 non-overlapping-requests3-task-

name-difference, 29 not-assoc-car-req, 47 not-corresponding-request-means, 24

-nil, 23 not-equal-car-least-deadline, 48 not-equal-car-least-deadline-spe

cial, 48 not-member-nthcdr-add1, 47 not-numberp-corresponding, 21 nth, 4, 6, 14–20, 22–26, 35–40, 44,

47 nth-append, 36 nth-cons, 44 nth-edf-simple, 37 nth-edf-simple-simpler, 36 nth-first-instance, 25 nth-first-instance-simple, 20 nth-firstn, 16 nth-make-element-edf, 37 nth-make-element-edf-sub1, 40 nth-make-element-simple, 40 nth-make-schedule-edf-simple, 36 nth-nthcdr, 15 nth-replace-nth, 18 nth-too-big, 23 nthcdr, 4, 5, 10, 14–21, 23, 25, 30,

31, 35, 37, 39–41, 43–50, 54, 59

nthcdr-1, 15 nthcdr-append, 10 nthcdr-cons-cons-repeat, 59 nthcdr-cons-firstn, 17 nthcdr-expand-induct, 45 nthcdr-expand-list, 45 nthcdr-firstn-plus, 15 nthcdr-is-nil, 43 nthcdr-n-cons-firstn-n, 40 nthcdr-nthcdr, 15 nthcdr-repeat, 17 nthcdr-repeat-list, 10 nthcdr-repeat-list-induct, 10 nthcdr-replace-nth, 16 nthcdr-sub1-firstn-plus, 17 nthcdr-x-edf-x, 44 nthcdr-x-firstn-x, 44 numberp-cadar, 48 numberp-first-instance, 39

occurrences, 5, 10, 11, 15, 20, 45–49 occurrences-append, 10 occurrences-edf-satisfied, 49 occurrences-expand-list, 45 occurrences-hack, 47 occurrences-hack2, 47 occurrences-make-length, 11 occurrences-repeat, 11 occurrences-repeat-list, 11 occurrences-replace-nth, 15 occurrences-substring-schedule, 11 overlapping-non-overlapping3-me

ans, 46

periodic-task-requests, 2, 3, 12, 26,

29–34, 38, 41, 55–58 periodic-task-requests-as-simple

-requests, 58 periodic-task-requests-expand, 32 periodic-task-requests-simple, 56 periodic-taskp, 2, 26, 31, 32, 34, 38,

55, 56, 58 periodic-tasks-requests, 2, 3, 12, 13,

26–30, 33, 34, 38, 39, 41, 42, 54–59

periodic-tasks-requests-expand, 33 periodic-tasks-requests-simple, 12 periodic-tasksp, 2, 9, 11–13, 26–28,

30, 33, 34, 38, 39, 41, 42, 53–59

periodic-tasksp-append-car, 38 periodic-tasksp-expand-tasks, 13 periodic-tasksp-means-cars-non-

nil-litatoms, 28 plist, 4, 7, 10, 14, 16, 26, 27, 32,

34, 35, 38, 41–43, 46, 50, 55–59 plist-active-task-requests, 56 plist-append, 35 plist-edf-simple, 35 plist-expand-list, 43 plist-expand-tasks-requests, 32 plist-firstn, 14 plist-make-element-edf, 35 plist-make-simple-schedule, 42 plist-nthcdr, 43 plist-periodic-task-requests, 32 plist-repeat, 16 plist-repeat-list, 7 plist-replace-nth2, 35 plist-requests-deadlines, 55 plist-requests-starts-earlier, 57 plist-simple-requests, 59 plist-swap, 35

quotient-add1-plus-special, 43 quotient-difference-special, 53 quotient-plus-add1-hack, 43

remainder-add1-plus-special, 43 remainder-big-period-cdr, 9 remainder-big-period-sublist, 9 remainder-from-exp, 54 remainder-hack, 51 remainder-period-0-if-big-perio

d, 55 remainder-period-if-remainder-bi

g-period, 12 remainder-plus-add1-hack, 43 remove-until, 8, 9, 41 remove-until-append, 8 repeat, 3, 11, 16, 17, 23, 26, 28, 34–

36, 39, 41–45, 53, 59 repeat-1, 43 repeat-list, 3, 7, 9–12, 27, 28 repeat-list-plus, 9 replace-nth, 6, 14–16, 18, 23, 24, 26,

27, 35, 39 replace-nth-first-instance-nnum

berp, 39 replace-nth-idempotent, 14 replace-nth-nlistp, 35 replace-nth-replace-nth, 14 request-time, 5 requests-deadlines-append, 55 requests-deadlines-not-greater, 54–56 requests-deadlines-not-greater-pe

riodic-help, 55 riodic-rewrite, 56 riodic-task, 55

requests-deadlines-periodic-tas

k-simple, 55 requests-starts-earlier, 57, 59 requests-starts-earlier-append, 57 requests-starts-earlier-periodi

c-task, 57 c-tasks, 57

requests-starts-earlier-simple-requests, 59

simple-requests, 58, 59 sublistp, 8, 9, 12, 19–21, 41, 49–51,

53, 55, 57 sublistp-active-task-requests, 21 sublistp-append, 9 sublistp-append-induct, 8, 9 sublistp-cdr1, 9 sublistp-cdr2, 9 sublistp-cons-rewrite, 8 sublistp-remove-until, 41 sublistp-unfulfilled, 20 sublistp-x-x, 12 substring-schedule, 3, 11–13, 28, 30,

42 swap, 6, 7, 15, 18, 23, 35 swap-commutative, 15 swap-preserves-good-schedule, 18 swap-preserves-good-schedule-si

mple, 22

task-abbr, 5 times-1-arg2, 44 times-quotient-quotient-special, 11 tk-duration, 2, 42 tk-name, 1, 2 tk-period, 1, 2, 5, 42 transitivity-of-append, 9

unfulfilled, 5, 7, 20–22, 33, 34, 36– 40, 47–51, 53

unfulfilled-0, 34 unfulfilled-0-edf, 51 unfulfilled-0-expand-tasks-reque

sts, 51 unfulfilled-append, 37 unfulfilled-expand-list, 50 unfulfilled-expanded-on-line, 49 unfulfilled-expanded-on-line-be

ginning, 51 unfulfilled-nnumberp, 36 unfulfilled-schedule-first-part

-only, 36 unfulfilled-sub1-expanded-on-li

ne, 50 unfulfilled-task-later-in-good-

schedule, 20 unfulfilled-too-big, 51 unfulfilled-too-big-sub1, 51

valid-requests, 33, 34, 41, 47–51, 53,

55 valid-requests-active-task-reque

sts, 34 valid-requests-append, 34 valid-requests-expand-tasks-req

uests, 48 valid-requests-periodic-task, 34 valid-requests-periodic-tasks, 34 valid-requests-sublistp, 50 valid-requests-unfulfilled, 48 value-all-cars, 29 value-all-cars-periodic-task-req

uests, 29

zerop-big-period, 13