Event: Start with the library "c-signal".

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                           ;;
;;                          EXACT-TIME PROG2 CASE                            ;;
;;                                                                           ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: prog2-meaning-r-2 (car (stmt) = 'prog2-mg) → (mg-meaning-r (stmt, proc-list, mg-state, n, sizes)

= if n ≃ 0 then signal-system-error (mg-state, 'timed-out) elseif ¬ normal (mg-state) then mg-state elseif resources-inadequatep (stmt, proc-list, sizes) then signal-system-error (mg-state, 'resource-error) else mg-meaning-r (prog2-right-branch (stmt), proc-list, mg-meaning-r (prog2-left-branch (stmt), proc-list, mg-state, n − 1, sizes),

n − 1,

sizes) endif)

Theorem: mg-meaning-r-prog2-left-non-normal ((car (stmt) = 'prog2-mg) ∧ (cc (mg-state) = 'normal) ∧ (¬ resource-errorp (mg-meaning-r (stmt, proc-list, mg-state, n, sizes))) ∧ (¬ normal (mg-meaning-r (prog2-left-branch (stmt),

proc-list, mg-state, n − 1, sizes))))

→ (mg-meaning-r (stmt, proc-list, mg-state, n, sizes)

= mg-meaning-r (prog2-left-branch (stmt), proc-list, mg-state, n − 1, sizes))

Theorem: prog2-translation-2 (car (stmt) = 'prog2-mg)

→ (translate (cinfo, cond-list, stmt, proc-list)

= translate (translate (cinfo, cond-list, prog2-left-branch (stmt), proc-list),

cond-list,

prog2-right-branch (stmt), proc-list))

Theorem: prog2-left-branch-doesnt-halt ((car (stmt) = 'prog2-mg) ∧ normal (mg-state) ∧ (¬ resource-errorp (mg-meaning-r (stmt, proc-list, mg-state, n, sizes)))) → (mg-psw (mg-meaning-r (prog2-left-branch (stmt),

proc-list, mg-state, n − 1, sizes))

    = 'run)

Theorem: prog2-right-branch-doesnt-halt ((car (stmt) = 'prog2-mg) ∧ normal (mg-state) ∧ normal (mg-meaning-r (prog2-left-branch (stmt),

proc-list, mg-state, n − 1, sizes))

∧ (¬ resource-errorp (mg-meaning-r (stmt, proc-list, mg-state, n, sizes)))) → (mg-psw (mg-meaning-r (prog2-right-branch (stmt),

proc-list,

mg-meaning-r (prog2-left-branch (stmt), proc-list, mg-state, n − 1, sizes),

n − 1, sizes))

    = 'run)

Theorem: clock-prog2-left-non-normal ((car (stmt) = 'prog2-mg) ∧ (cc (mg-state) = 'normal) ∧ (¬ resource-errorp (mg-meaning-r (stmt, proc-list, mg-state, n, sizes))) ∧ (¬ normal (mg-meaning-r (prog2-left-branch (stmt), proc-list, mg-state, n − 1, sizes))))

→ (clock (stmt, proc-list, mg-state, n) = clock (prog2-left-branch (stmt), proc-list, mg-state, n − 1))

Theorem: prog2-code-rewrite ((car (stmt) = 'prog2-mg) ∧ ok-translation-parameters (cinfo, t-cond-list, stmt, proc-list, y)) → (append (code (translate (cinfo,

t-cond-list, prog2-left-branch (stmt), proc-list)),

append (code (translate (nullify (translate (nullify (cinfo), t-cond-list, prog2-left-branch (stmt), proc-list)),

t-cond-list, prog2-right-branch (stmt), proc-list)),

y))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)), y))

Event: Disable prog2-code-rewrite.

Theorem: prog2-left-branch-translation-parameters-ok ((car (stmt) = 'prog2-mg) ∧ ok-translation-parameters (cinfo, t-cond-list, stmt, proc-list, code2 )) → ok-translation-parameters (cinfo,

t-cond-list, prog2-left-branch (stmt), proc-list, append (code (translate (nullify (translate (nullify (cinfo),

t-cond-list,

prog2-left-branch (stmt), proc-list)),

t-cond-list, prog2-right-branch (stmt), proc-list)),

code2 ))

Event: Disable prog2-left-branch-translation-parameters-ok.

Theorem: prog2-left-branch-code-body-rewrite ((car (stmt) = 'prog2-mg) ∧ ok-translation-parameters (cinfo, t-cond-list, stmt, proc-list, code2 ) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 )))

→ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, prog2-left-branch (stmt), proc-list)),

append (code (translate (nullify (translate (nullify (cinfo), t-cond-list, prog2-left-branch (stmt), proc-list)),

t-cond-list,

prog2-right-branch (stmt), proc-list)),

code2 )))

Event: Disable prog2-left-branch-code-body-rewrite.

Theorem: prog2-nonnormal-left-state2-equals-final ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'prog2-mg) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-translation-parameters (cinfo, t-cond-list, stmt, proc-list, code2 ) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ cond-subsetp (r-cond-list, t-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ plistp (temp-stk) ∧ listp (ctrl-stk) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state))

