Event: Start with the library "c-begin". Event: Enable clock-predefined-proc-call-sequence. Event: Enable clock-predefined-proc-call-body-translation. Event: Enable predefined-proc-call-sequence. Event: Disable mg-to-p-simple-literal. Event: Disable ilessp. Event: Disable not-bool. Event: Disable inegate. Event: Disable fix-small-integer. Event: Disable iplus. Event: Disable idifference. Event: Disable signatures-match-preserves-plistp. Theorem: predefined-proc-call-meaning-r-2

 (car (stmt) = 'predefined-proc-call-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-predefined-proc-call (stmt, mg-state) endif)

Theorem: predefined-call-translation-2

 (car (stmt) = 'predefined-proc-call-mg)

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

= add-code (cinfo, predefined-proc-call-sequence (stmt,

label-alist (cinfo))))

Theorem: unlabel-call unlabel (cons ('call, x)) = cons ('call, x)

Theorem: lessp-add1-add1-2 ((1 + (1 + x)) < 2) = f

Theorem: lessp-add1-add1-add1-3 ((1 + (1 + (1 + x))) < 3) = f

;; >> get rid of the extra "d"

Theorem: simple-typed-literalp-mapping-listp simple-typed-literalp (lit, type) → listp (mg-to-p-simple-literal (lit))

Theorem: boolean-mg-to-p-simple-literal

(x ∈ '(true-mg false-mg))

→ (mg-to-p-simple-literal (tag ('boolean-mg, x))

= tag ('bool,

            if x = 'false-mg then 'f

else 't endif))

Theorem: boolean-mg-to-p-simple-literal2 mg-to-p-simple-literal (mg-bool (x)) = tag ('bool,

if ¬ x then 'f else 't endif)

Theorem: mg-to-p-simple-literalp-preserves-untag-equality (simple-typed-literalp (x, type) ∧ simple-typed-literalp (y, type)) → ((untag (mg-to-p-simple-literal (x))

= untag (mg-to-p-simple-literal (y))) = (untag (x) = untag (y)))

Theorem: mg-to-p-simple-literalp-preserves-untag-ilessp (int-literalp (x) ∧ int-literalp (y)) → (ilessp (untag (mg-to-p-simple-literal (x)),

untag (mg-to-p-simple-literal (y))) = ilessp (untag (x), untag (y)))

Theorem: simple-identifiers-have-simple-values (mg-alistp (alist) ∧ simple-identifierp (x, alist)) → simple-typed-literalp (caddr (assoc (x, alist)), cadr (assoc (x, alist)))

Theorem: alist-element-type-conversion (mg-alistp (lst) ∧ simple-identifierp (x, lst)) → (type (mg-to-p-simple-literal (caddr (assoc (x, lst))))

= if cadr (assoc (x, lst)) = 'boolean-mg then 'bool else 'int endif)

Theorem: literal-type-conversion simple-typed-literalp (lit, type) → (type (mg-to-p-simple-literal (lit))

     = if type = 'boolean-mg then 'bool

else 'int endif)

Theorem: int-literals-mapping int-literalp (x) → ((type (mg-to-p-simple-literal (x)) = 'int)

∧ listp (mg-to-p-simple-literal (x))

∧ (cddr (mg-to-p-simple-literal (x)) = nil)

∧ small-integerp (untag (mg-to-p-simple-literal (x)), 32))

Theorem: int-identifiers-have-int-literal-values (mg-alistp (mg-vars) ∧ int-identifierp (x, mg-vars)) → int-literalp (caddr (assoc (x, mg-vars)))

Theorem: boolean-identifiers-have-boolean-literal-values (mg-alistp (mg-vars) ∧ boolean-identifierp (x, mg-vars)) → boolean-literalp (caddr (assoc (x, mg-vars)))

Theorem: length-plistp-2-rewrite (cddr (x) = nil) = length-plistp (x, 2)

Event: Disable length-plistp-2-rewrite.

;; There is no reason why this couldn't be changed to defined-identifierp's
;; rather than simple-identifierp's

Theorem: simple-identifier-mapping (mg-vars-list-ok-in-p-state (mg-vars, bindings, temp-stk) ∧ simple-identifierp (b, mg-vars) ∧ (length (temp-stk) < mg-max-temp-stk-size) ∧ all-cars-unique (mg-vars)) → ((type (value (b, bindings)) = 'nat)

∧ (cddr (value (b, bindings)) = nil)

∧ listp (value (b, bindings))

∧ small-naturalp (untag (value (b, bindings)), 32))

;; I think this is probably redundant.

Theorem: simple-identifier-mapping-2 (mg-vars-list-ok-in-p-state (mg-alist (mg-state), bindings, temp-stk) ∧ simple-identifierp (b, mg-alist (mg-state)) ∧ (length (temp-stk) < mg-max-temp-stk-size) ∧ all-cars-unique (mg-alist (mg-state))) → ((type (value (b, bindings)) = 'nat)

∧ (cddr (value (b, bindings)) = nil)

∧ listp (value (b, bindings))

∧ small-naturalp (untag (value (b, bindings)), 32))

Theorem: simple-identifier-mapping-3 (mg-vars-list-ok-in-p-state (mg-alist, bindings, temp-stk) ∧ definedp (b, mg-alist)) → ((untag (value (b, bindings)) < (1 + length (temp-stk))) = t)

Theorem: simple-identifier-nat-p-objectp (mg-vars-list-ok-in-p-state (mg-alist (mg-state), bindings, temp-stk) ∧ simple-identifierp (b, mg-alist (mg-state)) ∧ (length (temp-stk) < mg-max-temp-stk-size) ∧ all-cars-unique (mg-alist (mg-state)) ∧ (p-word-size (state) = mg-word-size)) → p-objectp-type ('nat, value (b, bindings), state)

Event: Enable mg-var-ok-in-p-state.

Theorem: array-identifier-nat-p-objectp (mg-vars-list-ok-in-p-state (mg-alist, bindings, temp-stk) ∧ definedp (b, mg-alist) ∧ (length (temp-stk) < mg-max-temp-stk-size) ∧ (p-word-size (state) = mg-word-size)) → p-objectp-type ('nat, value (b, bindings), state)

Theorem: int-literalp-mapping int-literalp (x) → (untag (mg-to-p-simple-literal (x)) = untag (x))

Theorem: boolean-literalp-mapping boolean-literalp (x) → (untag (mg-to-p-simple-literal (x))

= if untag (x) = 'false-mg then 'f else 't endif)

Theorem: untag-boolean boolean-literalp (x) → (untag (x) ∈ '(true-mg false-mg))

Theorem: int-literalp-value-small int-literalp (x) → small-integerp (untag (x), 32)

Theorem: small-integerp-mapping small-integerp (x, mg-word-size) → (mg-to-p-simple-literal (tag ('int-mg, x)) = tag ('int, x))

Theorem: special-conditions-mg-cond-to-p-nat (mg-cond-to-p-nat ('routineerror, state) = '(nat 1)) ∧ (mg-cond-to-p-nat ('normal, state) = '(nat 2))

Theorem: fix-small-integer-identity small-integerp (x, n) → (fix-small-integer (x, n) = x)

Theorem: int-literal-int-objectp (int-literalp (x) ∧ (p-word-size (state) = mg-word-size)) → p-objectp-type ('int, mg-to-p-simple-literal (x), state)

Theorem: untag-int-literal-integerp int-literalp (x) → integerp (untag (x))

Theorem: bool-literal-bool-objectp p-objectp-type ('bool, '(bool t), state) ∧ p-objectp-type ('bool, '(bool f), state)

Theorem: bool-literal-bool-objectp2 boolean-literalp (x) → p-objectp-type ('bool, mg-to-p-simple-literal (x), state)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                           ;;
;;             EXACT-TIME LEMMA MG-SIMPLE-VARIABLE-ASSIGNMENT                ;;
;;                                                                           ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: mg-simple-variable-assignment-args-definedp (ok-mg-statement (stmt, r-cond-list, name-alist, proc-list)

 ∧ (car (stmt) = 'predefined-proc-call-mg)
 ∧ (call-name (stmt) = 'mg-simple-variable-assignment)

∧ ok-mg-statep (mg-state, r-cond-list) ∧ signatures-match (mg-alist (mg-state), name-alist)) → (definedp (car (call-actuals (stmt)), mg-alist (mg-state))

∧ definedp (cadr (call-actuals (stmt)), mg-alist (mg-state)))

Theorem: mg-simple-variable-assignment-args-simple-identifierps (ok-mg-statement (stmt, r-cond-list, name-alist, proc-list)

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-assignment)

∧ ok-mg-statep (mg-state, r-cond-list) ∧ signatures-match (mg-alist (mg-state), name-alist)) → (simple-identifierp (car (call-actuals (stmt)), mg-alist (mg-state))

∧ simple-identifierp (cadr (call-actuals (stmt)), mg-alist (mg-state)))

Theorem: mg-simple-variable-assignment-steps-1-2 ((¬ resources-inadequatep (stmt,

proc-list,

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

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

∧ normal (mg-state)) → (p-step (p-step (map-down (mg-state,

proc-list, ctrl-stk, temp-stk, tag ('pc, cons (subr, length (code (cinfo)))), t-cond-list))) = p-state (tag ('pc, cons (subr, length (code (cinfo)) + 2)),

ctrl-stk,

push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

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

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))
;; (call mg-simple-variable-assignment)

Theorem: mg-simple-variable-assignment-step-3 ((¬ resources-inadequatep (stmt,

proc-list,

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

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

∧ normal (mg-state)) → (p-step (p-state (tag ('pc, cons (subr, length (code (cinfo)) + 2)),

ctrl-stk,

push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

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

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

                 'run))

= p-state (tag ('pc,

                  '(mg-simple-variable-assignment . 0)),

push (p-frame (list (cons ('dest,

value (car (call-actuals (stmt)),

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

                              cons ('source,

value (cadr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 3))),

ctrl-stk), map-down-values (mg-alist (mg-state),

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

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))
;; (push-local source)

Theorem: mg-simple-variable-assignment-step-4 ((¬ resources-inadequatep (stmt,

proc-list,

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

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

∧ normal (mg-state)) → (p-step (p-state (tag ('pc,

                     '(mg-simple-variable-assignment . 0)),

push (p-frame (list (cons ('dest, value (car (call-actuals (stmt)),

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

                   cons ('source,

value (cadr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 3))),

ctrl-stk), map-down-values (mg-alist (mg-state),

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

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

   'run))

= p-state (tag ('pc,

    '(mg-simple-variable-assignment . 1)),

push (p-frame (list (cons ('dest,

value (car (call-actuals (stmt)),

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

                cons ('source,

value (cadr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 3))),

ctrl-stk), push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

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

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Theorem: mg-simple-variable-assignment-step-5 ((¬ resources-inadequatep (stmt,

proc-list,

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

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

∧ normal (mg-state)) → (p-step (p-state (tag ('pc,

                     '(mg-simple-variable-assignment . 1)),

push (p-frame (list (cons ('dest,

value (car (call-actuals (stmt)),

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

                                 cons ('source,

value (cadr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 3))),

ctrl-stk), push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

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

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

                 'run))

= p-state (tag ('pc,

    '(mg-simple-variable-assignment . 2)),

push (p-frame (list (cons ('dest,

value (car (call-actuals (stmt)),

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

                cons ('source,

value (cadr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 3))),

ctrl-stk), push (rget (untag (value (cadr (call-actuals (stmt)),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))
;; (push-local dest)

Theorem: mg-simple-variable-assignment-step-6 ((¬ resources-inadequatep (stmt,

proc-list,

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ all-cars-unique (mg-alist (mg-state))

∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

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

∧ normal (mg-state)) → (p-step (p-state (tag ('pc,

    '(mg-simple-variable-assignment . 2)),

push (p-frame (list (cons ('dest,

value (car (call-actuals (stmt)),

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

                cons ('source,

value (cadr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 3))),

ctrl-stk), push (rget (untag (value (cadr (call-actuals (stmt)),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

= p-state (tag ('pc,

 '(mg-simple-variable-assignment . 3)),

push (p-frame (list (cons ('dest,

value (car (call-actuals (stmt)),

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

              cons ('source,

value (cadr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 3))),

ctrl-stk), push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (rget (untag (value (cadr (call-actuals (stmt)),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk))),

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))
;; (deposit-temp-stk)

Theorem: mg-simple-variable-assignment-step-7 ((¬ resources-inadequatep (stmt,

proc-list,

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

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

∧ normal (mg-state)) → (p-step (p-state (tag ('pc,

                     '(mg-simple-variable-assignment . 3)),

push (p-frame (list (cons ('dest, value (car (call-actuals (stmt)),

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

                cons ('source,

value (cadr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 3))),

ctrl-stk), push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (rget (untag (value (cadr (call-actuals (stmt)),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk))),

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

= p-state (tag ('pc,

 '(mg-simple-variable-assignment . 4)),

push (p-frame (list (cons ('dest,

value (car (call-actuals (stmt)),

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

              cons ('source,

value (cadr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 3))),

ctrl-stk), rput (rget (untag (value (cadr (call-actuals (stmt)),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

untag (value (car (call-actuals (stmt)), bindings (top (ctrl-stk)))), map-down-values (mg-alist (mg-state),

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

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))
;; (ret)

Theorem: mg-simple-variable-assignment-step-8 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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)) ∧ normal (mg-state)) → (p-step (p-state (tag ('pc,

                     '(mg-simple-variable-assignment . 4)),

push (p-frame (list (cons ('dest,

value (car (call-actuals (stmt)),

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

                                 cons ('source,

value (cadr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 3))),

ctrl-stk), rput (rget (untag (value (cadr (call-actuals (stmt)),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

untag (value (car (call-actuals (stmt)),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

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

mg-cond-to-p-nat (cc (mg-state), 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))

Theorem: mg-simple-variable-assignment-exact-time-lemma ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-assignment)

∧ 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))))))

→ (p (map-down (mg-state, proc-list, ctrl-stk, temp-stk, tag ('pc, cons (subr, length (code (cinfo)))), t-cond-list), clock (stmt, proc-list, mg-state, n))

= 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))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                           ;;
;;             EXACT-TIME LEMMA MG-SIMPLE-CONSTANT-ASSIGNMENT                ;;
;;                                                                           ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: mg-simple-constant-assignment-args-simple-identifierps (ok-mg-statement (stmt, r-cond-list, name-alist, proc-list)

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-constant-assignment)

∧ ok-mg-statep (mg-state, r-cond-list) ∧ signatures-match (mg-alist (mg-state), name-alist)) → simple-identifierp (car (call-actuals (stmt)), mg-alist (mg-state))

Theorem: mg-simple-constant-assignment-steps-1-2 ((¬ resources-inadequatep (stmt,

proc-list,

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-constant-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

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

∧ normal (mg-state)) → (p-step (p-step (map-down (mg-state,

proc-list, ctrl-stk, temp-stk, tag ('pc, cons (subr, length (code (cinfo)))), t-cond-list))) = p-state (tag ('pc, cons (subr, length (code (cinfo)) + 2)),

ctrl-stk,

push (mg-to-p-simple-literal (cadr (call-actuals (stmt))),

push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

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

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))
;; (call mg-simple-constant-assignment)

Theorem: mg-simple-constant-assignment-step-3 ((¬ resources-inadequatep (stmt,

proc-list,

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-constant-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

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

∧ normal (mg-state)) → (p-step (p-state (tag ('pc, cons (subr, length (code (cinfo)) + 2)),

ctrl-stk,

push (mg-to-p-simple-literal (cadr (call-actuals (stmt))),

push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

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

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

                 'run))

= p-state (tag ('pc,

                  '(mg-simple-constant-assignment . 0)),

push (p-frame (list (cons ('dest,

value (car (call-actuals (stmt)),

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

                              cons ('source,

mg-to-p-simple-literal (cadr (call-actuals (stmt))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 3))),

ctrl-stk), map-down-values (mg-alist (mg-state),

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

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))
;; (push-local source)

Theorem: mg-simple-constant-assignment-steps-4-5 ((¬ resources-inadequatep (stmt,

proc-list,

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-constant-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

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

∧ normal (mg-state)) → (p-step (p-step (p-state (tag ('pc,

                           '(mg-simple-constant-assignment
                             . 0)),

push (p-frame (list (cons ('dest,

value (car (call-actuals (stmt)),

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

                                       cons ('source,

mg-to-p-simple-literal (cadr (call-actuals (stmt))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 3))),

ctrl-stk), map-down-values (mg-alist (mg-state),

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

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

mg-cond-to-p-nat (cc (mg-state),

t-cond-list))),

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

         'run)))

= p-state (tag ('pc,

    '(mg-simple-constant-assignment . 2)),

push (p-frame (list (cons ('dest,

value (car (call-actuals (stmt)),

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

                cons ('source,

mg-to-p-simple-literal (cadr (call-actuals (stmt))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 3))),

ctrl-stk), push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (mg-to-p-simple-literal (cadr (call-actuals (stmt))), map-down-values (mg-alist (mg-state),

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

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))
;; (deposit-temp-stk)

Theorem: mg-simple-constant-assignment-step-6 ((¬ resources-inadequatep (stmt,

proc-list,

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-constant-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ mg-vars-list-ok-in-p-state (mg-alist (mg-state),

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

∧ normal (mg-state)) → (p-step (p-state (tag ('pc,

    '(mg-simple-constant-assignment . 2)),

push (p-frame (list (cons ('dest,

value (car (call-actuals (stmt)),

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

                cons ('source,

mg-to-p-simple-literal (cadr (call-actuals (stmt))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 3))),

ctrl-stk), push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (mg-to-p-simple-literal (cadr (call-actuals (stmt))), map-down-values (mg-alist (mg-state),

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

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

= p-state (tag ('pc,

 '(mg-simple-constant-assignment . 3)),

push (p-frame (list (cons ('dest,

value (car (call-actuals (stmt)),

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

              cons ('source,

mg-to-p-simple-literal (cadr (call-actuals (stmt))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 3))),

ctrl-stk), rput (mg-to-p-simple-literal (cadr (call-actuals (stmt))),

untag (value (car (call-actuals (stmt)),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))
;; (ret)

Theorem: mg-simple-constant-assignment-step-7 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-constant-assignment)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-cond-list) ∧ listp (ctrl-stk) ∧ (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) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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)) ∧ normal (mg-state)) → (p-step (p-state (tag ('pc,

                     '(mg-simple-constant-assignment . 3)),

push (p-frame (list (cons ('dest, value (car (call-actuals (stmt)),

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

                cons ('source,

mg-to-p-simple-literal (cadr (call-actuals (stmt))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 3))),

ctrl-stk), rput (mg-to-p-simple-literal (cadr (call-actuals (stmt))),

untag (value (car (call-actuals (stmt)),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

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

mg-cond-to-p-nat (cc (mg-state), 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))

Theorem: mg-simple-constant-assignment-exact-time-lemma ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-constant-assignment)

∧ 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))))))

→ (p (map-down (mg-state, proc-list, ctrl-stk, temp-stk, tag ('pc, cons (subr, length (code (cinfo)))), t-cond-list), clock (stmt, proc-list, mg-state, n))

= 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))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                           ;;
;;                 EXACT-TIME LEMMA MG-SIMPLE-CONSTANT-EQ                    ;;
;;                                                                           ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: mg-simple-variable-eq-args-simple-identifierps (ok-mg-statement (stmt, r-cond-list, name-alist, proc-list)

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-eq)

∧ ok-mg-statep (mg-state, r-cond-list) ∧ signatures-match (mg-alist (mg-state), name-alist)) → (boolean-identifierp (car (call-actuals (stmt)), mg-alist (mg-state))

∧ simple-identifierp (cadr (call-actuals (stmt)), mg-alist (mg-state))

∧ simple-identifierp (caddr (call-actuals (stmt)), mg-alist (mg-state)))

Theorem: mg-simple-variable-eq-args-definedp (ok-mg-statement (stmt, r-cond-list, name-alist, proc-list)

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-eq)

∧ ok-mg-statep (mg-state, r-cond-list) ∧ signatures-match (mg-alist (mg-state), name-alist)) → (definedp (car (call-actuals (stmt)), mg-alist (mg-state))

∧ definedp (cadr (call-actuals (stmt)), mg-alist (mg-state)) ∧ definedp (caddr (call-actuals (stmt)), mg-alist (mg-state)))

Theorem: mg-simple-variable-eq-steps-1-3 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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)) ∧ normal (mg-state)) → (p-step (p-step (p-step (map-down (mg-state,

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

cons (subr, length (code (cinfo)))), t-cond-list))))

= p-state (tag ('pc, cons (subr, length (code (cinfo)) + 3)), ctrl-stk, push (value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

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

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-simple-variable-eq-step-4 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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)) ∧ normal (mg-state)) → (p-step (p-state (tag ('pc, cons (subr, length (code (cinfo)) + 3)),

ctrl-stk,

push (value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

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

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

   'run))
= p-state (tag ('pc, '(mg-simple-variable-eq . 0)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

value (caddr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), map-down-values (mg-alist (mg-state),

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

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Theorem: mg-simple-variable-eq-step-5 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list, list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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)) ∧ normal (mg-state))

→ (p-step (p-state (tag ('pc, '(mg-simple-variable-eq . 0)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

value (caddr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), map-down-values (mg-alist (mg-state),

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

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

                 'run))
    = p-state (tag ('pc, '(mg-simple-variable-eq . 1)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

value (caddr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

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

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-simple-variable-eq-step-6 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist)

∧ 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)) ∧ normal (mg-state))

→ (p-step (p-state (tag ('pc, '(mg-simple-variable-eq . 1)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

value (caddr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

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

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))
= p-state (tag ('pc, '(mg-simple-variable-eq . 2)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

value (caddr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), push (rget (untag (value (cadr (call-actuals (stmt)),

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

push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-simple-variable-eq-step-7 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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)) ∧ normal (mg-state))

→ (p-step (p-state (tag ('pc, '(mg-simple-variable-eq . 2)),

push (p-frame (list (cons ('ans, value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

value (caddr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), push (rget (untag (value (cadr (call-actuals (stmt)),

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

push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))
= p-state (tag ('pc, '(mg-simple-variable-eq . 3)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

value (caddr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), push (value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (rget (untag (value (cadr (call-actuals (stmt)),

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

push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk))),

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-simple-variable-eq-step-8 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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)) ∧ normal (mg-state))

→ (p-step (p-state (tag ('pc, '(mg-simple-variable-eq . 3)),

push (p-frame (list (cons ('ans, value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

value (caddr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), push (value (caddr (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (rget (untag (value (cadr (call-actuals (stmt)),

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

push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk))),

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))
= p-state (tag ('pc, '(mg-simple-variable-eq . 4)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

value (caddr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), push (rget (untag (value (caddr (call-actuals (stmt)),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

push (rget (untag (value (cadr (call-actuals (stmt)),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk))),

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-simple-variable-eq-step-9 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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))

∧ normal (mg-state))

→ (p-step (p-state (tag ('pc, '(mg-simple-variable-eq . 4)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

value (caddr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), push (rget (untag (value (caddr (call-actuals (stmt)),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

push (rget (untag (value (cadr (call-actuals (stmt)),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk))),

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))
= p-state (tag ('pc, '(mg-simple-variable-eq . 5)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y, value (caddr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), push (tag ('bool,

if untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))

= untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))

then 't

else 'f endif), map-down-values (mg-alist (mg-state),

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

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-simple-variable-eq-step-10 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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)) ∧ normal (mg-state))

→ (p-step (p-state (tag ('pc, '(mg-simple-variable-eq . 5)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

value (caddr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), push (tag ('bool, eq-value),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))
= p-state (tag ('pc, '(mg-simple-variable-eq . 6)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

value (caddr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (tag ('bool, eq-value), map-down-values (mg-alist (mg-state),

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

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-simple-variable-eq-step-11 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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)) ∧ normal (mg-state))

→ (p-step (p-state (tag ('pc, '(mg-simple-variable-eq . 6)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

value (caddr (call-actuals (stmt)), bindings (top (ctrl-stk))))), tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (tag ('bool, eq-value),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk))),

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

   'run))
= p-state (tag ('pc, '(mg-simple-variable-eq . 7)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

value (caddr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), rput (tag ('bool, eq-value),

untag (value (car (call-actuals (stmt)),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Theorem: mg-bool-ok-boolean ok-mg-valuep (mg-bool (x), 'boolean-mg)

Theorem: mg-simple-variable-eq-step-12-true-case ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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)) ∧ normal (mg-state) ∧ (untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))

= untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))))

→ (p-step (p-state (tag ('pc, '(mg-simple-variable-eq . 7)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

value (caddr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), rput (tag ('bool, 't),

untag (value (car (call-actuals (stmt)),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

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

mg-cond-to-p-nat (cc (mg-state), 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))

Theorem: mg-simple-variable-eq-step-12-false-case ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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)) ∧ normal (mg-state) ∧ (untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))

≠ untag (mg-to-p-simple-literal (caddr (assoc (caddr (call-actuals (stmt)),

mg-alist (mg-state)))))))

→ (p-step (p-state (tag ('pc, '(mg-simple-variable-eq . 7)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

value (caddr (call-actuals (stmt)),

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

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), rput (tag ('bool, 'f),

untag (value (car (call-actuals (stmt)),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

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

mg-cond-to-p-nat (cc (mg-state), 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))

Theorem: mg-simple-variable-eq-exact-time-lemma ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-variable-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list)

∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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)) ∧ normal (mg-state)) → (p (map-down (mg-state,

proc-list, ctrl-stk, temp-stk, tag ('pc, cons (subr, length (code (cinfo)))), t-cond-list), clock (stmt, proc-list, mg-state, n))

= 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))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                           ;;
;;                 EXACT-TIME LEMMA MG-SIMPLE-CONSTANT-EQ                    ;;
;;                                                                           ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: mg-simple-constant-eq-args-simple-identifierps (ok-mg-statement (stmt, r-cond-list, name-alist, proc-list)

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-constant-eq)

∧ ok-mg-statep (mg-state, r-cond-list) ∧ signatures-match (mg-alist (mg-state), name-alist)) → (boolean-identifierp (car (call-actuals (stmt)), mg-alist (mg-state))

∧ simple-identifierp (cadr (call-actuals (stmt)),

mg-alist (mg-state))

∧ simple-typed-literalp (caddr (call-actuals (stmt)), cadr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))

Theorem: mg-simple-constant-eq-args-definedp (ok-mg-statement (stmt, r-cond-list, name-alist, proc-list)

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-constant-eq)

∧ ok-mg-statep (mg-state, r-cond-list) ∧ signatures-match (mg-alist (mg-state), name-alist)) → (definedp (car (call-actuals (stmt)), mg-alist (mg-state))

∧ definedp (cadr (call-actuals (stmt)), mg-alist (mg-state)))

Theorem: mg-simple-constant-eq-steps-1-3 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-constant-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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)) ∧ normal (mg-state)) → (p-step (p-step (p-step (map-down (mg-state,

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

cons (subr, length (code (cinfo)))), t-cond-list))))

= p-state (tag ('pc, cons (subr, length (code (cinfo)) + 3)), ctrl-stk, push (mg-to-p-simple-literal (caddr (call-actuals (stmt))),

push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

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

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-simple-constant-eq-step-4 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-constant-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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)) ∧ normal (mg-state)) → (p-step (p-state (tag ('pc, cons (subr, length (code (cinfo)) + 3)),

ctrl-stk,

push (mg-to-p-simple-literal (caddr (call-actuals (stmt))),

push (value (cadr (call-actuals (stmt)), bindings (top (ctrl-stk))), push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

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

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

   'run))
= p-state (tag ('pc, '(mg-simple-constant-eq . 0)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

mg-to-p-simple-literal (caddr (call-actuals (stmt))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), map-down-values (mg-alist (mg-state),

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

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Theorem: mg-simple-constant-eq-step-5 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-constant-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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)) ∧ normal (mg-state))

→ (p-step (p-state (tag ('pc, '(mg-simple-constant-eq . 0)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

mg-to-p-simple-literal (caddr (call-actuals (stmt))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), map-down-values (mg-alist (mg-state),

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

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

                 'run))
    = p-state (tag ('pc, '(mg-simple-constant-eq . 1)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x, value (cadr (call-actuals (stmt)),

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

cons ('y,

mg-to-p-simple-literal (caddr (call-actuals (stmt))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

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

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-simple-constant-eq-step-6 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-constant-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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)) ∧ normal (mg-state))

→ (p-step (p-state (tag ('pc, '(mg-simple-constant-eq . 1)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

mg-to-p-simple-literal (caddr (call-actuals (stmt))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

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

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))
= p-state (tag ('pc, '(mg-simple-constant-eq . 2)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

mg-to-p-simple-literal (caddr (call-actuals (stmt))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), push (rget (untag (value (cadr (call-actuals (stmt)),

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

push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

bindings (top (ctrl-stk)), temp-stk))), map-down-values (mg-alist (mg-state),

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

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-simple-constant-eq-step-7 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-constant-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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)) ∧ normal (mg-state))

→ (p-step (p-state (tag ('pc, '(mg-simple-constant-eq . 2)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

mg-to-p-simple-literal (caddr (call-actuals (stmt))))),

tag ('pc, cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), push (rget (untag (value (cadr (call-actuals (stmt)),

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

push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))
= p-state (tag ('pc, '(mg-simple-constant-eq . 3)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

mg-to-p-simple-literal (caddr (call-actuals (stmt))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), push (mg-to-p-simple-literal (caddr (call-actuals (stmt))),

push (rget (untag (value (cadr (call-actuals (stmt)),

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

push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk))), translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-simple-constant-eq-step-8 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-constant-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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)) ∧ normal (mg-state))

→ (p-step (p-state (tag ('pc, '(mg-simple-constant-eq . 3)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

mg-to-p-simple-literal (caddr (call-actuals (stmt))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), push (mg-to-p-simple-literal (caddr (call-actuals (stmt))),

push (rget (untag (value (cadr (call-actuals (stmt)),

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

push (value (cadr (call-actuals (stmt)),

bindings (top (ctrl-stk))), map-down-values (mg-alist (mg-state),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk))),

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))
= p-state (tag ('pc, '(mg-simple-constant-eq . 4)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

mg-to-p-simple-literal (caddr (call-actuals (stmt))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), push (tag ('bool,

if untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))

= untag (mg-to-p-simple-literal (caddr (call-actuals (stmt)))) then 't else 'f endif),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-simple-constant-eq-step-9 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-constant-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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)) ∧ normal (mg-state))

→ (p-step (p-state (tag ('pc, '(mg-simple-constant-eq . 4)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

mg-to-p-simple-literal (caddr (call-actuals (stmt))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), push (tag ('bool, eq-value),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)), translate-proc-list (proc-list), list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

   'run))
= p-state (tag ('pc, '(mg-simple-constant-eq . 5)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

mg-to-p-simple-literal (caddr (call-actuals (stmt))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (tag ('bool, eq-value),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk))),

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

'run))

Theorem: mg-simple-constant-eq-step-10 ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-constant-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list)

∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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)) ∧ normal (mg-state))

→ (p-step (p-state (tag ('pc, '(mg-simple-constant-eq . 5)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

mg-to-p-simple-literal (caddr (call-actuals (stmt))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), push (value (car (call-actuals (stmt)),

bindings (top (ctrl-stk))), push (tag ('bool, eq-value),

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk))),

translate-proc-list (proc-list),

list (list ('c-c,

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

                 'run))
    = p-state (tag ('pc, '(mg-simple-constant-eq . 6)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x, value (cadr (call-actuals (stmt)),

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

cons ('y,

mg-to-p-simple-literal (caddr (call-actuals (stmt))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), rput (tag ('bool, eq-value),

untag (value (car (call-actuals (stmt)),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

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

mg-cond-to-p-nat (cc (mg-state), t-cond-list))), mg-max-ctrl-stk-size, mg-max-temp-stk-size, mg-word-size,

              'run))

Theorem: mg-simple-constant-eq-step-11-true-case ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-constant-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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))

∧ normal (mg-state) ∧ (untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))

= untag (mg-to-p-simple-literal (caddr (call-actuals (stmt))))))

→ (p-step (p-state (tag ('pc, '(mg-simple-constant-eq . 6)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

mg-to-p-simple-literal (caddr (call-actuals (stmt))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), rput (tag ('bool, 't),

untag (value (car (call-actuals (stmt)),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

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

mg-cond-to-p-nat (cc (mg-state), 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))

Theorem: mg-simple-constant-eq-step-11-false-case ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-constant-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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)) ∧ normal (mg-state) ∧ (untag (mg-to-p-simple-literal (caddr (assoc (cadr (call-actuals (stmt)),

mg-alist (mg-state)))))

≠ untag (mg-to-p-simple-literal (caddr (call-actuals (stmt))))))

→ (p-step (p-state (tag ('pc, '(mg-simple-constant-eq . 6)),

push (p-frame (list (cons ('ans,

value (car (call-actuals (stmt)),

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

cons ('x,

value (cadr (call-actuals (stmt)),

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

cons ('y,

mg-to-p-simple-literal (caddr (call-actuals (stmt))))),

tag ('pc,

cons (subr, length (code (cinfo)) + 4))),

ctrl-stk), rput (tag ('bool, 'f),

untag (value (car (call-actuals (stmt)),

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

map-down-values (mg-alist (mg-state), bindings (top (ctrl-stk)), temp-stk)),

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

mg-cond-to-p-nat (cc (mg-state), 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))

Theorem: mg-simple-constant-eq-exact-time-lemma ((n ≄ 0) ∧ (¬ resources-inadequatep (stmt,

proc-list,

list (length (temp-stk),

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

∧ (car (stmt) = 'predefined-proc-call-mg)
∧ (call-name (stmt) = 'mg-simple-constant-eq)

∧ ok-mg-statement (stmt, r-cond-list, name-alist, proc-list) ∧ ok-mg-def-plistp (proc-list) ∧ ok-mg-statep (mg-state, r-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) ∧ listp (ctrl-stk) ∧ all-cars-unique (mg-alist (mg-state)) ∧ signatures-match (mg-alist (mg-state), name-alist) ∧ 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)) ∧ normal (mg-state)) → (p (map-down (mg-state,

proc-list, ctrl-stk, temp-stk, tag ('pc, cons (subr, length (code (cinfo)))), t-cond-list), clock (stmt, proc-list, mg-state, n))

= 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: Make the library "c-predefined1".

Index

add-code, 2 alist-element-type-conversion, 3 all-cars-unique, 3, 4, 10, 11, 13, 15,

18, 24, 25, 28, 30, 31, 33, 34, 36, 38, 40, 42, 44, 46, 48, 51, 53, 54, 56, 57, 59, 61, 63, 65, 66, 69, 71

array-identifier-nat-p-objectp, 4

bindings, 6–72 bool-literal-bool-objectp, 5 bool-literal-bool-objectp2, 5 boolean-identifierp, 3, 29, 52 boolean-identifiers-have-boolea

n-literal-values, 3 boolean-literalp, 3–5 boolean-literalp-mapping, 4 boolean-mg-to-p-simple-literal, 2 boolean-mg-to-p-simple-literal2, 2

call-actuals, 5–16, 19–26, 29–49, 52–

67, 69 call-name, 5–8, 10, 11, 13, 15, 17,

19–23, 25, 27, 29–31, 33, 34, 36, 38, 40, 42, 44, 46, 48, 50, 52–55, 57, 59, 61, 63, 64, 66, 68, 71

cc, 7–29, 31–45, 47–52, 54–62, 64–

70, 72 clock, 18, 28, 51, 71 code, 6–72 cond-subsetp, 17, 27

definedp, 4, 5, 30, 53

fetch-label, 16, 19, 26, 28, 47, 50,

51, 68, 70, 72 find-label, 17, 19, 27, 29, 47, 50, 52,

68, 70, 72 fix-small-integer, 5 fix-small-integer-identity, 5 ilessp, 2 int-identifierp, 3 int-identifiers-have-int-litera

l-values, 3 int-literal-int-objectp, 5 int-literalp, 2–5 int-literalp-mapping, 4 int-literalp-value-small, 5 int-literals-mapping, 3 integerp, 5

label-alist, 2, 16, 19, 26, 28, 47, 50,

51, 68, 70, 72 length, 3, 4, 6–72 length-plistp, 3 length-plistp-2-rewrite, 3 lessp-add1-add1-2, 2 lessp-add1-add1-add1-3, 2 literal-type-conversion, 3

map-down, 6, 18, 20, 28, 30, 51, 53,

71 map-down-values, 6–17, 19–27, 29,

31–45, 47–50, 52, 54–60, 62– 70, 72

mg-alist, 4–72 mg-alistp, 2, 3 mg-bool, 2, 46 mg-bool-ok-boolean, 46 mg-cond-to-p-nat, 5, 7–17, 19–27,

29, 31–45, 47–50, 52, 54– 62, 64–69, 71, 72

mg-max-ctrl-stk-size, 7–17, 19–27, 29, 31–45, 47–50, 52, 54–62, 64– 69, 71, 72

mg-max-temp-stk-size, 3, 4, 7–17, 19–27, 29, 31–45, 47–50, 52, 54–69, 71, 72

mg-meaning-predefined-proc-call, 1 mg-meaning-r, 1, 16–19, 26–29, 47–

52, 67, 68, 70–72 mg-simple-constant-assignment-a

rgs-simple-identifierps, 19 mg-simple-constant-assignment-e

xact-time-lemma, 27 mg-simple-constant-assignment-step

-3, 20 -6, 23 -7, 25 s-1-2, 20 s-4-5, 22

mg-simple-constant-eq-args-defi

nedp, 53 mg-simple-constant-eq-args-simp

le-identifierps, 52 mg-simple-constant-eq-exact-time

-lemma, 71 mg-simple-constant-eq-step-10, 64 mg-simple-constant-eq-step-11-f

alse-case, 68 mg-simple-constant-eq-step-11-t

rue-case, 66 mg-simple-constant-eq-step-4, 54 mg-simple-constant-eq-step-5, 55 mg-simple-constant-eq-step-6, 57 mg-simple-constant-eq-step-7, 59 mg-simple-constant-eq-step-8, 61 mg-simple-constant-eq-step-9, 63 mg-simple-constant-eq-steps-1-3, 53 mg-simple-variable-assignment-a

rgs-definedp, 5 rgs-simple-identifierps, 6

mg-simple-variable-assignment-e

xact-time-lemma, 17 mg-simple-variable-assignment-step

-3, 7 -4, 8 -5, 10 -6, 11 -7, 13 -8, 15 s-1-2, 6

mg-simple-variable-eq-args-defi

nedp, 30 mg-simple-variable-eq-args-simp

le-identifierps, 29 mg-simple-variable-eq-exact-time

-lemma, 50 mg-simple-variable-eq-step-10, 42 mg-simple-variable-eq-step-11, 44 mg-simple-variable-eq-step-12-f

alse-case, 48 mg-simple-variable-eq-step-12-t

rue-case, 46 mg-simple-variable-eq-step-4, 31 mg-simple-variable-eq-step-5, 32 mg-simple-variable-eq-step-6, 34 mg-simple-variable-eq-step-7, 36 mg-simple-variable-eq-step-8, 38 mg-simple-variable-eq-step-9, 40 mg-simple-variable-eq-steps-1-3, 30 mg-to-p-simple-literal, 2–5, 20–26, 42, 46, 48, 49, 54–67, 69

mg-to-p-simple-literalp-preserve s-untag-equality, 2 s-untag-ilessp, 2

mg-vars-list-ok-in-p-state, 3, 4, 6–8, 10, 12, 13, 15, 18, 20–22, 24, 25, 28, 30, 31, 33, 35, 36, 38, 40, 42, 44, 46, 48, 51, 53, 54, 56, 57, 59, 61, 63, 65, 66, 69, 71 mg-word-size, 4, 5, 7–17, 19–27, 29,

31–45, 47–50, 52, 54–69, 71, 72

no-p-aliasing, 15, 18, 25, 28, 30, 31, 33, 35, 36, 38, 40, 43, 44, 46, 48, 51, 53, 54, 56, 57, 59, 61, 63, 65, 66, 69, 71

normal, 1, 6–8, 10, 12, 13, 15, 16, 18, 20–22, 24–26, 28, 30, 31, 33, 35, 36, 38, 41, 43, 44, 46–49, 51, 53, 54, 56, 57, 59, 61, 63, 65, 67, 69– 71

ok-mg-def-plistp, 6–8, 10, 11, 13, 15, 17, 20–23, 25, 27, 30, 31, 33, 34, 36, 38, 40, 42, 44, 46, 48, 51, 53, 54, 56, 57, 59, 61, 63, 64, 66, 69, 71

ok-mg-statement, 5–8, 10, 11, 13, 15, 17, 19–23, 25, 27, 29– 31, 33, 34, 36, 38, 40, 42, 44, 46, 48, 50, 52–54, 56, 57, 59, 61, 63, 64, 66, 69, 71

ok-mg-statep, 5–8, 10, 11, 13, 15, 17, 19–23, 25, 27, 29–31, 33, 34, 36, 38, 40, 42, 44, 46, 48, 51–54, 56, 57, 59, 61, 63, 65, 66, 69, 71

ok-mg-valuep, 46 ok-translation-parameters, 17, 27

p, 18, 28, 51, 71 p-ctrl-stk-size, 6–8, 10, 11, 13, 15–

23, 25–31, 33, 34, 36, 38, 40, 42, 44, 46–55, 57, 59, 61, 63, 64, 66–68, 70–72

p-frame, 8–12, 14, 16, 21–24, 26, 32– 35, 37, 39, 41–43, 45, 46, 49, 55–58, 60–67, 69

p-objectp-type, 4, 5 p-state, 7–17, 19–27, 29, 31–45, 47–

50, 52, 54–69, 71, 72 p-step, 6, 7, 9, 10, 12, 14, 16, 20, 21,

23, 24, 26, 30, 32, 33, 35, 37, 39, 41, 43, 45, 47, 49, 53, 55, 56, 58, 60, 62, 64, 65, 67, 69

p-word-size, 4, 5 plistp, 18, 28 predefined-call-translation-2, 1 predefined-proc-call-meaning-r-

2, 1 predefined-proc-call-sequence, 2 push, 6–14, 16, 20–26, 31–46, 49,

54–67, 69

resource-errorp, 18, 28 resources-inadequatep, 1, 6–8, 10,

11, 13, 15, 17, 20–23, 25, 27, 30, 31, 33, 34, 36, 38, 40, 42, 44, 46, 48, 50, 53– 55, 57, 59, 61, 63, 64, 66, 68, 71

rget, 11–14, 16, 36–41, 58, 60, 62 rput, 15, 16, 25, 26, 45, 47, 49, 66,

67, 69

signal-system-error, 1

signatures-match, 5, 6, 10, 12, 13, 15, 18, 19, 24, 25, 28–31, 33, 34, 36, 38, 40, 42, 44, 46, 48, 51–54, 56, 57, 59, 61, 63, 65, 66, 69, 71

simple-identifier-mapping, 3 simple-identifier-mapping-2, 4 simple-identifier-mapping-3, 4 simple-identifier-nat-p-objectp, 4 simple-identifierp, 2–4, 6, 19, 29, 30,

52 simple-identifiers-have-simple-v

alues, 2 simple-typed-literalp, 2, 3, 53 simple-typed-literalp-mapping-li

stp, 2 small-integerp, 3, 5 small-integerp-mapping, 5 small-naturalp, 3, 4 special-conditions-mg-cond-to-p

-nat, 5

tag, 2, 5–39, 41–47, 49–72

top, 6–72

translate, 1, 6–8, 10, 11, 13, 15–22, 24–31, 33, 34, 36, 38, 40, 42, 44, 46–54, 56, 57, 59, 61, 63, 65–72 translate-def-body, 6–8, 10, 11, 13,

15, 17, 20–22, 24, 25, 27, 30, 31, 33, 34, 36, 38, 40, 42, 44, 46, 48, 51, 53, 54, 56, 57, 59, 61, 63, 65, 66, 69, 71

translate-proc-list, 6–17, 19–27, 29, 31–45, 47–50, 52, 54–62, 64– 70, 72

type, 3, 4

unlabel, 2 unlabel-call, 2 untag, 2–5, 11–14, 16, 25, 26, 36–

42, 45–49, 58, 60, 62, 66, 67, 69

untag-boolean, 4 untag-int-literal-integerp, 5 user-defined-procp, 6–8, 10, 11, 13,

15, 18, 20–22, 24, 25, 27, 30, 31, 33, 34, 36, 38, 40, 42, 44, 46, 48, 51, 53, 54, 56, 57, 59, 61, 63, 65, 66, 69, 71

value, 3, 4, 6–16, 20–26, 31–47, 49, 54–67, 69