Event: Start with the library "c3".

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                           ;;
;;                    %CORRESPONDENCE BETWEEN MG AND P                       ;;
;;                                                                           ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: mg-to-p-simple-literal (lit) = if int-literalp (lit) then list ('int, cadr (lit))

elseif boolean-literalp (lit)

then if cadr (lit) = 'false-mg then list ('bool, 'f)

else list ('bool, 't) endif elseif character-literalp (lit) then list ('int, cadr (lit)) else 0 endif

Event: Disable mg-to-p-simple-literal.

;; An array value is a list of simple mg literals.  Recall that in the most common
;; case, the values will be reversed because they will be in contiguous locations
;; on the stack, which is indexed from the bottom.

Definition: mg-to-p-simple-literal-list (lst) = if lst ≃ nil then nil

else cons (mg-to-p-simple-literal (car (lst)), mg-to-p-simple-literal-list (cdr (lst))) endif

Theorem: mg-to-p-simple-literal-list-plistp plistp (mg-to-p-simple-literal-list (x))

Theorem: length-mg-to-p-simple-literal-list length (mg-to-p-simple-literal-list (x)) = length (x)

Definition: p-to-mg-simple-literal (lit, typespec) = if typespec = 'int-mg then list ('int-mg, cadr (lit))

elseif typespec = 'boolean-mg

    then list ('boolean-mg,

if cadr (lit) = 'f then 'false-mg else 'true-mg endif) else list ('character-mg, cadr (lit)) endif Definition: p-to-mg-simple-literal-list (lst, typespec) = if lst ≃ nil then nil

else cons (p-to-mg-simple-literal (car (lst), typespec), p-to-mg-simple-literal-list (cdr (lst), typespec)) endif

Theorem: p-to-mg-to-p-simple-literal simple-typed-literalp (lit, typespec) → (p-to-mg-simple-literal (mg-to-p-simple-literal (lit), typespec) = lit)

Event: Disable p-to-mg-to-p-simple-literal.

Theorem: p-to-mg-to-p-simple-literal-list simple-typed-literal-plistp (lst, type) → (p-to-mg-simple-literal-list (mg-to-p-simple-literal-list (lst), type)

= lst)

Event: Disable p-to-mg-to-p-simple-literal-list.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                        %Mapping Conditions                         ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Each MG condition in the state is translated to a natural in the
;; Piton state.  This is done by finding it's index in the cond-list,
;; except for 'normal, 'routineerror, 'leave, and 'timed-out which are computed
;; directly.
;; The assumption in the Piton world is that there is always an operative list of
;; conditions (which is really (append formal-conds local-conds) of the procedure
;; definition.  The Piton condition stored is the index of the MG condition into
;; this list.  However, there are potential conditions which are not in this list also.
;; These are 'timed-out, 'leave, 'routineerror, and 'normal and are computed specially.
;; These result is a Piton natural.

Definition: condition-index (cond, cond-list) = if cond = 'leave then 0

elseif cond = 'routineerror then 1

elseif cond = 'normal then 2

else 1 + (1 + index (cond, cond-list)) endif Theorem: condition-index-append (cc ∈ lst1 ) → (condition-index (cc, append (lst1 , lst2 )) = condition-index (cc, lst1 ))

Theorem: condition-index-append2

 ((cc ∉ lst1 ) ∧ (cc ∉ '(normal routineerror leave)))

→ (condition-index (cc, append (lst1 , lst2 ))

= (length (lst1 ) + condition-index (cc, lst2 )))

Definition: mg-cond-to-p-nat (c, cond-list) = list ('nat, condition-index (c, cond-list))

Definition: p-nat-to-mg-cond (p-nat, cond-list)

= if p-nat = '(nat 0) then 'leave
    elseif p-nat = '(nat 1) then 'routineerror

elseif p-nat = '(nat 2) then 'normal

else car (nth (cond-list, ((cadr (p-nat) − 1) − 1) − 1)) endif

Theorem: condition-mapping-inverts ok-cc (c, cond-list) → (p-nat-to-mg-cond (mg-cond-to-p-nat (c, cond-list), cond-list) = c)

Event: Disable condition-mapping-inverts.

Event: Disable mg-cond-to-p-nat.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                     %Depositing Array Values                       ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; The hypothesis will be that each of the locals in bindings contains an address into the
;; temp-stk.  This takes the values of the mg variables and puts them into those locations.
;; Given the values-list for an array, this maps them into successive values in the
;; temp-stk starting at index nat.

Definition: deposit-temp (val, nat, temp-stk) = rput (val, untag (nat), temp-stk)

Definition: fetch-temp (nat, temp-stk) = rget (untag (nat), temp-stk)

Theorem: deposit-temp-preserves-length (untag (y) < length (z)) → (length (deposit-temp (x, y, z)) = length (z))

Event: Disable deposit-temp.

Event: Disable fetch-temp.

Definition: fetch-n-temp-stk-elements (temp-stk, nat, n) = if n ≃ 0 then nil

else cons (fetch-temp (nat, temp-stk),

fetch-n-temp-stk-elements (temp-stk, add1-nat (nat), n − 1)) endif

Definition: deposit-array-value (lit-list, nat, temp-stk) = if lit-list ≃ nil then temp-stk

else deposit-array-value (cdr (lit-list), add1-nat (nat), deposit-temp (mg-to-p-simple-literal (car (lit-list)),

nat,

temp-stk)) endif

Definition: deposit-alist-value (mg-alist-element, bindings, temp-stk) = if simple-mg-type-refp (m-type (mg-alist-element))

then deposit-temp (mg-to-p-simple-literal (m-value (mg-alist-element)), cdr (assoc (car (mg-alist-element), bindings)), temp-stk) else deposit-array-value (m-value (mg-alist-element),

cdr (assoc (car (mg-alist-element), bindings)),

temp-stk) endif

Definition: map-down-values (mg-alist, bindings, temp-stk) = if mg-alist ≃ nil then temp-stk

else map-down-values (cdr (mg-alist), bindings, deposit-alist-value (car (mg-alist),

bindings,

temp-stk)) endif Theorem: map-down-values-distributes map-down-values (append (lst1 , lst2 ), bindings, temp-stk) = map-down-values (lst2 , bindings, map-down-values (lst1 , bindings, temp-stk))

Event: Disable map-down-values-distributes.

Theorem: deposit-array-value-preserves-plistp plistp (temp-stk) → plistp (deposit-array-value (lst, nat, temp-stk))

Event: Disable deposit-array-value-preserves-plistp.

Theorem: map-down-values-preserves-plistp plistp (temp-stk) → plistp (map-down-values (alist, bindings, temp-stk))

Theorem: extra-bindings-dont-affect-deposit-alist-value (car (x) ∉ listcars (bindings1 )) → (deposit-alist-value (x, append (bindings1 , bindings2 ), temp-stk)

= deposit-alist-value (x, bindings2 , temp-stk))

Theorem: deposit-alist-value-not-affected-by-extra-element (car (y) ≠ car (x)) → (deposit-alist-value (y, append (lst1 , cons (x, lst2 )), temp-stk)

= deposit-alist-value (y, append (lst1 , lst2 ), temp-stk))

Theorem: deposit-alist-value-not-affected-by-extra-element2 (car (y) ≠ car (x)) → (deposit-alist-value (y, cons (x, lst2 ), temp-stk)

= deposit-alist-value (y, lst2 , temp-stk))

Theorem: map-down-values-not-affected-by-extra-binding (car (x) ∉ listcars (lst)) → (map-down-values (lst, append (lst1 , cons (x, lst2 )), temp-stk)

= map-down-values (lst, append (lst1 , lst2 ), temp-stk))

Theorem: new-binding-doesnt-disturb-map-down-values (car (x) ∉ listcars (lst1 )) → (map-down-values (lst1 , cons (x, bindings), temp-stk)

= map-down-values (lst1 , bindings, temp-stk))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                       %Ok-Temp-Stk-Index                           ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: ok-temp-stk-index (nat, temp-stk) = (length-plistp (nat, 2)

∧ (type (nat) = 'nat) ∧ (untag (nat) ∈ N) ∧ (untag (nat) < length (temp-stk)))

Event: Disable ok-temp-stk-index.

;; This in the hyps says that each of the piton local names in the piton bindings
;; points to a slot in temp-stk.  It DOESNT say that the value is the right one.
;; The function map-down-values puts the right value at that spot.
;; This needs to also talk about the array case; the length of the temp-stk should be
;; such that not only is the temp-stk-index in the right range, but so are all of the
;; indices of the array elements.

Definition: ok-temp-stk-array-index (nat, temp-stk, lngth) = (length-plistp (nat, 2)

∧ (type (nat) = 'nat) ∧ (untag (nat) ∈ N) ∧ ((untag (nat) + (lngth − 1)) < length (temp-stk)))

Event: Disable ok-temp-stk-array-index.

Theorem: ok-temp-stk-index-sensitive-to-length (ok-temp-stk-index (x, temp-stk1 ) ∧ (length (temp-stk2 ) ≮ length (temp-stk1 ))) → ok-temp-stk-index (x, temp-stk2 )

Event: Disable ok-temp-stk-index-sensitive-to-length.

Theorem: ok-temp-stk-array-index-sensitive-to-length (ok-temp-stk-array-index (x, temp-stk1 , n) ∧ (length (temp-stk2 ) ≮ length (temp-stk1 ))) → ok-temp-stk-array-index (x, temp-stk2 , n)

Event: Disable ok-temp-stk-array-index-sensitive-to-length.

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

;;             %Operations Preserve Temp-Stk Length                   ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: deposit-temp-never-shrinks (length (deposit-temp (x, y, z)) < length (z)) = f

Event: Disable deposit-temp-never-shrinks.

Theorem: lessp-transitive2 ((x ≮ y) ∧ (y ≮ z)) → ((x < z) = f)

Event: Disable lessp-transitive2.

Theorem: deposit-array-value-never-shrinks (length (deposit-array-value (x, y, z)) < length (z)) = f

Event: Disable deposit-array-value-never-shrinks.

Theorem: deposit-alist-value-never-shrinks (length (deposit-alist-value (y, bindings, temp-stk)) < length (temp-stk)) = f

Event: Disable deposit-alist-value-never-shrinks.

Event: Disable deposit-alist-value.

Theorem: deposit-alist-value-never-shrinks2 (u < length (temp-stk)) → ((u < length (deposit-alist-value (y, bindings, temp-stk))) = t)

Event: Disable deposit-alist-value-never-shrinks2.

Theorem: map-down-values-never-shrinks (length (map-down-values (y, bindings, temp-stk)) < length (temp-stk)) = f

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                     %Mg-vars-ok-in-p-state                         ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: mg-var-ok-in-p-state (mg-var, bindings, temp-stk) = (definedp (car (mg-var), bindings)

∧ if simple-mg-type-refp (m-type (mg-var))

then ok-temp-stk-index (cdr (assoc (car (mg-var), bindings)), temp-stk)

else ok-temp-stk-array-index (cdr (assoc (car (mg-var),

bindings)),

temp-stk,

array-length (m-type (mg-var))) endif)

Definition: mg-vars-list-ok-in-p-state (mg-vars, bindings, temp-stk) = if mg-vars ≃ nil then t

else mg-var-ok-in-p-state (car (mg-vars), bindings, temp-stk)

∧ mg-vars-list-ok-in-p-state (cdr (mg-vars), bindings, temp-stk) endif

Theorem: mg-vars-list-ok-in-p-state-cdr (mg-vars-list-ok-in-p-state (x, y, z) ∧ listp (x)) → mg-vars-list-ok-in-p-state (cdr (x), y, z)

Theorem: mg-var-ok-temp-stk-index (mg-vars-list-ok-in-p-state (lst, bindings, temp-stk) ∧ definedp (b, lst)) → ((untag (value (b, bindings)) < length (temp-stk)) = t)

Event: Disable mg-var-ok-temp-stk-index.

Theorem: mg-vars-list-ok-in-p-state-distributes mg-vars-list-ok-in-p-state (append (lst1 , lst2 ), bindings, temp-stk) = (mg-vars-list-ok-in-p-state (lst1 , bindings, temp-stk)

∧ mg-vars-list-ok-in-p-state (lst2 , bindings, temp-stk))

Theorem: mg-vars-list-ok-reorder-cars mg-vars-list-ok-in-p-state (cons (x, cons (y, lst)), bindings, temp-stk) → mg-vars-list-ok-in-p-state (cons (y, cons (x, lst)), bindings, temp-stk)

Theorem: mg-vars-list-ok-strip-off-car (car (x) ∉ listcars (lst1 )) → (mg-vars-list-ok-in-p-state (lst1 , cons (x, lst2 ), temp-stk)

= mg-vars-list-ok-in-p-state (lst1 , lst2 , temp-stk))

Event: Disable mg-vars-list-ok-strip-off-car.

Theorem: mg-vars-list-ok-sensitive-to-temp-stk-length2 ((length (temp-stk2 ) ≮ length (temp-stk1 )) ∧ mg-vars-list-ok-in-p-state (alist, bindings, temp-stk1 )) → mg-vars-list-ok-in-p-state (alist, bindings, temp-stk2 )

Event: Disable mg-vars-list-ok-sensitive-to-temp-stk-length2.

Theorem: append-bindings-doesnt-affect-mg-vars-list-ok mg-vars-list-ok-in-p-state (alist, bindings, temp-stk) → mg-vars-list-ok-in-p-state (alist, append (bindings, lst), temp-stk)

Event: Disable append-bindings-doesnt-affect-mg-vars-list-ok.

Theorem: append-bindings-left-doesnt-affect-mg-vars-list-ok (mg-vars-list-ok-in-p-state (alist, bindings2 , temp-stk) ∧ all-cars-unique (append (bindings1 , bindings2 ))) → mg-vars-list-ok-in-p-state (alist, append (bindings1 , bindings2 ), temp-stk)

Theorem: mg-vars-list-members-ok-vars (mg-vars-list-ok-in-p-state (alist, bindings, temp-stk) ∧ (x ∈ alist)) → mg-var-ok-in-p-state (x, bindings, temp-stk)

Theorem: mg-var-ok-value-lessp-length-temp-stk (mg-vars-list-ok-in-p-state (lst, bindings, temp-stk) ∧ definedp (x, lst)) → ((untag (cdr (assoc (x, bindings))) < length (temp-stk)) = t)

Event: Disable mg-var-ok-value-lessp-length-temp-stk.

Theorem: mg-var-ok-untag-value-numberp (mg-vars-list-ok-in-p-state (lst, bindings, temp-stk) ∧ definedp (x, lst)) → (untag (cdr (assoc (x, bindings))) ∈ N)

Event: Disable mg-var-ok-untag-value-numberp.

Theorem: mg-var-ok-array-index-ok (mg-vars-list-ok-in-p-state (lst, bindings, temp-stk) ∧ mg-alistp (lst) ∧ (y ∈ lst) ∧ (¬ simple-mg-type-refp (m-type (y)))) → (((untag (cdr (assoc (car (y), bindings))) + (length (caddr (y)) − 1))

< length (temp-stk)) = t)

Event: Disable mg-var-ok-array-index-ok.

Theorem: mg-var-ok-array-index-ok2 (mg-vars-list-ok-in-p-state (lst, bindings, temp-stk) ∧ mg-alistp (lst) ∧ (y ∈ lst) ∧ (¬ simple-mg-type-refp (m-type (y)))) → (((untag (cdr (assoc (car (y), bindings))) + (array-length (cadr (y)) − 1))

< length (temp-stk)) = t)

Event: Disable mg-var-ok-array-index-ok2.

Theorem: deposit-alist-value-preserves-mg-vars-list-ok mg-vars-list-ok-in-p-state (cons (x, lst), bindings, temp-stk) → mg-vars-list-ok-in-p-state (lst,

bindings,

deposit-alist-value (x, bindings, temp-stk))

Theorem: deposit-array-value-preserves-length ((untag (nat) + (length (value) − 1)) < length (temp-stk)) → (length (deposit-array-value (value, nat, temp-stk)) = length (temp-stk))

Theorem: member-array-lengths-match (mg-alistp (lst) ∧ (x ∈ lst) ∧ (¬ simple-mg-type-refp (m-type (x)))) → (length (caddr (x)) = array-length (cadr (x)))

Theorem: array-index-lessp (mg-alistp (lst) ∧ (x ∈ lst) ∧ mg-vars-list-ok-in-p-state (lst, bindings, temp-stk) ∧ (¬ simple-mg-type-refp (m-type (x)))) → (((untag (cdr (assoc (car (x), bindings))) + (length (caddr (x)) − 1))

< length (temp-stk)) = t)

Theorem: deposit-alist-value-preserves-length (mg-alistp (lst) ∧ (x ∈ lst) ∧ mg-vars-list-ok-in-p-state (lst, bindings, temp-stk)) → (length (deposit-alist-value (x, bindings, temp-stk))

= length (temp-stk))

Theorem: map-down-values-preserves-length (mg-vars-list-ok-in-p-state (x, y, temp-stk) ∧ mg-alistp (x)) → (length (map-down-values (x, y, temp-stk)) = length (temp-stk))

Theorem: deposit-temp-append1 ((untag (nat) ∈ N) ∧ (untag (nat) < length (temp-stk))) → (deposit-temp (x, nat, append (lst, temp-stk))

= append (lst, deposit-temp (x, nat, temp-stk)))

Event: Disable deposit-temp-append1.

Theorem: deposit-temp-append ((x ∈ vars) ∧ simple-mg-type-refp (cadr (x)) ∧ mg-vars-list-ok-in-p-state (vars, bindings, temp-stk)) → (deposit-temp (value, cdr (assoc (car (x), bindings)), append (lst, temp-stk))

= append (lst,

deposit-temp (value, cdr (assoc (car (x), bindings)), temp-stk)))

Event: Disable deposit-temp-append.

Theorem: map-down-values-doesnt-affect-mg-vars-list-ok (mg-alistp (u) ∧ mg-alistp (x) ∧ mg-vars-list-ok-in-p-state (u, v, temp-stk) ∧ mg-vars-list-ok-in-p-state (x, y, append (lst1 , temp-stk))) → mg-vars-list-ok-in-p-state (x,

y,

append (lst1 , map-down-values (u, v, temp-stk)))

Theorem: signatures-match-preserves-mg-vars-list-ok (signatures-match (x, y) ∧ mg-vars-list-ok-in-p-state (x, z, w)) → mg-vars-list-ok-in-p-state (y, z, w)

Event: Disable signatures-match-preserves-mg-vars-list-ok.

Theorem: ok-temp-stk-simple-member (simple-mg-type-refp (cadr (assoc (x, mg-vars))) ∧ mg-vars-list-ok-in-p-state (mg-vars, bindings, temp-stk)) → ok-temp-stk-index (cdr (assoc (x, bindings)), temp-stk)

Theorem: ok-temp-stk-index-actual (listp (formals) ∧ plistp (mg-vars) ∧ ok-actual-params-list (actuals, mg-vars)

∧ data-param-lists-match (actuals, formals, mg-vars) ∧ ok-mg-formal-data-params-plistp (formals) ∧ mg-vars-list-ok-in-p-state (mg-vars, bindings, temp-stk) ∧ simple-mg-type-refp (cadar (formals))) → ok-temp-stk-index (cdr (assoc (car (actuals), bindings)), temp-stk)

Theorem: ok-temp-stk-array-simple-member (array-mg-type-refp (cadr (assoc (x, mg-vars))) ∧ mg-vars-list-ok-in-p-state (mg-vars, bindings, temp-stk)) → ok-temp-stk-array-index (cdr (assoc (x, bindings)),

temp-stk,

array-length (cadr (assoc (x, mg-vars))))

Theorem: ok-temp-stk-index-array-actual (listp (formals) ∧ plistp (mg-vars) ∧ ok-actual-params-list (actuals, mg-vars) ∧ data-param-lists-match (actuals, formals, mg-vars) ∧ ok-mg-formal-data-params-plistp (formals) ∧ mg-vars-list-ok-in-p-state (mg-vars, bindings, temp-stk) ∧ (¬ simple-mg-type-refp (cadar (formals)))) → ok-temp-stk-array-index (cdr (assoc (car (actuals), bindings)),

temp-stk,

array-length (cadar (formals)))

;; %mg-vars-list-ok-in-p-state
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                      %N-Successive-Pointers                        ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: n-successive-pointers (nat, n) = if n ≃ 0 then nil

else cons (untag (nat), n-successive-pointers (add1-nat (nat), n − 1)) endif

Theorem: n-successive-pointers-plistp plistp (n-successive-pointers (nat, n))

Theorem: lesser-number-not-member-n-successive-pointers (i < untag (nat)) → (i ∉ n-successive-pointers (nat, n))

Theorem: no-duplicates-successive-pointers (untag (nat) ∈ N) → no-duplicates (n-successive-pointers (nat, n))

Theorem: car-member-n-successive-pointers (n ≄ 0) → (untag (nat) ∈ n-successive-pointers (nat, n))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                        %Collect-Pointers                           ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: collect-pointers (bindings, alist) = if alist ≃ nil then nil

elseif simple-mg-type-refp (cadr (car (alist)))

then cons (untag (cdr (assoc (car (car (alist)), bindings))), collect-pointers (bindings, cdr (alist))) else append (n-successive-pointers (cdr (assoc (car (car (alist)),

bindings)), array-length (cadr (car (alist)))),

collect-pointers (bindings, cdr (alist))) endif

Theorem: collect-pointers-plistp plistp (collect-pointers (bindings, alist))

Theorem: collect-pointers-distributes collect-pointers (bindings, append (lst1 , lst2 )) = append (collect-pointers (bindings, lst1 ),

collect-pointers (bindings, lst2 ))

Theorem: signatures-match-preserves-collect-pointers signatures-match (alist2 , alist1 ) → (collect-pointers (bindings, alist1 )

= collect-pointers (bindings, alist2 ))

Event: Disable signatures-match-preserves-collect-pointers.

Theorem: extra-bindings-dont-affect-collect-pointers no-duplicates (listcars (append (bindings1 , lst))) → (collect-pointers (append (bindings1 , bindings2 ), lst)

= collect-pointers (bindings2 , lst))

Event: Disable extra-bindings-dont-affect-collect-pointers.

Theorem: extra-bindings-dont-affect-collect-pointers2 no-duplicates (listcars (append (bindings2 , lst))) → (collect-pointers (append (bindings1 , bindings2 ), lst)

= collect-pointers (bindings1 , lst))

Event: Disable extra-bindings-dont-affect-collect-pointers2.

Theorem: extra-binding-doesnt-affect-collect-pointers (x ∉ listcars (lst)) → (collect-pointers (cons (cons (x, y), bindings), lst)

= collect-pointers (bindings, lst))

Event: Disable extra-binding-doesnt-affect-collect-pointers.

Theorem: defined-array-pointers-subset-collect-pointers (definedp (x, lst) ∧ (¬ simple-mg-type-refp (cadr (assoc (x, lst)))) ∧ mg-alistp (lst)) → subset (n-successive-pointers (cdr (assoc (x, bindings)),

length (caddr (assoc (x, lst)))),

collect-pointers (bindings, lst))

Event: Disable defined-array-pointers-subset-collect-pointers.

;; %collect-pointers
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                          %No-P-Aliasing                            ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; This says that none of the pointers in the variable list point to the same location.
;; This is much stricter than the Gypsy aliasing requirement since it doesn't make any
;; distinction between const and var parameters.  It is consistent with the restriction
;; made in mg-meaning, but both need to be relaxed.

Definition: no-p-aliasing (bindings, alist) = no-duplicates (collect-pointers (bindings, alist))

Theorem: no-p-aliasing-cdr (listp (lst) ∧ no-p-aliasing (bindings, lst)) → no-p-aliasing (bindings, cdr (lst))

Theorem: no-p-aliasing-cdr2 no-p-aliasing (bindings, cons (x, lst)) → no-p-aliasing (bindings, lst)

Theorem: no-p-aliasing-append-commutes no-p-aliasing (bindings, append (x, y)) → no-p-aliasing (bindings, append (y, x))

Event: Disable no-p-aliasing-append-commutes.

Theorem: cons-car-append-no-p-aliasing (listp (x) ∧ no-p-aliasing (bindings, append (x, y))) → no-p-aliasing (bindings, cons (car (x), y))

Event: Disable cons-car-append-no-p-aliasing.

Theorem: no-p-aliasing-cdr-append (listp (y) ∧ no-p-aliasing (bindings, append (x, y))) → no-p-aliasing (bindings, append (x, cdr (y)))

Event: Disable no-p-aliasing-cdr-append.

Theorem: no-p-aliasing-cons-cdr no-p-aliasing (bindings, cons (x, cons (y, lst))) → no-p-aliasing (bindings, cons (x, lst))

Event: Disable no-p-aliasing-cons-cdr.

Theorem: signatures-match-preserves-no-p-aliasing (signatures-match (alist1 , alist2 ) ∧ no-p-aliasing (bindings, alist1 )) → no-p-aliasing (bindings, alist2 )

Event: Disable signatures-match-preserves-no-p-aliasing.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;           %Distinct Variables Have Distinct Pointers               ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: member-pointer-collect-pointers (definedp (x, alist) ∧ mg-name-alistp (alist)) → (untag (cdr (assoc (x, bindings))) ∈ collect-pointers (bindings, alist))

Theorem: no-p-aliasing-distinct-variables-base-case0 (listp (alist) ∧ (x = caar (alist)) ∧ (untag (cdr (assoc (x, bindings))) = untag (cdr (assoc (y, bindings)))) ∧ mg-name-alistp (alist) ∧ definedp (y, alist) ∧ (x ≠ y)) → (¬ no-duplicates (collect-pointers (bindings, alist)))

Event: Disable no-p-aliasing-distinct-variables-base-case0.

Theorem: no-p-aliasing-distinct-variables-base-case (listp (alist) ∧ (x = caar (alist)) ∧ no-p-aliasing (bindings, alist) ∧ mg-name-alistp (alist) ∧ definedp (x, alist) ∧ definedp (y, alist) ∧ (x ≠ y)) → (untag (cdr (assoc (x, bindings))) ≠ untag (cdr (assoc (y, bindings))))

Event: Disable no-p-aliasing-distinct-variables-base-case.

Theorem: no-p-aliasing-distinct-variables (no-p-aliasing (bindings, alist) ∧ mg-name-alistp (alist) ∧ definedp (x, alist) ∧ definedp (y, alist) ∧ (x ≠ y)) → (untag (cdr (assoc (x, bindings))) ≠ untag (cdr (assoc (y, bindings))))

Theorem: distinct-variables-lemma2-base-case (listp (lst) ∧ (x = caar (lst)) ∧ (untag (cdr (assoc (x, bindings)))

∈ n-successive-pointers (cdr (assoc (y, bindings)),

length (caddr (assoc (y, lst)))))

∧ mg-alistp (lst) ∧ definedp (x, lst) ∧ definedp (y, lst) ∧ (x ≠ y) ∧ (¬ simple-mg-type-refp (cadr (assoc (y, lst))))) → (¬ no-p-aliasing (bindings, lst))

Event: Disable distinct-variables-lemma2-base-case.

Theorem: distinct-variables-lemma2 (no-p-aliasing (bindings, lst) ∧ mg-alistp (lst) ∧ definedp (x, lst) ∧ definedp (y, lst) ∧ (x ≠ y) ∧ (¬ simple-mg-type-refp (cadr (assoc (y, lst))))) → (untag (cdr (assoc (x, bindings)))

∉ n-successive-pointers (cdr (assoc (y, bindings)), length (caddr (assoc (y, lst)))))

Theorem: distinct-array-values-one-way-disjoint (mg-vars-list-ok-in-p-state (lst, bindings, temp-stk) ∧ no-p-aliasing (bindings, lst) ∧ mg-alistp (lst) ∧ all-cars-unique (lst) ∧ definedp (x, lst) ∧ definedp (y, lst) ∧ (x ≠ y) ∧ (¬ simple-mg-type-refp (cadr (assoc (x, lst)))) ∧ (¬ simple-mg-type-refp (cadr (assoc (y, lst))))) → one-way-disjoint (n-successive-pointers (cdr (assoc (x, bindings)),

length (caddr (assoc (x, lst)))),

n-successive-pointers (cdr (assoc (y, bindings)), length (caddr (assoc (y, lst)))))

Event: Disable distinct-array-values-one-way-disjoint.

Theorem: distinct-array-values-disjoint (mg-vars-list-ok-in-p-state (lst, bindings, temp-stk) ∧ no-p-aliasing (bindings, lst) ∧ mg-alistp (lst) ∧ all-cars-unique (lst) ∧ definedp (x, lst) ∧ definedp (y, lst) ∧ (x ≠ y) ∧ (¬ simple-mg-type-refp (cadr (assoc (x, lst)))) ∧ (¬ simple-mg-type-refp (cadr (assoc (y, lst))))) → disjoint (n-successive-pointers (cdr (assoc (x, bindings)),

array-length (cadr (assoc (x, lst)))),

n-successive-pointers (cdr (assoc (y, bindings)), array-length (cadr (assoc (y, lst)))))

;; %distinct variables
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                        %Deposits Commutes                          ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: deposit-array-value-append1 ((untag (nat) ∈ N) ∧ ((untag (nat) + (length (value) − 1)) < length (temp-stk))) → (deposit-array-value (value, nat, append (lst, temp-stk))

= append (lst, deposit-array-value (value, nat, temp-stk)))

Event: Disable deposit-array-value-append1.

Theorem: deposit-array-value-append ((x ∈ vars) ∧ mg-alistp (vars) ∧ mg-vars-list-ok-in-p-state (vars, bindings, temp-stk) ∧ (¬ simple-mg-type-refp (cadr (x)))) → (deposit-array-value (caddr (x),

cdr (assoc (car (x), bindings)), append (lst, temp-stk))

= append (lst,

deposit-array-value (caddr (x), cdr (assoc (car (x), bindings)), temp-stk)))

Event: Disable deposit-array-value-append.

Theorem: deposit-alist-value-append ((x ∈ vars) ∧ mg-alistp (vars) ∧ mg-vars-list-ok-in-p-state (vars, bindings, temp-stk)) → (deposit-alist-value (x, bindings, append (lst, temp-stk))

= append (lst, deposit-alist-value (x, bindings, temp-stk)))

Theorem: deposit-temp-commutes ((untag (y) ≠ untag (u)) ∧ (untag (y) ∈ N) ∧ (untag (u) ∈ N) ∧ (untag (u) < length (v)) ∧ (untag (y) < length (v)))

→ (deposit-temp (x, y, deposit-temp (z, u, v))

= deposit-temp (z, u, deposit-temp (x, y, v)))

Event: Disable deposit-temp-commutes.

Theorem: deposit-temp-commutes0 (mg-vars-list-ok-in-p-state (lst, bindings, temp-stk) ∧ no-p-aliasing (bindings, lst) ∧ mg-alistp (lst) ∧ all-cars-unique (lst) ∧ (x ∈ lst) ∧ (y ∈ lst) ∧ (car (x) ≠ car (y))) → (deposit-temp (x-value,

cdr (assoc (car (x), bindings)), deposit-temp (y-value,

cdr (assoc (car (y), bindings)), temp-stk))

= deposit-temp (y-value, cdr (assoc (car (y), bindings)), deposit-temp (x-value,

cdr (assoc (car (x), bindings)), temp-stk)))

Event: Disable deposit-temp-commutes0.

Theorem: deposit-temp-deposit-array-value-commute ((untag (nat1 ) ∉ n-successive-pointers (nat2 , length (value))) ∧ (untag (nat1 ) ∈ N) ∧ (untag (nat2 ) ∈ N) ∧ (untag (nat1 ) < length (temp-stk)) ∧ ((untag (nat2 ) + (length (value) − 1)) < length (temp-stk))) → (deposit-temp (z, nat1 , deposit-array-value (value, nat2 , temp-stk))

= deposit-array-value (value, nat2 , deposit-temp (z, nat1 , temp-stk)))

Event: Disable deposit-temp-deposit-array-value-commute.

Theorem: deposit-temp-deposit-array-value-commute2 (mg-vars-list-ok-in-p-state (lst, bindings, temp-stk) ∧ no-p-aliasing (bindings, lst) ∧ mg-alistp (lst) ∧ all-cars-unique (lst) ∧ (x ∈ lst)

∧ (y ∈ lst) ∧ (car (x) ≠ car (y)) ∧ (¬ simple-mg-type-refp (cadr (y))) ∧ (length (y-value) = array-length (cadr (y)))) → (deposit-temp (z,

cdr (assoc (car (x), bindings)), deposit-array-value (y-value,

cdr (assoc (car (y), bindings)), temp-stk))

= deposit-array-value (y-value, cdr (assoc (car (y), bindings)), deposit-temp (z,

cdr (assoc (car (x), bindings)), temp-stk)))

Event: Disable deposit-temp-deposit-array-value-commute2.

Theorem: one-way-disjoint-non-member-n-successive-pointers (one-way-disjoint (n-successive-pointers (x-nat, n),

n-successive-pointers (y-nat, m))

∧ (n ≄ 0)) → (untag (x-nat) ∉ n-successive-pointers (y-nat, m))

Theorem: deposit-array-value-commutes ((untag (x-nat) ∈ N) ∧ (untag (y-nat) ∈ N) ∧ ((untag (x-nat) + (length (x-value) − 1)) < length (temp-stk)) ∧ ((untag (y-nat) + (length (y-value) − 1)) < length (temp-stk)) ∧ disjoint (n-successive-pointers (x-nat, length (x-value)),

n-successive-pointers (y-nat, length (y-value))))

→ (deposit-array-value (x-value, x-nat, deposit-array-value (y-value, y-nat, temp-stk))

= deposit-array-value (y-value, y-nat, deposit-array-value (x-value,

x-nat, temp-stk)))

Event: Disable deposit-array-value-commutes.

Theorem: deposit-array-value-commutes2 (mg-vars-list-ok-in-p-state (lst, bindings, temp-stk) ∧ no-p-aliasing (bindings, lst)

∧ mg-alistp (lst) ∧ all-cars-unique (lst) ∧ (x ∈ lst) ∧ (y ∈ lst) ∧ (car (x) ≠ car (y)) ∧ (¬ simple-mg-type-refp (cadr (x))) ∧ (¬ simple-mg-type-refp (cadr (y))) ∧ (length (x-value) = array-length (cadr (x))) ∧ (length (y-value) = array-length (cadr (y)))) → (deposit-array-value (x-value,

cdr (assoc (car (x), bindings)), deposit-array-value (y-value,

cdr (assoc (car (y), bindings)), temp-stk))

= deposit-array-value (y-value, cdr (assoc (car (y), bindings)), deposit-array-value (x-value,

cdr (assoc (car (x),

bindings)),

temp-stk)))

Event: Disable deposit-array-value-commutes2.

Theorem: deposit-alist-value-commutes (mg-vars-list-ok-in-p-state (lst, bindings, temp-stk) ∧ no-p-aliasing (bindings, lst) ∧ mg-alistp (lst) ∧ all-cars-unique (lst) ∧ (x ∈ lst) ∧ (y ∈ lst) ∧ (car (x) ≠ car (y))) → (deposit-alist-value (x,

bindings,

deposit-alist-value (y, bindings, temp-stk))

= deposit-alist-value (y, bindings, deposit-alist-value (x, bindings, temp-stk)))

Theorem: deposit-temp-deposit-array-value-commute3 ((untag (nat) < untag (nat1 )) ∧ (untag (nat) ∈ N) ∧ ((untag (nat1 ) + (length (lst) − 1)) < length (temp-stk))) → (deposit-array-value (lst, nat1 , deposit-temp (x, nat, temp-stk))

= deposit-temp (x, nat, deposit-array-value (lst, nat1 , temp-stk)))

Event: Disable deposit-temp-deposit-array-value-commute3.

Theorem: multiple-rputs-cancel rput (x, y, rput (u, y, z)) = rput (x, y, z)

Theorem: multiple-deposit-temps-cancel deposit-temp (x, nat, deposit-temp (y, nat, temp-stk)) = deposit-temp (x, nat, temp-stk)

Event: Disable multiple-deposit-temps-cancel.

Definition: double-cdr-induction2 (x, y, nat) = if x ≃ nil then t

else double-cdr-induction2 (cdr (x), cdr (y), add1-nat (nat)) endif

Theorem: multiple-deposit-array-values-cancel ((length (value1 ) = length (value2 )) ∧ (untag (nat) ∈ N) ∧ ((untag (nat) + (length (value1 ) − 1)) < length (temp-stk))) → (deposit-array-value (value1 ,

nat,

deposit-array-value (value2 , nat, temp-stk))

= deposit-array-value (value1 , nat, temp-stk))

Event: Disable multiple-deposit-array-values-cancel.

Theorem: mg-var-ok-car-definedp ((y ∈ alist) ∧ mg-vars-list-ok-in-p-state (alist, bindings, temp-stk)) → definedp (car (y), bindings)

Theorem: deposit-temp-deposit-temp-commute2 (no-p-aliasing (append (bindings1 , bindings2 ), append (alist1 , alist2 )) ∧ mg-vars-list-ok-in-p-state (alist1 , bindings1 , temp-stk) ∧ mg-vars-list-ok-in-p-state (alist2 , bindings2 , temp-stk) ∧ all-cars-unique (append (alist1 , alist2 )) ∧ all-cars-unique (append (bindings1 , bindings2 )) ∧ mg-alistp (append (alist1 , alist2 )) ∧ (x ∈ alist1 ) ∧ simple-mg-type-refp (cadr (x)) ∧ (y ∈ alist2 ) ∧ simple-mg-type-refp (cadr (y))) → (deposit-temp (x-value, cdr (assoc (car (x), bindings1 )), deposit-temp (y-value,

cdr (assoc (car (y), bindings2 )), temp-stk))

= deposit-temp (y-value, cdr (assoc (car (y), bindings2 )), deposit-temp (x-value,

cdr (assoc (car (x), bindings1 )), temp-stk)))

Event: Disable deposit-temp-deposit-temp-commute2.

Theorem: deposit-temp-deposit-array-value-commute5 (no-p-aliasing (append (bindings1 , bindings2 ), append (alist1 , alist2 )) ∧ mg-vars-list-ok-in-p-state (alist1 , bindings1 , temp-stk) ∧ mg-vars-list-ok-in-p-state (alist2 , bindings2 , temp-stk) ∧ all-cars-unique (append (alist1 , alist2 )) ∧ all-cars-unique (append (bindings1 , bindings2 )) ∧ mg-alistp (append (alist1 , alist2 )) ∧ (x ∈ alist1 ) ∧ simple-mg-type-refp (cadr (x)) ∧ (y ∈ alist2 ) ∧ (¬ simple-mg-type-refp (cadr (y)))) → (deposit-temp (value,

cdr (assoc (car (x), bindings1 )), deposit-array-value (caddr (y),

cdr (assoc (car (y), bindings2 )), temp-stk))

= deposit-array-value (caddr (y), cdr (assoc (car (y), bindings2 )), deposit-temp (value,

cdr (assoc (car (x), bindings1 )), temp-stk)))

Event: Disable deposit-temp-deposit-array-value-commute5.

Theorem: deposit-temp-deposit-alist-value-commute2 (no-p-aliasing (append (bindings1 , bindings2 ), append (alist1 , alist2 )) ∧ mg-vars-list-ok-in-p-state (alist1 , bindings1 , temp-stk) ∧ mg-vars-list-ok-in-p-state (alist2 , bindings2 , temp-stk) ∧ all-cars-unique (append (alist1 , alist2 )) ∧ all-cars-unique (append (bindings1 , bindings2 )) ∧ mg-alistp (append (alist1 , alist2 ))

∧ (x ∈ alist1 ) ∧ simple-mg-type-refp (cadr (x)) ∧ (y ∈ alist2 )) → (deposit-temp (value,

cdr (assoc (car (x), bindings1 )),

deposit-alist-value (y, bindings2 , temp-stk))

= deposit-alist-value (y, bindings2 , deposit-temp (value,

cdr (assoc (car (x), bindings1 )), temp-stk)))

Event: Disable deposit-temp-deposit-alist-value-commute2.

Theorem: deposit-array-value-deposit-array-value-commute2 (no-p-aliasing (append (bindings1 , bindings2 ), append (alist1 , alist2 )) ∧ mg-vars-list-ok-in-p-state (alist1 , bindings1 , temp-stk) ∧ mg-vars-list-ok-in-p-state (alist2 , bindings2 , temp-stk) ∧ all-cars-unique (append (alist1 , alist2 )) ∧ all-cars-unique (append (bindings1 , bindings2 )) ∧ mg-alistp (append (alist1 , alist2 )) ∧ (x ∈ alist1 ) ∧ (¬ simple-mg-type-refp (cadr (x))) ∧ (y ∈ alist2 ) ∧ (¬ simple-mg-type-refp (cadr (y)))) → (deposit-array-value (caddr (x),

cdr (assoc (car (x), bindings1 )), deposit-array-value (caddr (y),

cdr (assoc (car (y), bindings2 )), temp-stk))

= deposit-array-value (caddr (y), cdr (assoc (car (y), bindings2 )), deposit-array-value (caddr (x),

cdr (assoc (car (x),

bindings1 )),

temp-stk)))

Event: Disable deposit-array-value-deposit-array-value-commute2.

Theorem: deposit-array-value-deposit-temp-commute (no-p-aliasing (append (bindings1 , bindings2 ), append (alist1 , alist2 )) ∧ mg-vars-list-ok-in-p-state (alist1 , bindings1 , temp-stk) ∧ mg-vars-list-ok-in-p-state (alist2 , bindings2 , temp-stk)

∧ all-cars-unique (append (alist1 , alist2 )) ∧ all-cars-unique (append (bindings1 , bindings2 )) ∧ mg-alistp (append (alist1 , alist2 )) ∧ (x ∈ alist1 ) ∧ simple-mg-type-refp (cadr (y)) ∧ (y ∈ alist2 ) ∧ (¬ simple-mg-type-refp (cadr (x)))) → (deposit-array-value (caddr (x),

cdr (assoc (car (x), bindings1 )),

deposit-temp (value, cdr (assoc (car (y), bindings2 )), temp-stk))

= deposit-temp (value, cdr (assoc (car (y), bindings2 )), deposit-array-value (caddr (x),

cdr (assoc (car (x), bindings1 )), temp-stk)))

Event: Disable deposit-array-value-deposit-temp-commute.

Theorem: deposit-array-value-deposit-alist-value-commute (no-p-aliasing (append (bindings1 , bindings2 ), append (alist1 , alist2 )) ∧ mg-vars-list-ok-in-p-state (alist1 , bindings1 , temp-stk) ∧ mg-vars-list-ok-in-p-state (alist2 , bindings2 , temp-stk) ∧ all-cars-unique (append (alist1 , alist2 )) ∧ all-cars-unique (append (bindings1 , bindings2 )) ∧ mg-alistp (append (alist1 , alist2 )) ∧ (x ∈ alist1 ) ∧ (¬ simple-mg-type-refp (cadr (x))) ∧ (y ∈ alist2 )) → (deposit-array-value (caddr (x),

cdr (assoc (car (x), bindings1 )),

deposit-alist-value (y, bindings2 , temp-stk))

= deposit-alist-value (y, bindings2 , deposit-array-value (caddr (x),

cdr (assoc (car (x),

bindings1 )),

temp-stk)))

Event: Disable deposit-array-value-deposit-alist-value-commute.

Theorem: deposit-alist-value-commute2 (no-p-aliasing (append (bindings1 , bindings2 ), append (alist1 , alist2 )) ∧ mg-vars-list-ok-in-p-state (alist1 , bindings1 , temp-stk) ∧ mg-vars-list-ok-in-p-state (alist2 , bindings2 , temp-stk) ∧ all-cars-unique (append (alist1 , alist2 )) ∧ all-cars-unique (append (bindings1 , bindings2 )) ∧ mg-alistp (append (alist1 , alist2 )) ∧ (x ∈ alist1 ) ∧ (y ∈ alist2 )) → (deposit-alist-value (x,

bindings1 ,

deposit-alist-value (y, bindings2 , temp-stk))

= deposit-alist-value (y, bindings2 , deposit-alist-value (x, bindings1 , temp-stk)))

Event: Disable deposit-alist-value-commute2.

;; %deposits commute
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                     %Map-Down-Values Commutes                      ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: map-down-values-deposit-alist-value-commute (no-p-aliasing (bindings, cons (x, lst)) ∧ mg-vars-list-ok-in-p-state (cons (x, lst), bindings, temp-stk) ∧ mg-alistp (cons (x, lst)) ∧ all-cars-unique (cons (x, lst))) → (map-down-values (lst,

bindings,

deposit-alist-value (x, bindings, temp-stk))

= deposit-alist-value (x, bindings, map-down-values (lst, bindings, temp-stk)))

Theorem: deposit-temp-map-down-values-commute (all-cars-unique (cons (x, lst)) ∧ mg-alistp (cons (x, lst)) ∧ no-p-aliasing (bindings, cons (x, lst)) ∧ mg-vars-list-ok-in-p-state (cons (x, lst), bindings, temp-stk)) → (deposit-temp (y,

cdr (assoc (car (x), bindings)),

map-down-values (lst, bindings, temp-stk))

= map-down-values (lst, bindings, deposit-temp (y,

cdr (assoc (car (x), bindings)), temp-stk)))

Event: Disable deposit-temp-map-down-values-commute.

Event: Disable no-p-aliasing.

Theorem: deposit-temp-map-down-values-commute-2 (all-cars-unique (cons (x, lst)) ∧ mg-alistp (cons (x, lst)) ∧ no-p-aliasing (bindings, cons (x, lst)) ∧ mg-vars-list-ok-in-p-state (cons (x, lst), bindings, temp-stk)) → (map-down-values (lst,

bindings,

deposit-temp (y, cdr (assoc (car (x), bindings)), temp-stk))

= deposit-temp (y, cdr (assoc (car (x), bindings)), map-down-values (lst, bindings, temp-stk)))

Event: Disable deposit-temp-map-down-values-commute-2.

Theorem: deposit-same-value-doesnt-disturb-map-down-values (mg-vars-list-ok-in-p-state (mg-vars, bindings, temp-stk) ∧ all-cars-unique (mg-vars) ∧ mg-alistp (mg-vars) ∧ no-p-aliasing (bindings, mg-vars) ∧ (x ∈ listcars (mg-vars)) ∧ simple-mg-type-refp (cadr (assoc (x, mg-vars)))) → (rput (mg-to-p-simple-literal (caddr (assoc (x, mg-vars))),

untag (cdr (assoc (x, bindings))),

map-down-values (mg-vars, bindings, temp-stk)) = map-down-values (mg-vars, bindings, temp-stk))

Event: Disable deposit-same-value-doesnt-disturb-map-down-values.

Theorem: deposit-same-array-value-doesnt-disturb-map-down-values (mg-vars-list-ok-in-p-state (mg-vars, bindings, temp-stk) ∧ all-cars-unique (mg-vars)

∧ mg-alistp (mg-vars) ∧ no-p-aliasing (bindings, mg-vars) ∧ (x ∈ listcars (mg-vars)) ∧ (¬ simple-mg-type-refp (cadr (assoc (x, mg-vars))))) → (deposit-array-value (caddr (assoc (x, mg-vars)),

cdr (assoc (x, bindings)),

map-down-values (mg-vars, bindings, temp-stk))

= map-down-values (mg-vars, bindings, temp-stk))

Event: Disable deposit-same-array-value-doesnt-disturb-map-down-values.

Theorem: deposit-same-value-doesnt-disturb-map-down-values2 (mg-vars-list-ok-in-p-state (mg-vars, bindings, temp-stk) ∧ all-cars-unique (mg-vars) ∧ mg-alistp (mg-vars) ∧ no-p-aliasing (bindings, mg-vars) ∧ (x ∈ listcars (mg-vars)) ∧ (¬ simple-mg-type-refp (cadr (assoc (x, mg-vars))))) → (rput (mg-to-p-simple-literal (caaddr (assoc (x, mg-vars))),

untag (cdr (assoc (x, bindings))),

map-down-values (mg-vars, bindings, temp-stk)) = map-down-values (mg-vars, bindings, temp-stk))

Theorem: deposit-same-array-value-doesnt-disturb-map-down-values2 (mg-vars-list-ok-in-p-state (mg-vars, bindings, temp-stk) ∧ all-cars-unique (mg-vars) ∧ mg-alistp (mg-vars) ∧ no-p-aliasing (bindings, mg-vars) ∧ (x ∈ listcars (mg-vars)) ∧ (¬ simple-mg-type-refp (cadr (assoc (x, mg-vars))))) → (deposit-array-value (cdr (caddr (assoc (x, mg-vars))),

add1-nat (cdr (assoc (x, bindings))),

map-down-values (mg-vars, bindings, temp-stk))

= map-down-values (mg-vars, bindings, temp-stk))

Theorem: map-down-values-commutes1 (all-cars-unique (append (alist1 , alist2 )) ∧ mg-alistp (append (alist1 , alist2 )) ∧ no-p-aliasing (bindings, append (alist1 , alist2 )) ∧ mg-vars-list-ok-in-p-state (append (alist1 , alist2 ), bindings, temp-stk)) → (map-down-values (alist1 ,

bindings,

map-down-values (alist2 , bindings, temp-stk))

= map-down-values (alist2 , bindings, map-down-values (alist1 , bindings, temp-stk)))

Theorem: listcars-restriction1 ((listcars (alist) = append (listcars (alist1 ), listcars (alist2 ))) ∧ plistp (alist) ∧ no-duplicates (listcars (alist))) → (append (restrict (alist, listcars (alist1 )),

restrict (alist, listcars (alist2 ))) = alist)

Event: Disable listcars-restriction1.

Theorem: meaning-restriction-append1 ((listcars (alist) = append (listcars (alist1 ), listcars (alist2 ))) ∧ no-duplicates (listcars (alist)) ∧ mg-alistp (alist) ∧ no-p-aliasing (bindings, alist) ∧ mg-vars-list-ok-in-p-state (alist, bindings, temp-stk)) → (map-down-values (alist, bindings, temp-stk)

= map-down-values (restrict (alist, listcars (alist1 )), bindings, map-down-values (restrict (alist,

listcars (alist2 )), bindings, temp-stk)))

Event: Disable meaning-restriction-append1.

Theorem: deposit-alist-value-map-down-values-commute2 (no-p-aliasing (append (bindings1 , bindings2 ), append (alist1 , alist2 )) ∧ mg-vars-list-ok-in-p-state (alist1 , bindings1 , temp-stk) ∧ mg-vars-list-ok-in-p-state (alist2 , bindings2 , temp-stk) ∧ all-cars-unique (append (alist1 , alist2 )) ∧ all-cars-unique (append (bindings1 , bindings2 )) ∧ plistp (alist1 ) ∧ mg-alistp (append (alist1 , alist2 )) ∧ (x ∈ alist1 )) → (deposit-alist-value (x,

bindings1 ,

map-down-values (alist2 , bindings2 , temp-stk))

= map-down-values (alist2 , bindings2 , deposit-alist-value (x, bindings1 , temp-stk)))

Event: Disable deposit-alist-value-map-down-values-commute2.

Theorem: map-down-values-commute (all-cars-unique (append (alist1 , alist2 )) ∧ all-cars-unique (append (bindings1 , bindings2 )) ∧ plistp (alist1 ) ∧ mg-alistp (append (alist1 , alist2 )) ∧ no-p-aliasing (append (bindings1 , bindings2 ), append (alist1 , alist2 )) ∧ mg-vars-list-ok-in-p-state (alist1 , bindings1 , temp-stk) ∧ mg-vars-list-ok-in-p-state (alist2 , bindings2 , temp-stk)) → (map-down-values (alist1 ,

bindings1 ,

map-down-values (alist2 , bindings2 , temp-stk))

= map-down-values (alist2 , bindings2 , map-down-values (alist1 , bindings1 , temp-stk)))

Event: Disable map-down-values-commute.

Theorem: deposit-temp-doesnt-affect-map-down-values (mg-alistp (cons (x, mg-vars)) ∧ all-cars-unique (cons (x, mg-vars)) ∧ no-p-aliasing (bindings, cons (x, mg-vars)) ∧ mg-vars-list-ok-in-p-state (cons (x, mg-vars), bindings, temp-stk)) → (map-down-values (mg-vars,

bindings,

deposit-temp (value, cdr (assoc (car (x), bindings)), temp-stk))

= deposit-temp (value, cdr (assoc (car (x), bindings)), map-down-values (mg-vars, bindings, temp-stk)))

Event: Disable deposit-temp-doesnt-affect-map-down-values.

Definition: rget-array-mapping-induction-hint (value, index, nat, temp-stk) = if value ≃ nil then t

elseif index ≃ 0 then t

else rget-array-mapping-induction-hint (cdr (value), index − 1, add1-nat (nat), deposit-temp (mg-to-p-simple-literal (car (value)), nat, temp-stk)) endif

Theorem: rget-array-index-mapping0 (((untag (nat) + (length (value) − 1)) < length (temp-stk)) ∧ (untag (nat) ∈ N) ∧ (index < length (value))) → (rget (untag (nat) + index, deposit-array-value (value, nat, temp-stk))

= mg-to-p-simple-literal (get (index, value)))

Theorem: rget-array-index-mapping (mg-alistp (mg-vars) ∧ all-cars-unique (mg-vars) ∧ no-p-aliasing (bindings, mg-vars) ∧ array-identifierp (a, mg-vars) ∧ mg-vars-list-ok-in-p-state (mg-vars, bindings, temp-stk) ∧ (index < array-length (cadr (assoc (a, mg-vars))))) → (rget (untag (value (a, bindings)) + index,

map-down-values (mg-vars, bindings, temp-stk)) = mg-to-p-simple-literal (get (index, caddr (assoc (a, mg-vars)))))

Event: Disable rget-array-index-mapping.

Theorem: append-doesnt-affect-rput (i < length (lst2 )) → (rput (value, i, append (lst1 , lst2 )) = append (lst1 , rput (value, i, lst2 )))

Event: Disable append-doesnt-affect-rput.

Theorem: append-doesnt-affect-deposit-temp (definedp (b, mg-vars) ∧ mg-alistp (mg-vars) ∧ mg-vars-list-ok-in-p-state (mg-vars, bindings, temp-stk)) → (deposit-temp (value,

cdr (assoc (b, bindings)),

append (lst, map-down-values (mg-vars, bindings, temp-stk)))

= append (lst,

deposit-temp (value, cdr (assoc (b, bindings)), map-down-values (mg-vars, bindings, temp-stk))))

Event: Disable append-doesnt-affect-deposit-temp.

;; %map-down-values commutes

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                %Ascending-Local-Address-Sequence                   ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; This function is used to describe the addresses pushed for the locals upon
;; entry to a procedure call.

Definition: ascending-local-address-sequence (locals, n) = if locals ≃ nil then nil

elseif simple-mg-type-refp (formal-type (car (locals)))

then cons (tag ('nat, n),

ascending-local-address-sequence (cdr (locals), 1 + n))

else cons (tag ('nat, n),

ascending-local-address-sequence (cdr (locals), array-length (formal-type (car (locals))) + n)) endif

Theorem: length-ascending-local-address-sequence length (ascending-local-address-sequence (locals, k)) = length (locals)

Theorem: ascending-local-address-sequence-plistp plistp (ascending-local-address-sequence (x, y))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                   %All-Pointer-Smaller/Bigger                      ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; These functions are used strictly in the proof that there is no-p-aliasing
;; in the call environment.
;; The previous version assumed that the pointers were still in the bindings.
;; This version assumes that we've applied the function collect-pointers and
;; therefore have a list of numberp's.

Definition: all-pointers-smaller (lst, n) = if lst ≃ nil then t

else (car (lst) < n) ∧ all-pointers-smaller (cdr (lst), n) endif Theorem: all-pointers-smaller-distributes all-pointers-smaller (append (lst1 , lst2 ), n) = (all-pointers-smaller (lst1 , n) ∧ all-pointers-smaller (lst2 , n))

Event: Disable all-pointers-smaller-distributes.

Definition: all-pointers-bigger (lst, n) = if lst ≃ nil then t

else (n ≤ car (lst)) ∧ all-pointers-bigger (cdr (lst), n) endif

Theorem: all-pointers-bigger-distributes all-pointers-bigger (append (lst1 , lst2 ), n) = (all-pointers-bigger (lst1 , n) ∧ all-pointers-bigger (lst2 , n))

Theorem: pointers-bigger-monotonic ((m ≮ n) ∧ all-pointers-bigger (x, m)) → all-pointers-bigger (x, n)

Event: Disable pointers-bigger-monotonic.

Theorem: all-pointers-smaller-member ((i ≮ n) ∧ all-pointers-smaller (lst, n)) → (i ∉ lst)

Event: Disable all-pointers-smaller-member.

Theorem: all-pointers-bigger-member ((i < n) ∧ all-pointers-bigger (lst, n)) → (i ∉ lst)

Event: Disable all-pointers-bigger-member.

Definition: successive-pointers-bigger-induction-hint (nat, n, m) = if m ≃ 0 then t

else successive-pointers-bigger-induction-hint (add1-nat (nat), 1 + n, m − 1) endif

Theorem: successive-pointers-bigger0 (nat = tag ('nat, n)) → all-pointers-bigger (n-successive-pointers (nat, m), n)

Event: Disable successive-pointers-bigger0.

Theorem: successive-pointers-bigger all-pointers-bigger (n-successive-pointers (tag ('nat, n), m), n)

Event: Disable successive-pointers-bigger.

Theorem: no-duplicates-all-pointers-disjoint (no-duplicates (lst1 ) ∧ no-duplicates (lst2 ) ∧ all-pointers-smaller (lst2 , n) ∧ all-pointers-bigger (lst1 , n)) → no-duplicates (append (lst1 , lst2 ))

Event: Disable no-duplicates-all-pointers-disjoint.

Theorem: no-duplicates-all-pointers-disjoint2 (no-duplicates (lst1 ) ∧ no-duplicates (lst2 ) ∧ all-pointers-smaller (lst1 , n) ∧ all-pointers-bigger (lst2 , n)) → no-duplicates (append (lst1 , lst2 ))

Theorem: successive-pointers-smaller2 ((untag (nat) ∈ N) ∧ (k ≮ (untag (nat) + m))) → all-pointers-smaller (n-successive-pointers (nat, m), k)

Theorem: no-p-aliasing-append1 (no-p-aliasing (bindings, lst1 ) ∧ no-p-aliasing (bindings, lst2 ) ∧ all-pointers-bigger (collect-pointers (bindings, lst1 ), n) ∧ all-pointers-smaller (collect-pointers (bindings, lst2 ), n)) → no-p-aliasing (bindings, append (lst1 , lst2 ))

Event: Disable no-p-aliasing-append1.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                        %Mapping Data Up                            ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; The list of mg-vars is of the form (... (cons name (cons value type)) ...)
;; and the p-vars of the form (... (cons name value) ...).  This takes the
;; p-vars and maps them up to the corresponding mg-vars list.  Using the types

;; to give the value-value mapping.
;; In mapping up from the Piton to the MG world, I need to know the signatures of
;; the variables at the lower level but not their values.  This returns a value
;; which is just like the variable alist but has all of the values set to (false).
;; The map up from Piton to MG world now has a layer of indirection.  That is,
;; the variable in the Piton world contains an address to the value in the
;; my-stack array.
;; Notice that the other stuff which may appear on an alist entry is
;; not preserved.
;; Notice that the value of the Piton variable is actually on the
;; my-stack data structure.  Consequently, we require a "fetch" into
;; that data structure to get it.  Thus, we must have the Piton state
;; p-data-segment as a parameter to the map-up-vars functions.
;; Every local in the bindings of the top frame contains a natural which is
;; an index into the temp-stk where the actual value is stored.
;; This should be removed when I have the opportunity to redo the events and
;; adjust for this difference.

Definition: map-up-vars-list-array (p-var, temp-stk, var-signature) = list (car (var-signature),

cadr (var-signature),

p-to-mg-simple-literal-list (fetch-n-temp-stk-elements (temp-stk, cdr (p-var), array-length (cadr (var-signature))),

array-elemtype (cadr (var-signature))))

Event: Disable map-up-vars-list-array.

Definition: map-up-vars-list-simple-element (p-var, temp-stk, var-signature) = list (car (var-signature),

cadr (var-signature),

p-to-mg-simple-literal (fetch-temp (cdr (p-var), temp-stk), cadr (var-signature)))

Event: Disable map-up-vars-list-simple-element.

Definition: map-up-vars-list-element (p-var, temp-stk, var-signature) = if simple-mg-type-refp (cadr (var-signature))

then map-up-vars-list-simple-element (p-var, temp-stk, var-signature) else map-up-vars-list-array (p-var, temp-stk, var-signature) endif

;; p-vars here is the bindings component from the topmost frame of the
;; P-CTRL-STK.

Definition: map-up-vars-list (p-vars, temp-stk, signature) = if signature ≃ nil then nil

else cons (map-up-vars-list-element (assoc (caar (signature), p-vars), temp-stk, car (signature)),

map-up-vars-list (p-vars, temp-stk, cdr (signature))) endif

;; The mg-state is computed from the p-state by tranforming the value of the
;; global int variable 'c-c to an mg condition.  The vars are mapped up and
;; given the corresponding values in the mg-state.

Definition: piton-cc (p) = fetch-adp ('(c-c . 0), p-data-segment (p))

Definition: map-up (p-state, mg-signature, cond-list) = mg-state (p-nat-to-mg-cond (piton-cc (p-state), cond-list),

map-up-vars-list (bindings (top (p-ctrl-stk (p-state))), p-temp-stk (p-state), mg-signature),

            'run)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                     %Map Up Inverts Map Down                       ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: definedp-car-cons2 listp (y) → definedp (caar (y), cons (x, y))

Theorem: put-doesnt-affect-get ((n ∈ N) ∧ (m ∈ N) ∧ (n < length (z)) ∧ (m < length (z)) ∧ (n ≠ m)) → (get (n, put (x, m, z)) = get (n, z))

Event: Disable put-doesnt-affect-get.

Theorem: rput-doesnt-affect-rget ((n ∈ N) ∧ (m ∈ N) ∧ (n < length (z)) ∧ (m < length (z)) ∧ (n ≠ m)) → (rget (n, rput (x, m, z)) = rget (n, z))

Event: Disable rput-doesnt-affect-rget.

Theorem: deposit-temp-doesnt-affect-fetch-temp ((untag (nat1 ) ≠ untag (nat2 )) ∧ (untag (nat1 ) ∈ N) ∧ (untag (nat2 ) ∈ N) ∧ (untag (nat1 ) < length (temp-stk)) ∧ (untag (nat2 ) < length (temp-stk))) → (fetch-temp (nat1 , deposit-temp (value, nat2 , temp-stk))

= fetch-temp (nat1 , temp-stk))

Event: Disable deposit-temp-doesnt-affect-fetch-temp.

Theorem: deposit-array-value-doesnt-affect-fetch-temp ((untag (nat1 ) ∈ N) ∧ (untag (nat2 ) ∈ N) ∧ (untag (nat1 ) ∉ n-successive-pointers (nat2 , length (value))) ∧ (untag (nat1 ) < length (temp-stk)) ∧ ((untag (nat2 ) + (length (value) − 1)) < length (temp-stk))) → (fetch-temp (nat1 , deposit-array-value (value, nat2 , temp-stk))

= fetch-temp (nat1 , temp-stk))

Event: Disable deposit-array-value-doesnt-affect-fetch-temp.

Theorem: deposit-temp-doesnt-affect-fetch-n-temp-stk-elements ((untag (nat1 ) ∈ N)

∧ (untag (nat2 ) ∈ N) ∧ (untag (nat2 ) ∉ n-successive-pointers (nat1 , n)) ∧ (untag (nat2 ) < length (temp-stk)) ∧ ((untag (nat1 ) + (n − 1)) < length (temp-stk))) → (fetch-n-temp-stk-elements (deposit-temp (x, nat2 , temp-stk), nat1 , n)

= fetch-n-temp-stk-elements (temp-stk, nat1 , n))

Event: Disable deposit-temp-doesnt-affect-fetch-n-temp-stk-elements.

Theorem: deposit-array-value-doesnt-affect-fetch-n-temp-stk-elements ((untag (nat1 ) ∈ N) ∧ (untag (nat2 ) ∈ N) ∧ ((untag (nat2 ) + (n − 1)) < length (temp-stk)) ∧ ((untag (nat1 ) + (length (value) − 1)) < length (temp-stk)) ∧ disjoint (n-successive-pointers (nat1 , length (value)),

n-successive-pointers (nat2 , n)))

→ (fetch-n-temp-stk-elements (deposit-array-value (value, nat1 , temp-stk), nat2 , n)

= fetch-n-temp-stk-elements (temp-stk, nat2 , n))

Event: Disable deposit-array-value-doesnt-affect-fetch-n-temp-stk-elements.

Theorem: deposit-at-lesser-index-doesnt-affect-fetch ((untag (nat1 ) ∈ N) ∧ (untag (nat1 ) < untag (nat2 )) ∧ ((untag (nat2 ) + (n − 1)) < length (temp-stk))) → (fetch-n-temp-stk-elements (deposit-temp (x, nat1 , temp-stk), nat2 , n)

= fetch-n-temp-stk-elements (temp-stk, nat2 , n))

Event: Disable deposit-at-lesser-index-doesnt-affect-fetch.

Theorem: append-doesnt-affect-rget (n < length (temp-stk)) → (rget (n, append (lst, temp-stk)) = rget (n, temp-stk))

Theorem: append-doesnt-affect-rget-corollary (n < length (temp-stk)) → (rget (n, push (x, temp-stk)) = rget (n, temp-stk))

Definition: fetch-temp-stk-elements-induction-hint (value, temp-stk, nat, n) = if value ≃ nil then t else fetch-temp-stk-elements-induction-hint (cdr (value),

temp-stk,

add1-nat (nat), n − 1) endif

Theorem: fetch-n-temp-stk-elements-inverts-deposit-array-value ((n = length (value)) ∧ (untag (nat) ∈ N) ∧ ((untag (nat) + (length (value) − 1)) < length (temp-stk))) → (fetch-n-temp-stk-elements (deposit-array-value (value, nat, temp-stk),

nat, n)

= mg-to-p-simple-literal-list (value))

Event: Disable fetch-n-temp-stk-elements-inverts-deposit-array-value.

Theorem: simple-vars-have-simple-values (mg-alist-elementp (x) ∧ simple-mg-type-refp (cadr (x))) → simple-typed-literalp (caddr (x), cadr (x))

Event: Disable simple-vars-have-simple-values.

Theorem: array-vars-have-simple-plistp-values (mg-alist-elementp (x) ∧ (¬ simple-mg-type-refp (cadr (x)))) → simple-typed-literal-plistp (caddr (x), array-elemtype (cadr (x)))

Event: Disable array-vars-have-simple-plistp-values.

Theorem: map-up-map-down-preserves-mg-alist-elements-equal ((mg-vars ≄ nil) ∧ all-cars-unique (mg-vars) ∧ mg-alistp (mg-vars) ∧ no-p-aliasing (bindings, mg-vars) ∧ mg-vars-list-ok-in-p-state (mg-vars, bindings, temp-stk)) → (map-up-vars-list-element (assoc (caar (mg-vars), bindings),

map-down-values (mg-vars, bindings, temp-stk), list (caar (mg-vars), cadar (mg-vars)))

= car (mg-vars))

Event: Disable map-up-map-down-preserves-mg-alist-elements-equal.

;; The proof of this should really be "packaged" up into the four
;; cases depending on which of x and (car mg-vars) are simple or not.

Theorem: deposit-alist-value-doesnt-affect-map-up-vars-list0 (all-cars-unique (cons (x, mg-vars)) ∧ mg-alistp (cons (x, mg-vars)) ∧ mg-vars-list-ok-in-p-state (cons (x, mg-vars), bindings, temp-stk) ∧ no-p-aliasing (bindings, cons (x, mg-vars))) → (map-up-vars-list (bindings,

deposit-alist-value (x, bindings, temp-stk), signature (mg-vars))

= map-up-vars-list (bindings, temp-stk, signature (mg-vars)))

Event: Disable deposit-alist-value-doesnt-affect-map-up-vars-list0.

Theorem: deposit-alist-value-doesnt-affect-map-up-vars-list (all-cars-unique (cons (x, mg-vars)) ∧ mg-alistp (cons (x, mg-vars)) ∧ mg-vars-list-ok-in-p-state (cons (x, mg-vars), bindings, temp-stk) ∧ no-p-aliasing (bindings, cons (x, mg-vars))) → (map-up-vars-list (bindings,

map-down-values (mg-vars, bindings, deposit-alist-value (x,

bindings, temp-stk)),

signature (mg-vars))

= map-up-vars-list (bindings, map-down-values (mg-vars, bindings, temp-stk), signature (mg-vars)))

Event: Disable deposit-alist-value-doesnt-affect-map-up-vars-list.

Theorem: rget-rewrite1 (mg-alistp (mg-vars) ∧ all-cars-unique (mg-vars) ∧ no-p-aliasing (bindings, mg-vars) ∧ simple-identifierp (y, mg-vars) ∧ mg-vars-list-ok-in-p-state (mg-vars, bindings, temp-stk)) → (rget (untag (value (y, bindings)),

map-down-values (mg-vars, bindings, temp-stk)) = mg-to-p-simple-literal (caddr (assoc (y, mg-vars))))

Theorem: set-alist-value-deposit-temp-relation (mg-alistp (mg-vars) ∧ all-cars-unique (mg-vars) ∧ no-p-aliasing (bindings, mg-vars)

∧ simple-identifierp (y, mg-vars) ∧ mg-vars-list-ok-in-p-state (mg-vars, bindings, temp-stk) ∧ ok-mg-valuep (value, cadr (assoc (y, mg-vars)))) → (map-down-values (set-alist-value (y, value, mg-vars), bindings, temp-stk)

= rput (mg-to-p-simple-literal (value), untag (value (y, bindings)), map-down-values (mg-vars, bindings, temp-stk)))

Event: Disable set-alist-value-deposit-temp-relation.

Theorem: set-alist-value-deposit-array-value-relation (mg-alistp (mg-vars) ∧ all-cars-unique (mg-vars) ∧ no-p-aliasing (bindings, mg-vars) ∧ array-identifierp (a, mg-vars) ∧ ok-mg-array-value (lst, cadr (assoc (a, mg-vars))) ∧ mg-vars-list-ok-in-p-state (mg-vars, bindings, temp-stk)) → (map-down-values (set-alist-value (a, lst, mg-vars), bindings, temp-stk)

= deposit-array-value (lst, value (a, bindings), map-down-values (mg-vars, bindings, temp-stk)))

Event: Disable set-alist-value-deposit-array-value-relation.

Theorem: append-doesnt-affect-deposit-alist-value (car (x) ∈ listcars (bindings1 )) → (deposit-alist-value (x, append (bindings1 , bindings2 ), temp-stk)

= deposit-alist-value (x, bindings1 , temp-stk))

Theorem: deposit-temp-length-cons plistp (temp-stk) → (deposit-temp (x, tag ('nat, length (temp-stk)), cons (y, temp-stk))

= cons (x, temp-stk))

Event: Disable deposit-temp-length-cons.

Definition: deposit-array-value-same-value-induction-hint (array-value, temp-stk) = if array-value ≃ nil then t

else deposit-array-value-same-value-induction-hint (cdr (array-value),

deposit-temp (mg-to-p-simple-literal (car (array-value)),

tag ('nat, length (temp-stk)), cons (mg-to-p-simple-literal (car (array-value)),

temp-stk))) endif

Theorem: deposit-temp-preserves-plistp plistp (z) → plistp (deposit-temp (x, y, z))

Theorem: deposit-array-value-same-value-doesnt-disturb-temp-stk plistp (temp-stk) → (deposit-array-value (array-value,

tag ('nat, length (temp-stk)), append (lst,

append (reverse (mg-to-p-simple-literal-list (array-value)),

temp-stk)))

= append (lst,

append (reverse (mg-to-p-simple-literal-list (array-value)), temp-stk)))

Event: Disable deposit-array-value-same-value-doesnt-disturb-temp-stk.

Event: Make the library "c4".

Index

add1-nat, 4, 12, 22, 28, 30, 33, 39 all-cars-unique, 9, 17, 19, 21–31, 39–

41 all-pointers-bigger, 33, 34 all-pointers-bigger-distributes, 33 all-pointers-bigger-member, 33 all-pointers-smaller, 32–34 all-pointers-smaller-distribute

s, 33 all-pointers-smaller-member, 33 append-bindings-doesnt-affect-m

g-vars-list-ok, 9 append-bindings-left-doesnt-affe

ct-mg-vars-list-ok, 9 append-doesnt-affect-deposit-ali

st-value, 41 append-doesnt-affect-deposit-te

mp, 31 append-doesnt-affect-rget, 38 append-doesnt-affect-rget-corol

lary, 38 append-doesnt-affect-rput, 31 array-elemtype, 35, 39 array-identifierp, 31, 41 array-index-lessp, 10 array-length, 8, 10, 12, 13, 17, 20,

21, 31, 32, 35 array-mg-type-refp, 12 array-vars-have-simple-plistp-v

alues, 39 ascending-local-address-sequence, 32

-plistp, 32

bindings, 36 boolean-literalp, 1

car-member-n-successive-pointer

s, 13 character-literalp, 1 collect-pointers, 13–16, 34 collect-pointers-distributes, 13 collect-pointers-plistp, 13 condition-index, 2, 3 condition-index-append, 3 condition-index-append2, 3 condition-mapping-inverts, 3 cons-car-append-no-p-aliasing, 15

data-param-lists-match, 12 defined-array-pointers-subset-c ollect-pointers, 14 definedp, 8, 9, 14–17, 22, 31, 36 definedp-car-cons2, 36 deposit-alist-value, 4, 5, 7, 10, 18, 21, 24–26, 29, 40, 41

deposit-alist-value-append, 18 deposit-alist-value-commute2, 26 deposit-alist-value-commutes, 21 deposit-alist-value-doesnt-affe ct-map-up-vars-list, 40 ct-map-up-vars-list0, 40 deposit-alist-value-map-down-va lues-commute2, 29 deposit-alist-value-never-shrin

ks, 7 ks2, 7

deposit-alist-value-not-affecte d-by-extra-element, 5 d-by-extra-element2, 5 deposit-alist-value-preserves-le

ngth, 10 deposit-alist-value-preserves-m g-vars-list-ok, 10

deposit-array-value, 4, 5, 7, 10, 18–

25, 28, 31, 37–39, 41, 42 deposit-array-value-append, 18 deposit-array-value-append1, 18 deposit-array-value-commutes, 20 deposit-array-value-commutes2, 20 deposit-array-value-deposit-ali st-value-commute, 25 deposit-array-value-deposit-arr

ay-value-commute2, 24 deposit-array-value-deposit-temp

-commute, 24 deposit-array-value-doesnt-affe

ct-fetch-n-temp-stk-elements, 38 ct-fetch-temp, 37

deposit-array-value-never-shrin

ks, 7 deposit-array-value-preserves-le

ngth, 10 deposit-array-value-preserves-p

listp, 5 deposit-array-value-same-value-

doesnt-disturb-temp-stk, 42 deposit-array-value-same-value-i

nduction-hint, 41, 42 deposit-at-lesser-index-doesnt-

affect-fetch, 38 deposit-same-array-value-doesnt

-disturb-map-down-values, 27 -disturb-map-down-values2, 28

deposit-same-value-doesnt-distu rb-map-down-values, 27 rb-map-down-values2, 28

deposit-temp, 3, 4, 7, 11, 19–25, 27,

30, 31, 37, 38, 41, 42 deposit-temp-append, 11 deposit-temp-append1, 11 deposit-temp-commutes, 18 deposit-temp-commutes0, 19 deposit-temp-deposit-alist-value

-commute2, 23 deposit-temp-deposit-array-value

-commute, 19 -commute2, 19 -commute3, 21 -commute5, 23

deposit-temp-deposit-temp-commute

2, 22 deposit-temp-doesnt-affect-fetc

h-n-temp-stk-elements, 37 h-temp, 37

deposit-temp-doesnt-affect-map-down-values, 30 deposit-temp-length-cons, 41 deposit-temp-map-down-values-co

mmute, 26 mmute-2, 27

deposit-temp-never-shrinks, 7 deposit-temp-preserves-length, 4 deposit-temp-preserves-plistp, 42 disjoint, 17, 20, 38 distinct-array-values-disjoint, 17 distinct-array-values-one-way-di

sjoint, 17 distinct-variables-lemma2, 17 distinct-variables-lemma2-base-

case, 16 double-cdr-induction2, 22

extra-binding-doesnt-affect-col

lect-pointers, 14 extra-bindings-dont-affect-colle

ct-pointers, 13 ct-pointers2, 14

extra-bindings-dont-affect-depo sit-alist-value, 5

fetch-adp, 36 fetch-n-temp-stk-elements, 4, 35, 38,

39 fetch-n-temp-stk-elements-invert

s-deposit-array-value, 39 fetch-temp, 3, 4, 35, 37 fetch-temp-stk-elements-inducti

on-hint, 38, 39 formal-type, 32

get, 31, 37

index, 2 int-literalp, 1

length, 1, 3, 4, 6–11, 14, 16–22, 31,

32, 37–39, 41, 42 length-ascending-local-address-

sequence, 32 length-mg-to-p-simple-literal-li

st, 1 length-plistp, 6 lesser-number-not-member-n-succe

ssive-pointers, 12 lessp-transitive2, 7 listcars, 5, 8, 13, 14, 27–29, 41 listcars-restriction1, 29

m-type, 4, 8–10 m-value, 4 map-down-values, 4, 5, 7, 10, 11,

26–31, 39–41 map-down-values-commute, 30 map-down-values-commutes1, 28 map-down-values-deposit-alist-v

alue-commute, 26 map-down-values-distributes, 5 map-down-values-doesnt-affect-m

g-vars-list-ok, 11 map-down-values-never-shrinks, 7 map-down-values-not-affected-by

-extra-binding, 5 map-down-values-preserves-lengt

h, 10 map-down-values-preserves-plistp, 5 map-up, 36 map-up-map-down-preserves-mg-ali

st-elements-equal, 39 map-up-vars-list, 36, 40 map-up-vars-list-array, 35, 36 map-up-vars-list-element, 36, 39 map-up-vars-list-simple-element, 35,

36 meaning-restriction-append1, 29 member-array-lengths-match, 10 member-pointer-collect-pointers, 15 mg-alist-elementp, 39 mg-alistp, 9–11, 14, 16–19, 21–31,

39–41 mg-cond-to-p-nat, 3 mg-name-alistp, 15, 16 mg-state, 36 mg-to-p-simple-literal, 1, 2, 4, 27,

28, 30, 31, 40–42 mg-to-p-simple-literal-list, 1, 2, 39,

42 mg-to-p-simple-literal-list-pli

stp, 1 mg-var-ok-array-index-ok, 9 mg-var-ok-array-index-ok2, 10 mg-var-ok-car-definedp, 22 mg-var-ok-in-p-state, 8, 9 mg-var-ok-temp-stk-index, 8 mg-var-ok-untag-value-numberp, 9 mg-var-ok-value-lessp-length-te

mp-stk, 9 mg-vars-list-members-ok-vars, 9 mg-vars-list-ok-in-p-state, 8–12, 17–

31, 39–41 mg-vars-list-ok-in-p-state-cdr, 8 mg-vars-list-ok-in-p-state-dist

ributes, 8 mg-vars-list-ok-reorder-cars, 8 mg-vars-list-ok-sensitive-to-te mp-stk-length2, 9 mg-vars-list-ok-strip-off-car, 8 multiple-deposit-array-values-c

ancel, 22 multiple-deposit-temps-cancel, 22 multiple-rputs-cancel, 22

n-successive-pointers, 12–14, 16, 17, 19, 20, 33, 34, 37, 38

n-successive-pointers-plistp, 12 new-binding-doesnt-disturb-map-

down-values, 5 no-duplicates, 12–14, 16, 29, 34 no-duplicates-all-pointers-disj

oint, 34 oint2, 34

no-duplicates-successive-pointe

rs, 12 no-p-aliasing, 14–17, 19–31, 34, 39–

41 no-p-aliasing-append-commutes, 15 no-p-aliasing-append1, 34 no-p-aliasing-cdr, 14 no-p-aliasing-cdr-append, 15 no-p-aliasing-cdr2, 15 no-p-aliasing-cons-cdr, 15 no-p-aliasing-distinct-variable

s, 16

s-base-case, 16 s-base-case0, 16

nth, 3

ok-actual-params-list, 11, 12 ok-cc, 3 ok-mg-array-value, 41 ok-mg-formal-data-params-plistp, 12 ok-mg-valuep, 41 ok-temp-stk-array-index, 6, 8, 12 ok-temp-stk-array-index-sensitive

-to-length, 6 ok-temp-stk-array-simple-member, 12 ok-temp-stk-index, 6, 8, 11, 12 ok-temp-stk-index-actual, 11 ok-temp-stk-index-array-actual, 12 ok-temp-stk-index-sensitive-to-

length, 6 ok-temp-stk-simple-member, 11 one-way-disjoint, 17, 20 one-way-disjoint-non-member-n-s

uccessive-pointers, 20

p-ctrl-stk, 36 p-data-segment, 36 p-nat-to-mg-cond, 3, 36 p-temp-stk, 36 p-to-mg-simple-literal, 1, 2, 35 p-to-mg-simple-literal-list, 2, 35 p-to-mg-to-p-simple-literal, 2 p-to-mg-to-p-simple-literal-list, 2 piton-cc, 36 plistp, 1, 5, 11–13, 29, 30, 32, 41, 42 pointers-bigger-monotonic, 33 push, 38 put, 37 put-doesnt-affect-get, 37

restrict, 29 reverse, 42 rget, 3, 31, 37, 38, 40 rget-array-index-mapping, 31 rget-array-index-mapping0, 31 rget-array-mapping-induction-hi

nt, 30, 31 rget-rewrite1, 40 rput, 3, 22, 27, 28, 31, 37, 41 rput-doesnt-affect-rget, 37

set-alist-value, 41

set-alist-value-deposit-array-v alue-relation, 41 set-alist-value-deposit-temp-re

lation, 40 signature, 40 signatures-match, 11, 13, 15 signatures-match-preserves-colle

ct-pointers, 13 signatures-match-preserves-mg-v

ars-list-ok, 11 signatures-match-preserves-no-p

-aliasing, 15 simple-identifierp, 40, 41 simple-mg-type-refp, 4, 8–14, 16–18,

20–25, 27, 28, 32, 36, 39 simple-typed-literal-plistp, 2, 39 simple-typed-literalp, 2, 39 simple-vars-have-simple-values, 39 subset, 14 successive-pointers-bigger, 34 successive-pointers-bigger-indu

ction-hint, 33 successive-pointers-bigger0, 33 successive-pointers-smaller2, 34

tag, 32–34, 41, 42

top, 36 type, 6

untag, 3, 4, 6, 8–13, 15–22, 27, 28, 31, 34, 37–41

value, 8, 31, 40, 41