∧ signatures-match (mg-alist (mg-state), name-alist) ∧ normal (mg-state) ∧ all-cars-unique (mg-alist (mg-state)) ∧ (¬ resource-errorp (mg-meaning-r (stmt,

proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))))

∧ (¬ normal (mg-meaning-r (prog2-left-branch (stmt), proc-list, mg-state, n − 1, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))))

→ (p-state (tag ('pc,

cons (subr,

if normal (mg-meaning-r (prog2-left-branch (stmt), proc-list, mg-state, n − 1, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

then length (code (translate (cinfo, t-cond-list, prog2-left-branch (stmt), proc-list))) else find-label (fetch-label (cc (mg-meaning-r (prog2-left-branch (stmt),

proc-list, mg-state, n − 1, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

label-alist (translate (cinfo, t-cond-list, prog2-left-branch (stmt), proc-list))),

append (code (translate (cinfo, t-cond-list, prog2-left-branch (stmt), proc-list)),

append (code (translate (nullify (translate (nullify (cinfo), t-cond-list, prog2-left-branch (stmt),

proc-list)),

t-cond-list,

prog2-right-branch (stmt), proc-list)),

code2 ))) endif)),

ctrl-stk, map-down-values (mg-alist (mg-meaning-r (prog2-left-branch (stmt),

proc-list, mg-state, n − 1, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-meaning-r (prog2-left-branch (stmt), proc-list, mg-state, n − 1, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run)

= p-state (tag ('pc,

cons (subr,

if normal (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

then length (code (translate (cinfo, t-cond-list, stmt, proc-list)))

else find-label (fetch-label (cc (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

label-alist (translate (cinfo, t-cond-list, stmt, proc-list))),

append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 )) endif)),

ctrl-stk, map-down-values (mg-alist (mg-meaning-r (stmt,

proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Event: Disable prog2-nonnormal-left-state2-equals-final.

Theorem: prog2-right-branch-translation-parameters-ok ((car (stmt) = 'prog2-mg) ∧ ok-translation-parameters (cinfo, t-cond-list, stmt, proc-list, code2 )) → ok-translation-parameters (translate (cinfo,

t-cond-list,

prog2-left-branch (stmt), proc-list),

t-cond-list,

prog2-right-branch (stmt), proc-list, code2 )

Event: Disable prog2-right-branch-translation-parameters-ok.

Theorem: prog2-right-branch-hyps ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'prog2-mg) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-translation-parameters (cinfo, t-cond-list, stmt, proc-list, code2 ) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ cond-subsetp (r-cond-list, t-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ plistp (temp-stk) ∧ listp (ctrl-stk) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ normal (mg-state) ∧ all-cars-unique (mg-alist (mg-state)) ∧ (¬ resource-errorp (mg-meaning-r (stmt,

proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))))

∧ normal (mg-meaning-r (prog2-left-branch (stmt), proc-list, mg-state, n − 1, list (length (temp-stk), p-ctrl-stk-size (ctrl-stk)))))

→ (ok-mg-statement (prog2-right-branch (stmt), r-cond-list, name-alist,

proc-list)

∧ ok-translation-parameters (translate (cinfo, t-cond-list, prog2-left-branch (stmt), proc-list),

t-cond-list,

prog2-right-branch (stmt), proc-list, code2 )

∧ ok-mg-statep (mg-meaning-r (prog2-left-branch (stmt), proc-list, mg-state, n − 1, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))),

r-cond-list)

∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (translate (cinfo, t-cond-list, prog2-left-branch (stmt), proc-list),

t-cond-list,

prog2-right-branch (stmt), proc-list)),

code2 ))

∧ mg-vars-list-ok-in-p-state (mg-alist (mg-meaning-r (prog2-left-branch (stmt), proc-list, mg-state, n − 1, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)),

mg-alist (mg-meaning-r (prog2-left-branch (stmt), proc-list, mg-state, n − 1, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))))

∧ signatures-match (mg-alist (mg-meaning-r (prog2-left-branch (stmt), proc-list, mg-state, n − 1, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

name-alist)

∧ all-cars-unique (mg-alist (mg-meaning-r (prog2-left-branch (stmt), proc-list, mg-state, n − 1, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))))

∧ (¬ resource-errorp (mg-meaning-r (prog2-right-branch (stmt), proc-list, mg-meaning-r (prog2-left-branch (stmt), proc-list, mg-state, n − 1, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))),

n − 1,

list (length (temp-stk), p-ctrl-stk-size (ctrl-stk))))))

Theorem: prog2-state2-equals-state3 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'prog2-mg) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-translation-parameters (cinfo, t-cond-list, stmt, proc-list, code2 ) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ cond-subsetp (r-cond-list, t-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ plistp (temp-stk) ∧ listp (ctrl-stk) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist)

∧ normal (mg-state) ∧ all-cars-unique (mg-alist (mg-state)) ∧ (¬ resource-errorp (mg-meaning-r (stmt,

proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))))

∧ normal (mg-meaning-r (prog2-left-branch (stmt), proc-list, mg-state, n − 1, list (length (temp-stk), p-ctrl-stk-size (ctrl-stk)))))

