I attached the wrong file yesterday.
From: Long Duong
I realize my attempt yesterday at asking my question didn’t have enough
information so I’m sending my pvs file with the question again.
I’m trying to construct a machine that keeps a running list of add requests
from arbitrary users modeled as nat IDs. When the machine encounters a
later access request by that same ID, the access is allowed. I’m trying
to prove that any given access allowed through to the machine output must
have been preceded by a previous [add ID] machine input, see theorem
in the attached pvs file.
I’m having a hard time trying to prove this. Thank you for any help with the
proof or with any suggestion for a better model.
Long Duong, Ph.D
Description: Binary data