→ (p-state (tag ('pc,

cons (subr,

if normal (mg-meaning-r (prog2-left-branch (stmt), proc-list, mg-state, n − 1, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

then length (code (translate (cinfo, t-cond-list, prog2-left-branch (stmt), proc-list))) else find-label (fetch-label (cc (mg-meaning-r (prog2-left-branch (stmt),

proc-list, mg-state, n − 1, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

label-alist (translate (cinfo, t-cond-list, prog2-left-branch (stmt), proc-list))),

append (code (translate (cinfo, t-cond-list, prog2-left-branch (stmt), proc-list)),

append (code (translate (nullify (translate (nullify (cinfo), t-cond-list, prog2-left-branch (stmt), proc-list)),

t-cond-list, prog2-right-branch (stmt), proc-list)),

code2 ))) endif)),

ctrl-stk, map-down-values (mg-alist (mg-meaning-r (prog2-left-branch (stmt),

proc-list, mg-state, n − 1, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-meaning-r (prog2-left-branch (stmt), proc-list, mg-state, n − 1, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run)

= map-down (mg-meaning-r (prog2-left-branch (stmt), proc-list, mg-state, n − 1, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))),

proc-list, ctrl-stk, temp-stk, tag ('pc,

cons (subr,

length (code (translate (cinfo, t-cond-list, prog2-left-branch (stmt), proc-list))))),

t-cond-list))

Event: Disable prog2-state2-equals-state3.

Theorem: prog2-state4-equals-final ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

∧ (car (stmt) = 'prog2-mg) ∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-translation-parameters (cinfo, t-cond-list, stmt, proc-list, code2 ) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ cond-subsetp (r-cond-list, t-cond-list) ∧ (code (translate-def-body (assoc (subr, proc-list), proc-list))

= append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 ))

∧ user-defined-procp (subr, proc-list) ∧ plistp (temp-stk) ∧ listp (ctrl-stk) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk)

∧ no-p-aliasing (bindings (top (ctrl-stk)), mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ normal (mg-state) ∧ all-cars-unique (mg-alist (mg-state)) ∧ (¬ resource-errorp (mg-meaning-r (stmt,

proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))))

∧ normal (mg-meaning-r (prog2-left-branch (stmt), proc-list, mg-state, n − 1, list (length (temp-stk), p-ctrl-stk-size (ctrl-stk)))))

→ (p-state (tag ('pc,

cons (subr,

if normal (mg-meaning-r (prog2-right-branch (stmt), proc-list, mg-meaning-r (prog2-left-branch (stmt), proc-list, mg-state, n − 1, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))),

n − 1, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

then length (code (translate (translate (cinfo, t-cond-list, prog2-left-branch (stmt), proc-list),

t-cond-list, prog2-right-branch (stmt), proc-list)))

else find-label (fetch-label (cc (mg-meaning-r (prog2-right-branch (stmt), proc-list, mg-meaning-r (prog2-left-branch (stmt),

proc-list, mg-state, n − 1, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))),

n − 1, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

label-alist (translate (translate (cinfo, t-cond-list, prog2-left-branch (stmt), proc-list),

t-cond-list,

prog2-right-branch (stmt), proc-list))),

append (code (translate (translate (cinfo, t-cond-list, prog2-left-branch (stmt), proc-list),

t-cond-list, prog2-right-branch (stmt), proc-list)),

code2 )) endif)),

ctrl-stk, map-down-values (mg-alist (mg-meaning-r (prog2-right-branch (stmt),

proc-list, mg-meaning-r (prog2-left-branch (stmt),

proc-list, mg-state, n − 1, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))),

n − 1,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-meaning-r (prog2-right-branch (stmt), proc-list, mg-meaning-r (prog2-left-branch (stmt), proc-list, mg-state, n − 1, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))),

n − 1,

list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run)

= p-state (tag ('pc,

cons (subr,

if normal (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk))))

then length (code (translate (cinfo, t-cond-list, stmt, proc-list)))

else find-label (fetch-label (cc (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))), label-alist (translate (cinfo,

t-cond-list, stmt, proc-list))),

append (code (translate (cinfo, t-cond-list, stmt, proc-list)),

code2 )) endif)),

ctrl-stk, map-down-values (mg-alist (mg-meaning-r (stmt,

proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

bindings (top (ctrl-stk)), temp-stk),

translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-meaning-r (stmt, proc-list, mg-state, n, list (length (temp-stk),

p-ctrl-stk-size (ctrl-stk)))),

t-cond-list))),

mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Event: Disable prog2-state4-equals-final.

Theorem: prog2-normal-left-exact-time-schema ((stmt-time = (left-time + right-time)) ∧ (p (initial, left-time) = state2 ) ∧ (state2 = state3 ) ∧ (p (state3 , right-time) = state4 ) ∧ (state4 = final)) → (p (initial, stmt-time) = final)

Event: Disable prog2-normal-left-exact-time-schema.

(prove-lemma exact-time-lemma-prog2-case (rewrite)
      (implies
(and
(not (zerop n))
(not (resources-inadequatep stmt proc-list
    (list (length temp-stk)
  (p-ctrl-stk-size ctrl-stk))))
(equal (car stmt) 'prog2-mg)
(ok-mg-statement stmt r-cond-list name-alist proc-list)
(ok-mg-def-plistp proc-list)
(ok-translation-parameters cinfo t-cond-list stmt proc-list code2)
(ok-mg-statep mg-state r-cond-list)
(cond-subsetp r-cond-list t-cond-list)
(equal (code (translate-def-body (assoc subr proc-list)
 proc-list))
(append (code (translate cinfo t-cond-list stmt proc-list))
code2))
(user-defined-procp subr proc-list)
(plistp temp-stk)
(listp ctrl-stk)
(mg-vars-list-ok-in-p-state (mg-alist mg-state)
    (bindings (top ctrl-stk))
    temp-stk)
(no-p-aliasing (bindings (top ctrl-stk))
(mg-alist mg-state))
(signatures-match (mg-alist mg-state)
  name-alist)
(normal mg-state)
(all-cars-unique (mg-alist mg-state))
(not (resource-errorp (mg-meaning-r stmt proc-list mg-state n
    (list (length temp-stk)
  (p-ctrl-stk-size ctrl-stk)))))
(implies
(and
 (ok-mg-statement (prog2-left-branch stmt)
  r-cond-list name-alist proc-list)
 (ok-mg-def-plistp proc-list)
 (ok-translation-parameters cinfo t-cond-list
    (prog2-left-branch stmt)
    proc-list
    (append (code (translate (nullify (translate (nullify cinfo)
 t-cond-list

(prog2-left-branch stmt)
proc-list))
    t-cond-list
    (prog2-right-branch stmt)
    proc-list))
   code2))
(ok-mg-statep mg-state r-cond-list)
(cond-subsetp r-cond-list t-cond-list)
(equal
 (code (translate-def-body (assoc subr proc-list)
   proc-list))
 (append
  (code (translate cinfo t-cond-list
   (prog2-left-branch stmt)
   proc-list))
  (append (code (translate (nullify (translate (nullify cinfo)
t-cond-list
(prog2-left-branch stmt)
proc-list))
   t-cond-list
   (prog2-right-branch stmt)
   proc-list))
  code2)))
(user-defined-procp subr proc-list)
(plistp temp-stk)
(listp ctrl-stk)
(mg-vars-list-ok-in-p-state (mg-alist mg-state)
    (bindings (top ctrl-stk))
    temp-stk)
(no-p-aliasing (bindings (top ctrl-stk))
(mg-alist mg-state))
(signatures-match (mg-alist mg-state)
  name-alist)
(normal mg-state)
(all-cars-unique (mg-alist mg-state))
(not (resource-errorp (mg-meaning-r (prog2-left-branch stmt)
    proc-list mg-state
    (sub1 n)
    (list (length temp-stk)
  (p-ctrl-stk-size ctrl-stk))))))
(equal
(p (map-down mg-state proc-list ctrl-stk temp-stk               ;; state1
     (tag 'pc
  (cons subr (length (code cinfo))))

    t-cond-list)
  (clock (prog2-left-branch stmt)                             ;; left-time
 proc-list mg-state
 (sub1 n)))
(p-state;; state2
(tag 'pc
(cons subr
   (if
(normal (mg-meaning-r (prog2-left-branch stmt)
proc-list mg-state
(sub1 n)
(list (length temp-stk)
   (p-ctrl-stk-size ctrl-stk))))
(length (code (translate cinfo t-cond-list
(prog2-left-branch stmt)
proc-list)))
(find-label
(fetch-label (cc (mg-meaning-r (prog2-left-branch stmt)
proc-list mg-state
(sub1 n)
(list (length temp-stk)
   (p-ctrl-stk-size ctrl-stk))))
   (label-alist (translate cinfo t-cond-list
   (prog2-left-branch stmt)
   proc-list)))
(append
(code (translate cinfo t-cond-list
(prog2-left-branch stmt)
proc-list))
(append (code (translate (nullify (translate (nullify cinfo)
    t-cond-list
    (prog2-left-branch stmt)
    proc-list))
t-cond-list
(prog2-right-branch stmt)
proc-list))
code2))))))
ctrl-stk
(map-down-values
 (mg-alist (mg-meaning-r (prog2-left-branch stmt)
 proc-list mg-state
 (sub1 n)
 (list (length temp-stk)
(p-ctrl-stk-size ctrl-stk))))

  (bindings (top ctrl-stk))
  temp-stk)
 (translate-proc-list proc-list)
 (list
  (list 'c-c
(mg-cond-to-p-nat (cc (mg-meaning-r (prog2-left-branch stmt)
    proc-list mg-state
    (sub1 n)
    (list (length temp-stk)
  (p-ctrl-stk-size ctrl-stk))))
  t-cond-list)))
 (MG-MAX-CTRL-STK-SIZE)
 (MG-MAX-TEMP-STK-SIZE)
 (MG-WORD-SIZE)
 'run)))
(implies
(and
(ok-mg-statement (prog2-right-branch stmt)
 r-cond-list name-alist proc-list)
(ok-mg-def-plistp proc-list)
(ok-translation-parameters (translate cinfo t-cond-list
(prog2-left-branch stmt)
proc-list)
   t-cond-list
   (prog2-right-branch stmt)
   proc-list code2)
(ok-mg-statep (mg-meaning-r (prog2-left-branch stmt)
    proc-list mg-state
    (sub1 n)
    (list (length temp-stk)
  (p-ctrl-stk-size ctrl-stk)))
r-cond-list)
(cond-subsetp r-cond-list t-cond-list)
(equal (code (translate-def-body (assoc subr proc-list)
 proc-list))
(append (code (translate (translate cinfo t-cond-list
   (prog2-left-branch stmt)
   proc-list)
t-cond-list
(prog2-right-branch stmt)
proc-list))
code2))
(user-defined-procp subr proc-list)
(plistp temp-stk)

(listp ctrl-stk)
(mg-vars-list-ok-in-p-state
(mg-alist (mg-meaning-r (prog2-left-branch stmt)
proc-list mg-state
(sub1 n)
(list (length temp-stk)
(p-ctrl-stk-size ctrl-stk))))
(bindings (top ctrl-stk))
temp-stk)
(no-p-aliasing (bindings (top ctrl-stk))
(mg-alist (mg-meaning-r (prog2-left-branch stmt)
proc-list mg-state
(sub1 n)
(list (length temp-stk)
    (p-ctrl-stk-size ctrl-stk)))))
(signatures-match
(mg-alist (mg-meaning-r (prog2-left-branch stmt)
proc-list mg-state
(sub1 n)
(list (length temp-stk)
(p-ctrl-stk-size ctrl-stk))))
name-alist)
(normal (mg-meaning-r (prog2-left-branch stmt)
proc-list mg-state
(sub1 n)
(list (length temp-stk)
   (p-ctrl-stk-size ctrl-stk))))
(all-cars-unique
(mg-alist (mg-meaning-r (prog2-left-branch stmt)
proc-list mg-state
(sub1 n)
(list (length temp-stk)
(p-ctrl-stk-size ctrl-stk)))))
(not
(resource-errorp
 (mg-meaning-r (prog2-right-branch stmt)
proc-list
(mg-meaning-r (prog2-left-branch stmt)
proc-list mg-state
(sub1 n)
(list (length temp-stk)
   (p-ctrl-stk-size ctrl-stk)))
(sub1 n)
(list (length temp-stk)

(p-ctrl-stk-size ctrl-stk))))))
 (equal
  (p (map-down (mg-meaning-r (prog2-left-branch stmt)               ;; state3
     proc-list mg-state
     (sub1 n)
     (list (length temp-stk)
   (p-ctrl-stk-size ctrl-stk)))
       proc-list ctrl-stk temp-stk
       (tag 'pc
    (cons subr
  (length (code (translate cinfo t-cond-list
   (prog2-left-branch stmt)
   proc-list)))))
       t-cond-list)
     (clock (prog2-right-branch stmt)                              ;; right-time
    proc-list
    (mg-meaning-r (prog2-left-branch stmt)
  proc-list mg-state
  (sub1 n)
  (list (length temp-stk)
(p-ctrl-stk-size ctrl-stk)))
    (sub1 n)))
  (p-state;; state4
   (tag 'pc
(cons subr
      (if
  (normal (mg-meaning-r (prog2-right-branch stmt)
proc-list
(mg-meaning-r (prog2-left-branch stmt)
      proc-list mg-state
      (sub1 n)
      (list (length temp-stk)
    (p-ctrl-stk-size ctrl-stk)))
(sub1 n)
(list (length temp-stk)
      (p-ctrl-stk-size ctrl-stk))))
  (length (code (translate (translate cinfo t-cond-list
      (prog2-left-branch stmt)
      proc-list)
   t-cond-list
   (prog2-right-branch stmt)
   proc-list)))
(find-label
 (fetch-label

(cc (mg-meaning-r (prog2-right-branch stmt)
  proc-list
  (mg-meaning-r (prog2-left-branch stmt)
proc-list mg-state
(sub1 n)
(list (length temp-stk)
(p-ctrl-stk-size ctrl-stk)))
  (sub1 n)
  (list (length temp-stk)
(p-ctrl-stk-size ctrl-stk))))
(label-alist (translate (translate cinfo t-cond-list
   (prog2-left-branch stmt)
   proc-list)
t-cond-list
(prog2-right-branch stmt)
proc-list)))
(append (code (translate (translate cinfo t-cond-list
   (prog2-left-branch stmt)
   proc-list)
t-cond-list
(prog2-right-branch stmt)
proc-list))
code2)))))
 ctrl-stk
 (map-down-values
  (mg-alist (mg-meaning-r (prog2-right-branch stmt)
  proc-list
  (mg-meaning-r (prog2-left-branch stmt)
proc-list mg-state
(sub1 n)
(list (length temp-stk)
(p-ctrl-stk-size ctrl-stk)))
  (sub1 n)
  (list (length temp-stk)
(p-ctrl-stk-size ctrl-stk))))
  (bindings (top ctrl-stk))
  temp-stk)
 (translate-proc-list proc-list)
 (list
  (list 'c-c
(mg-cond-to-p-nat
 (cc (mg-meaning-r (prog2-right-branch stmt)
   proc-list
   (mg-meaning-r (prog2-left-branch stmt)

proc-list mg-state
(sub1 n)
(list (length temp-stk)
(p-ctrl-stk-size ctrl-stk)))
  (sub1 n)
  (list (length temp-stk)
(p-ctrl-stk-size ctrl-stk))))
t-cond-list)))
(MG-MAX-CTRL-STK-SIZE)
(MG-MAX-TEMP-STK-SIZE)
(MG-WORD-SIZE)
'run))))
(equal
(p (map-down mg-state proc-list ctrl-stk temp-stk                     ;; initial
            (tag 'pc
                 (cons subr (length (code cinfo))))
            t-cond-list)
  (clock stmt proc-list mg-state n))                                 ;; stmt-time
(p-state                                                              ;; final
(tag 'pc
(cons subr
   (if
(normal (mg-meaning-r stmt proc-list mg-state n
(list (length temp-stk)
   (p-ctrl-stk-size ctrl-stk))))
(length (code (translate cinfo t-cond-list stmt proc-list)))
(find-label
(fetch-label (cc (mg-meaning-r stmt proc-list mg-state n
(list (length temp-stk)
   (p-ctrl-stk-size ctrl-stk))))
   (label-alist (translate cinfo t-cond-list stmt
   proc-list)))
(append (code (translate cinfo t-cond-list stmt proc-list))
code2)))))
ctrl-stk
(map-down-values (mg-alist (mg-meaning-r stmt proc-list mg-state n
                                         (list (length temp-stk)
                                               (p-ctrl-stk-size ctrl-stk))))
                 (bindings (top ctrl-stk))
                 temp-stk)
(translate-proc-list proc-list)
(list
 (list 'c-c
(mg-cond-to-p-nat (cc (mg-meaning-r stmt proc-list mg-state n

   (list (length temp-stk)
 (p-ctrl-stk-size ctrl-stk))))
 t-cond-list)))
(MG-MAX-CTRL-STK-SIZE)
(MG-MAX-TEMP-STK-SIZE)
(MG-WORD-SIZE)
'run)))
((instructions
(add-abbreviation @initial
                  (map-down mg-state proc-list ctrl-stk temp-stk
                            (tag 'pc
                                 (cons subr (length (code cinfo))))
                            t-cond-list))
(add-abbreviation @stmt-time
                  (clock stmt proc-list mg-state n))
(add-abbreviation @final
 (p-state
  (tag 'pc
(cons subr
(if
 (normal (mg-meaning-r stmt proc-list mg-state n
(list (length temp-stk)
(p-ctrl-stk-size ctrl-stk))))
 (length (code (translate cinfo t-cond-list stmt proc-list)))
(find-label
(fetch-label (cc (mg-meaning-r stmt proc-list mg-state n
(list (length temp-stk)
(p-ctrl-stk-size ctrl-stk))))
(label-alist (translate cinfo t-cond-list stmt
proc-list)))
(append (code (translate cinfo t-cond-list stmt proc-list))
code2)))))
  ctrl-stk
  (map-down-values
   (mg-alist (mg-meaning-r stmt proc-list mg-state n
   (list (length temp-stk)
 (p-ctrl-stk-size ctrl-stk))))
   (bindings (top ctrl-stk))
   temp-stk)
  (translate-proc-list proc-list)
  (list
   (list 'c-c
 (mg-cond-to-p-nat (cc (mg-meaning-r stmt proc-list mg-state n
(list (length temp-stk)

 (p-ctrl-stk-size ctrl-stk))))
 t-cond-list)))
(MG-MAX-CTRL-STK-SIZE)
(MG-MAX-TEMP-STK-SIZE)
(MG-WORD-SIZE)
'run))
(add-abbreviation @left-time
                (clock (prog2-left-branch stmt)
                       proc-list mg-state
                       (sub1 n)))
(add-abbreviation @state2
(p-state
(tag 'pc
(cons subr
(if
(normal (mg-meaning-r (prog2-left-branch stmt)
proc-list mg-state
(sub1 n)
(list (length temp-stk)
(p-ctrl-stk-size ctrl-stk))))
(length (code (translate cinfo t-cond-list
(prog2-left-branch stmt)
proc-list)))
(find-label
(fetch-label (cc (mg-meaning-r (prog2-left-branch stmt)
proc-list mg-state
(sub1 n)
(list (length temp-stk)
(p-ctrl-stk-size ctrl-stk))))
(label-alist (translate cinfo t-cond-list
(prog2-left-branch stmt)
proc-list)))
(append
(code (translate cinfo t-cond-list
(prog2-left-branch stmt)
proc-list))
(append (code (translate (nullify (translate (nullify cinfo)
t-cond-list
(prog2-left-branch stmt)
proc-list))
t-cond-list
(prog2-right-branch stmt)
proc-list))
code2))))))

ctrl-stk
(map-down-values
(mg-alist (mg-meaning-r (prog2-left-branch stmt)
proc-list mg-state
(sub1 n)
(list (length temp-stk)
(p-ctrl-stk-size ctrl-stk))))
(bindings (top ctrl-stk))
temp-stk)
(translate-proc-list proc-list)
(list
(list 'c-c
(mg-cond-to-p-nat (cc (mg-meaning-r (prog2-left-branch stmt)
proc-list mg-state
(sub1 n)
(list (length temp-stk)
(p-ctrl-stk-size ctrl-stk))))
t-cond-list)))
(MG-MAX-CTRL-STK-SIZE)
(MG-MAX-TEMP-STK-SIZE)
(MG-WORD-SIZE)
'run))
(add-abbreviation @state3
   (map-down (mg-meaning-r (prog2-left-branch stmt)
                           proc-list mg-state
                           (sub1 n)
                           (list (length temp-stk)
                                 (p-ctrl-stk-size ctrl-stk)))
             proc-list ctrl-stk temp-stk
             (tag 'pc
                  (cons subr
                        (length (code (translate cinfo t-cond-list
                                                 (prog2-left-branch stmt)
                                                 proc-list)))))
             t-cond-list))
(add-abbreviation @right-time
               (clock (prog2-right-branch stmt)
                      proc-list
                      (mg-meaning-r (prog2-left-branch stmt)
                                    proc-list mg-state
                                    (sub1 n)
                                    (list (length temp-stk)
                                          (p-ctrl-stk-size ctrl-stk)))
                      (sub1 n)))

(add-abbreviation @state4
(p-state
 (tag 'pc
(cons subr
(if
(normal (mg-meaning-r (prog2-right-branch stmt)
proc-list
(mg-meaning-r (prog2-left-branch stmt)
proc-list mg-state
(sub1 n)
(list (length temp-stk)
  (p-ctrl-stk-size ctrl-stk)))
(sub1 n)
(list (length temp-stk)
(p-ctrl-stk-size ctrl-stk))))
(length (code (translate (translate cinfo t-cond-list
(prog2-left-branch stmt)
proc-list)
 t-cond-list
 (prog2-right-branch stmt)
 proc-list)))
(find-label
(fetch-label
(cc (mg-meaning-r (prog2-right-branch stmt)
  proc-list
  (mg-meaning-r (prog2-left-branch stmt)
proc-list mg-state
(sub1 n)
(list (length temp-stk)
(p-ctrl-stk-size ctrl-stk)))
  (sub1 n)
  (list (length temp-stk)
(p-ctrl-stk-size ctrl-stk))))
(label-alist (translate (translate cinfo t-cond-list
   (prog2-left-branch stmt)
   proc-list)
t-cond-list
(prog2-right-branch stmt)
proc-list)))
(append (code (translate (translate cinfo t-cond-list
   (prog2-left-branch stmt)
   proc-list)
t-cond-list
(prog2-right-branch stmt)

proc-list))
code2)))))
ctrl-stk
(map-down-values
 (mg-alist (mg-meaning-r (prog2-right-branch stmt)
 proc-list
 (mg-meaning-r (prog2-left-branch stmt)
proc-list mg-state
(sub1 n)
(list (length temp-stk)
(p-ctrl-stk-size ctrl-stk)))
 (sub1 n)
 (list (length temp-stk)
(p-ctrl-stk-size ctrl-stk))))
 (bindings (top ctrl-stk))
 temp-stk)
(translate-proc-list proc-list)
(list
 (list 'c-c
(mg-cond-to-p-nat
        (cc (mg-meaning-r (prog2-right-branch stmt)
                          proc-list
                          (mg-meaning-r (prog2-left-branch stmt)
                                        proc-list mg-state
                                        (sub1 n)
                                        (list (length temp-stk)
                                              (p-ctrl-stk-size ctrl-stk)))
                          (sub1 n)
                          (list (length temp-stk)
                                (p-ctrl-stk-size ctrl-stk))))
        t-cond-list)))
(MG-MAX-CTRL-STK-SIZE)
(MG-MAX-TEMP-STK-SIZE)
(MG-WORD-SIZE)
'run))
promote
(demote 19)
(dive 1 1)
push top promote
(claim (not (normal (mg-meaning-r (prog2-left-branch stmt)
                                proc-list mg-state
                                (sub1 n)
                                (list (length temp-stk)
                                      (p-ctrl-stk-size ctrl-stk)))))

(drop 19)
(claim (equal @state2 @final) 0)
(claim (equal @stmt-time @left-time)
       0)
(demote 19 21 22)
drop
(generalize ((@right-time right-time)
             (@left-time left-time)
             (@state4 state4)
             (@state3 state3)
             (@state2 state2)
             (@final final)
             (@stmt-time stmt-time)
             (@initial initial)))
prove
(contradict 22)
(dive 1)
(rewrite clock-prog2-left-non-normal
         (($sizes (list (length temp-stk)
                        (p-ctrl-stk-size ctrl-stk)))))
up s
(demote 16)
s
(contradict 21)
(dive 1)
(rewrite prog2-nonnormal-left-state2-equals-final)
top s-prop
(demote 19)
(dive 1 1)
push top promote
(claim (equal @stmt-time
              (plus @left-time @right-time))
       0)
(claim (equal @state2 @state3) 0)
(claim (equal @state4 @final) 0)
(demote 19 21 22 23 24)
drop
(generalize ((@right-time right-time)
             (@left-time left-time)
             (@state4 state4)
             (@state3 state3)
             (@state2 state2)
             (@final final)

             (@stmt-time stmt-time)
             (@initial initial)))
(use-lemma prog2-normal-left-exact-time-schema)
prove
(contradict 24)
(dive 1)
(rewrite prog2-state4-equals-final)
drop top prove
(contradict 23)
(dive 1)
(rewrite prog2-state2-equals-state3)
top s
(contradict 22)
(dive 1)
(rewrite clock-prog2)
s up
(rewrite plus-equality-lemma1)
(dive 2 3)
(rewrite mg-meaning-equivalence)
top s s
(dive 1)
(rewrite prog2-left-branch-doesnt-halt)
top s split
(rewrite prog2-right-branch-hyps)
(rewrite prog2-right-branch-hyps)
(rewrite prog2-right-branch-hyps)
(dive 1)
(rewrite prog2-right-branch-hyps)
top s
(rewrite prog2-right-branch-hyps)
(rewrite prog2-right-branch-hyps)
(rewrite prog2-right-branch-hyps)
(rewrite prog2-right-branch-hyps)
(dive 1)
(rewrite prog2-right-branch-hyps)
top s
(drop 19)
split
(rewrite ok-prog2-statement)
(rewrite prog2-left-branch-translation-parameters-ok)
(dive 1)
(rewrite prog2-left-branch-code-body-rewrite)
up s s
(dive 1)

(rewrite prog2-left-branch-doesnt-halt)
top s)))

Event: Disable exact-time-lemma-prog2-case.

Event: Make the library "c-prog2".

Index

all-cars-unique, 5, 8, 10, 11, 13

bindings, 4, 6–10, 12, 13, 15, 16

cc, 1, 2, 5–7, 11, 12, 14–16 clock, 3 clock-prog2-left-non-normal, 2 code, 3–16 cond-subsetp, 4, 8, 10, 13

fetch-label, 5, 7, 11, 14, 16 find-label, 6, 7, 12, 14, 16

label-alist, 5, 7, 11, 14, 16 length, 4–16

map-down, 12 map-down-values, 6, 7, 12, 15, 16 mg-alist, 4–13, 15, 16 mg-cond-to-p-nat, 6, 7, 12, 15, 16 mg-max-ctrl-stk-size, 6, 7, 12, 15,

16 mg-max-temp-stk-size, 6, 7, 12, 15,

16 mg-meaning-r, 1–3, 5–16 mg-meaning-r-prog2-left-non-nor

mal, 1 mg-psw, 2 mg-vars-list-ok-in-p-state, 4, 8–10, 13 mg-word-size, 6, 7, 12, 15, 16

no-p-aliasing, 4, 8–10, 13 normal, 1–3, 5, 6, 8, 11, 13–15 nullify, 3–6, 11

ok-mg-def-plistp, 4, 8, 10, 13 ok-mg-statement, 4, 8–10, 13 ok-mg-statep, 4, 8–10, 13 ok-translation-parameters, 3, 4, 7–

10, 13

p, 16 p-ctrl-stk-size, 4–16 p-state, 6, 7, 12, 15, 16 plistp, 4, 8, 10, 13 prog2-code-rewrite, 3 prog2-left-branch, 1–15 prog2-left-branch-code-body-rew

rite, 4 prog2-left-branch-doesnt-halt, 2 prog2-left-branch-translation-p

arameters-ok, 3 prog2-meaning-r-2, 1 prog2-nonnormal-left-state2-equ

als-final, 4 prog2-normal-left-exact-time-sc

hema, 16 prog2-right-branch, 1–4, 6–10, 12–

15 prog2-right-branch-doesnt-halt, 2 prog2-right-branch-hyps, 8 prog2-right-branch-translation-p

arameters-ok, 7 prog2-state2-equals-state3, 10 prog2-state4-equals-final, 13 prog2-translation-2, 1

resource-errorp, 1, 2, 5, 8, 10, 11, 13 resources-inadequatep, 1, 4, 8, 10,

13

signal-system-error, 1

signatures-match, 5, 8, 10, 13

tag, 6, 7, 12, 14, 16

top, 4, 6–10, 12, 13, 15, 16

translate, 2–16

translate-def-body, 4, 8–10, 13 translate-proc-list, 6, 7, 12, 15, 16

user-defined-procp, 4, 8, 10, 13