[sv-ac] 1668 update

Hi Folks:

I have good news about 1668.  I got the intuition last Monday
that introducing the parenthesized, scoped local variable 
declarations to the abstract syntax should be able to give
us a good solution for local variable declaration assignments
even for sequences that admit empty match.

I have spent a lot of time this past week working out the
theory for this, and it looks very good to me.  I have attached
my plain text notes, which I will also put on mantis.

I intend to revise the proposal documents to remove the restriction
disallowing empty match, one which I have never liked.

I also introduced a formal definition of admits_empty at the
level of the abstract syntax to address Dmitry's concerns.  I 
carried out the proof that this definition faithfully represents
at that level the notion of admitting tight satisfaction by the
empty word after local variable declaration assignments and
clocks are eliminated.  This was not as easy as I had hoped, but
maybe the proofs can be simplified.

Please have a look and send any feedback that you have.

J.H.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.


-------------------------------
2007-08-18

In the updated technical report on local variables deposited with
Mantis 1549, it is shown how to incorporate local variable declarations
into the abstract syntax for sequences within a parenthesized scope:

   (t v; r)

It is shown how to define the functions sample, block, and flow 
for this form so that all the theory in that technical report 
continues to hold:

   sample((t v; r)) = sample(r) - {v}
   block((t v; r))  = block(r) - {v}
   flow(X,(t v; r)) = (X \cap {v}) \cup (flow(X-{v},r) - {v})

The objective of these notes is to show how the scoping aspect of
these definitions allows us cleanly and clearly to solve the problem
of attaching a local variable declaration assignment to a sequence
that may or may not admit empty match, a problem that has been been
confounding me up until now.

Let's recall what was troublesome about allowing empty match.  For
simplicity, let r be an unclocked sequence, and suppose that we want
to attach the local variable declaration assignment v = e.

The following is from the draft plain text proposal that was originally 
deposited on Mantis:

   1. Sequences.  This may have a flow problem:
   
     (r intersect 1[*0])  // r matches empty, no assignment
     or 
     ((1, v=e) ##0 r)     // non-empty match of r fused with initialization
   
        flow(X, (r intersect 1[*0]))
        = (flow(X,r) \cup flow(X,1[*0])) - block(r)
        = (flow(X,r) \cup X) - block(r)
        = [Theorem 4.1]
          ( 
             ((X \cup flow({},r)) - block(r))
             \cup X
          ) - block(r) 
        = (((X \cup flow({},r)) - block(r)) - block(r)) \cup (X - block(r))
        = ((X \cup flow({},r)) - block(r)) \cup (X - block(r))
        = (X \cup flow({},r) \cup X) - block(r)
        = (X \cup flow({},r)) - block(r)
        = flow(X,r)
        
        flow(X, ((1, v=e) ##0 r))
        = flow(flow(X, (1,v=e)), r)
        = flow(X \cup {v}, r)
   
     Therefore the overall flow of X through the "or" is
   
        flow(X,r) \cap flow(X\cup{v}, r)
   
     which in general can throw away the v.

In fact, from Proposition 4.3 in the technical report it follows that

   flow(X,r) \cap flow(X\cup{v},r) = flow(X,r)

The concern and confusion has been over the way that v is handled and
does or does not flow out when empty match is or is not possible, and
if possible, whether the current attempt matches empty or not.  For 
example, if r does not admit empty match, then why doesn't this behave 
the same way as ((1,v=e) ##0 r), for which

   flow(X, ((1,v=e) ##0 r)) = flow(X\cup{v},r)  ?


The treatment below shows that by using the scoped local variable
declarations, we get a cleaner result:

    R = (t v=e; r)   

is rewritten to

    R' = (t v; ( ((1,v=e) ##0 r) or (r intersect 1[*0]) ) )

and we get

    sample(R) = sample(R')
    block(R)  = block(R')
    flow(X,R) = flow(X,R')

regardless of whether or not r admits empty match.  The flow rule is

   flow(X,(t v=e; r))
   = flow(X,(t v; r)) 
   = (X \cap {v}) \cup (flow(X-{v},r) - {v})

This makes clear that if there is an outside v in X, it is preserved,
but the inside v in (t v=e; r) does not flow out of this scope.

These notes also show that sample, block, and flow can be lifted to
the level of the abstract syntax with clocks.  Basically, they are
independent of clocks.  This is done by giving the obvious definitions
at the higher level and showing that the functions are invariant under
the clock rewrite transformations.

The notes also define a function admits_empty at the level of the abstract
syntax, which captures the intuitive notion of admitting empty match.
This function is needed in order to define precisely in 1668 the case
splitting for the push function prior to the definition of tight satisfaction.
It is proved that admits_empty does the right thing by showing that for
any r without local variable declaration assignments or clocks and any
local variable context L,

   admits_empty(r) = 1  iff  \emptyword,L,L|_{flow(dom(L),r)} |== r


Along the way it is shown that 

   admits_empty(r) = 1  =>  flow(X,r) \subseteq X

This actually explains the some of the mystery of how the originally conceived 
formulation of attaching declaration assignment v=e to r as

   R' = ( ((1,v=e) ##0 r) or (r intersect 1[*0]) )    

works.  It says that if r admits empty match, then v flows out of r and R' only
if v flows in.  One can check that in the case of an empty match, the value that
flows out is the same as the value that flows in, but in the case of a non-empty
match the value that flows out is affected by the declaration assignment and
other possible assignments within r.  

This situation is actually not desirable for the semantics of a scoped
variable, since we do not want v to flow out at all, but without the
parenthesized scopes in the abstract syntax, the problem would be
solved by uniquefying names so that it doesn't matter if v flows out.

Regardless of whether the original formulation can be made to work with
unique name, I think that the formulation with the parenthesized, scoped local 
variable declarations is much better.


===================================================================================

First, we lift the functions sample, block, and flow to work on the
abstract syntax and argue that they are preserved through the
transformations that eliminate local variable declarations and clocks.
To avoid confusion, capital letters will be used at the level of the
abstract syntax, i.e., Sample, Block, and Flow.

In fact, we generalize the abstract syntax for sequences to

R ::= (t v[=e]; R)  
   |  (1, v=e)
   |  b
   |  (R)
   |  (R ##1 R)
   |  (R ##0 R)
   |  (R or R)
   |  (R intersect R)
   |  first_match(R)
   |  R[*0]
   |  R[*1:$]
   |  @(b) R


DEFINITION 1 (Sample):
. Sample((t v[=e]; r)) = Sample(r) - {v}
. Sample((1, v=e)) = {v}
. Sample(b) = {}
. Sample((r)) = Sample(r)
. Sample((r ##1 s)) = Sample(r) \cup Sample(s)
. Sample((r ##0 s)) = Sample(r) \cup Sample(s)
. Sample((r or s)) = Sample(r) \cup Sample(s)
. Sample((r intersect s)) = Sample(r) \cup Sample(s)
. Sample(first_match(r)) = Sample(r)
. Sample(r[*0]) = {}
. Sample(r[*1:$]) = Sample(r)
. Sample(@(b)r) = Sample(r)
////

DEFINITION 2 (Block):
. Block((t v[=e]; r)) = Block(r) - {v}
. Block((1, v=e)) = {}
. Block(b) = {}
. Block((r)) = Block(r)
. Block((r ##1 s)) = (Block(r) - Flow({},s)) \cup Block(s)
. Block((r ##0 s)) = (Block(r) - Flow({},s)) \cup Block(s)
. Block((r or s)) = Block(r) \cup Block(s)
. Block((r intersect s)) = Block(r) \cup Block(s) \cup (Sample(r) \cap Sample(s))
. Block(first_match(r)) = Block(r)
. Block(r[*0]) = {}
. Block(r[*1:$]) = Block(r)
. Block(@(b)r) = Block(r)
////

DEFINIION 3 (Flow):
. Flow(X,(t v[=e]; r)) = (X \cap {v}) \cup (Flow(X-{v},r) - {v})
. Flow(X,(1, v=e)) = X \cup {v}
. Flow(X,b) = X
. Flow(X,(r)) = Flow(X,r)
. Flow(X,(r ##1 s)) = Flow(Flow(X,r),s)
. Flow(X,(r ##0 s)) = Flow(Flow(X,r),s)
. Flow(X,(r or s)) = Flow(X,r) \cap Flow(X,s)
. Flow(X,(r intersect s)) 
  = (Flow(X,r) \cup Flow(X,s)) - Block((r intersect s))
  = (Flow(X,r) \cup Flow(X,s)) - (Block(r) \cup Block(s) \cup (Sample(r) \cap Sample(s)))
. Flow(X,first_match(r)) = Flow(X,r)
. Flow(X,r[*0]) = X
. Flow(X,r[*1:$]) = Flow(X,r)
. Flow(X,@(b)r) = Flow(X,r)
////

DEFINITION 4 (admits_empty):
. admits_empty((t v[=e]; r)) = admits_empty(r)
. admits_empty((1, v=e)) = 0
. admits_empty(b) = 0
. admits_empty((r)) = admits_empty(r)
. admits_empty((r ##1 s)) = admits_empty(r) && admits_empty(s)
. admits_empty((r ##0 s)) = 0
. admits_empty((r or s)) = admits_empty(r) || admits_empty(s)
. admits_empty((r intersect s)) = admits_empty(r) && admits_empty(s)
. admits_empty(first_match(r)) = admits_empty(r)
. admits_empty(r[*0]) = 1
. admits_empty(r[*1:$]) = admits_empty(r)
. admits_empty(@(b)r) = admits_empty(r)
////


CLAIM 5:  If admits_empty(r) = 1, then Flow(X,r) \subseteq X.

PROOF:  By induction.  Assume that admits_empty(r) = 1.

. r = (t v[=e]; s).  Then admits_empty(s) = 1.

  Flow(X,(t v[=e]; s))
  = (X \cap {v}) \cup (Flow(X-{v},s) - {v})
  \subseteq [induction]
    (X \cap {v}) \cup ((X-{v}) - {v})
  = X

. r = b.  There is nothing to show since admits_empty(r) = 0.

. r = (1, v=e).  There is nothing to show since admits_empty(r) = 0.

. r = (s).  Then admits_empty(s) = 1.

  Flow(X,(s))
  = Flow(X,s)
  \subseteq [induction]
    X

. r = (s ##1 s').  Then admits_empty(s) = admits_empty(s') = 1.

  Flow(X,(s ##1 s'))
  = Flow(Flow(X,s),s')
  \subseteq [induction]
    Flow(X,s)
  \subseteq [induction]
    X

. r = (s ##0 s').  There is nothing to show since admits_empty(r) = 0.

. r = (s or s').  Then either admits_empty(s) = 1 or admits_empty(s') = 1.
  Assume WLOG that admits_empty(s) = 1.

  Flow(X,(s or s'))
  = Flow(X,s) \cap Flow(X,s')
  \subseteq Flow(X,s)
  \subseteq [induction]
    X

. r = (s intersect s').  Then admits_empty(s) = admits_empty(s') = 1.
  
  Flow(X,(s intersect s'))
  \subseteq Flow(X,s) \cup Flow(X,s')
  \subseteq [induction]
    X \cup X
  = X

. r = first_match(s).  Then admits_empty(s) = 1.

  Flow(X,first_match(s))
  = Flow(X,s)
  \subseteq [induction]
    X

. r = s[*0].  

  Flow(X,s[*0])
  = X

. r = s[*1:$].  Then admits_empty(s) = 1.
  
  Flow(X,s[*1:$])
  = Flow(X,s)
  \subseteq [induction]
    X

. r = @(b) s.  Then admits_empty(s) = 1.

  Flow(X,@(b) s)
  = Flow(X,s)
  \subseteq [induction]
    X

////


CLAIM 6:  Let k be either @(b) or the empty string.

     Sample( ( t v; k ( ((1,v=e) ##0 (r)) or ((r) intersect 1[*0]) ) ) ) 
   = Sample( ( t v; k ( ((1,v=e) ##0 (r)) or                1[*0]  ) ) )
   = Sample( ( t v; k   ((1,v=e) ##0 (r))                            ) ) 
   = Sample((t v[=e]; r))
   = Sample(r) - {v}

PROOF:  The last equality is by definition.

     Sample( ( t v; k ( ((1,v=e) ##0 (r)) or ((r) intersect 1[*0]) ) ) ) 
   = Sample(        k ( ((1,v=e) ##0 (r)) or ((r) intersect 1[*0]) )   ) - {v}
   = Sample(          ( ((1,v=e) ##0 (r)) or ((r) intersect 1[*0]) )   ) - {v}
   = (
        Sample( ((1,v=e) ##0 (r)) ) 
        \cup 
        Sample( ((r) intersect 1[*0])) )
     ) - {v}
   = ( 
        ( Sample((1,v=e)) \cup Sample((r)) )
        \cup
        ( Sample((r)) \cup Sample(1[*0]) )
     ) - {v}
   = ( 
        ( {v}             \cup Sample(r)   )
        \cup 
        ( Sample(r)   \cup {}            )
     ) - {v}
   = Sample(r) - {v}

     Sample( ( t v; k ( ((1,v=e) ##0 (r)) or 1[*0] ) ) )
   = Sample(        k ( ((1,v=e) ##0 (r)) or 1[*0] )   ) - {v}
   = Sample(          ( ((1,v=e) ##0 (r)) or 1[*0] )   ) - {v}
   = (
        Sample( ((1,v=e) ##0 (r)) ) 
        \cup 
        Sample(1[*0])
     ) - {v}
   = ( 
        ( Sample((1,v=e)) \cup Sample((r)) )
        \cup
        {}
     ) - {v}
   = ( 
        ( {v}             \cup Sample(r)   )
     ) - {v}
   = Sample(r) - {v}

     Sample( ( t v; k ((1,v=e) ##0 (r)) ) )
   = Sample(        k ((1,v=e) ##0 (r))   ) - {v}
   = Sample(          ((1,v=e) ##0 (r))   ) - {v}
   = ( 
        Sample((1,v=e)) \cup Sample((r))
     ) - {v}
   = ( 
        {v}             \cup Sample(r)
     ) - {v}
   = Sample(r) - {v}

////


CLAIM 7:  Let k be either @(b) or the empty string.

     Block( ( t v; k ( ((1,v=e) ##0 (r)) or ((r) intersect 1[*0]) ) ) )
   = Block( ( t v; k ( ((1,v=e) ##0 (r)) or                1[*0]  ) ) )
   = Block( ( t v; k   ((1,v=e) ##0 (r))                            ) ) 
   = Block((t v[=e]; r))
   = Block(r) - {v}

PROOF:  The last equality is by definition.

     Block( ( t v; k ( ((1,v=e) ##0 (r)) or ((r) intersect 1[*0]) ) ) )
   = Block(        k ( ((1,v=e) ##0 (r)) or ((r) intersect 1[*0]) )   ) - {v}
   = Block(          ( ((1,v=e) ##0 (r)) or ((r) intersect 1[*0]) )   ) - {v}
   = ( 
        Block( ((1,v=e) ##0 (r)) ) 
        \cup 
        Block( ((r) intersect 1[*0]) ) 
     ) - {v}
   = ( 
        ( ( Block((1,v=e)) - Flow({},(r)) ) \cup Block((r)) ) 
        \cup 
        ( Block((r)) \cup Block(1[*0]) \cup ( Sample((r)) \cap Sample(1[*0]) ) )
     ) - {v}
   = ( 
        ( ( {}             - Flow({},r)   ) \cup Block(r)   ) 
        \cup 
        ( Block(r)   \cup {}           \cup ( Sample(r)   \cap {}            ) )
     ) - {v}
   = Block(r) - {v}

     Block( ( t v; k ( ((1,v=e) ##0 (r)) or 1[*0] ) ) )
   = Block(        k ( ((1,v=e) ##0 (r)) or 1[*0] )   ) - {v}
   = Block(          ( ((1,v=e) ##0 (r)) or 1[*0] )   ) - {v}
   = ( 
        Block( ((1,v=e) ##0 (r)) ) 
        \cup 
        Block(1[*0]) 
     ) - {v}
   = ( 
        ( ( Block((1,v=e)) - Flow({},(r)) ) \cup Block((r)) ) 
        \cup 
        {}
     ) - {v}
   = ( 
        ( ( {}             - Flow({},r)   ) \cup Block(r)   ) 
     ) - {v}
   = Block(r) - {v}

     Block( ( t v; k ( ((1,v=e) ##0 (r)) or 1[*0] ) ) ) 
   = Block(        k ( ((1,v=e) ##0 (r)) or 1[*0] )   ) - {v}
   = Block(          ( ((1,v=e) ##0 (r)) or 1[*0] )   ) - {v}
   = ( 
        Block( ((1,v=e) ##0 (r)) ) 
        \cup 
        Block(1[*0]) 
     ) - {v}
   = ( 
        ( ( Block((1,v=e)) - Flow({},(r)) ) \cup Block((r)) ) 
        \cup 
        {}
     ) - {v}
   = ( 
        ( ( {}             - Flow({},r)   ) \cup Block(r)   ) 
     ) - {v}
   = Block(r) - {v}

////


THEOREM 8:  Let r be a sequence in the abstract syntax.

1. Flow(X,r)  =  (X \cup Flow({},r)) - Block(r).

2. Flow({},r) \subseteq Sample(r).

3. Block(r) \subseteq Sample(r).

PROOF:  Theorems 4.1 and 4.5 in the updated technical report on local
variables prove these results by induction over the structure of r for
sample, block, flow extended with the sequence form r = (t v; s).  The
definitions of Sample, Block, and Flow agree with those of sample,
block, and flow (resp.) on all the shared forms.  The definitions of
Sample, Block, and Flow on the form r = (t v=e; s) agree with those
for the form r = (t v; s), so the form r = (t v=e; s) is already
covered by the inductive proofs in the updated technical report.  It
remains to give the inductive proofs for the form r = @(b) s.

. r = @(b) s.

  Flow(X,@(b) s)
  = Flow(X,s)
  = [induction]
    (X \cup Flow({},s)) - Block(s)
  = (X \cup Flow({},@(b) s)) - Block(@(b) s)

  Flow({},@(b) s)
  = Flow({},s)
  \subseteq [induction]
    Sample(s)
  = Sample(@(b) s)

  Block(@(b) s)
  = Block(s)
  \subseteq [induction]
    Sample(s)
  = Sample(@(b) s)

////


CLAIM 9:

1.   Flow( X, ( t v; @(b) ( ((1,v=e) ##0 (r)) or ((r) intersect 1[*0]) ) ) )
   = Flow( X, ( t v; @(b)   ((1,v=e) ##0 (r))                            ) ) 
   = Flow(X,(t v[=e]; r))
   = (X \cap {v}) \cup (Flow(X-{v},r) - {v})

2. If admits_empty(r) = 1, then

   = Flow( X, ( t v; @(b) ( ((1,v=e) ##0 (r)) or 1[*0]  ) ) )
   = Flow(X,(t v[=e]; r))
   = (X \cap {v}) \cup (Flow(X-{v},r) - {v})

PROOF:  In each part, the last equality is by definition.

1. 

     Flow( X, ( t v; @(b) ( ((1,v=e) ##0 (r)) or ((r) intersect 1[*0]) ) ) )
   = (X \cap {v})
     \cup
     ( Flow( X-{v},  @(b) ( ((1,v=e) ##0 (r)) or ((r) intersect 1[*0]) )   ) - {v} )
   = (X \cap {v})
     \cup
     ( Flow( X-{v},       ( ((1,v=e) ##0 (r)) or ((r) intersect 1[*0]) )   ) - {v} )
   = (X \cap {v})
     \cup
     ( 
        (
           Flow( X-{v}, ((1,v=e) ##0 (r)) )
           \cap
           Flow( X-{v}, ((r) intersect 1[*0]) )
        )
        - {v} 
     )
   = (X \cap {v})
     \cup
     ( 
        (
           Flow( Flow( X-{v}, (1,v=e) ), (r) )
           \cap
           (
              (
                 Flow( X-{v}, (r) )
                 \cup 
                 Flow( X-{v}, 1[*0] ) 
              )
              -
              (
                 Block((r))
                 \cup
                 Block(1[*0])
                 \cup
                 ( Sample((r)) \cap Sample(1[*0]) )
              )
           )
        )
        - {v} 
     )
   = (X \cap {v})
     \cup
     ( 
        (
           Flow( (X-{v}) \cup {v}, r )
           \cap
           (
              (
                 Flow( X-{v}, r )
                 \cup 
                 (X-{v}) 
              )
              -
              (
                 Block(r)
                 \cup
                 {}
                 \cup
                 ( Sample(r) \cap {} )
              )
           )
        )
        - {v} 
     )
   = (X \cap {v})
     \cup
     ( 
        (
           Flow(X,r)
           \cap
           (
              (
                 Flow( X-{v}, r )
                 \cup 
                 (X-{v}) 
              )
              -
              Block(r)
           )
        )
        - {v} 
     )
   = [Theorem 8.1]
     (X \cap {v})
     \cup
     ( 
        (
           ( (X \cup Flow({},r)) - Block(r) ) // Flow(X,r)
           \cap
           (
              (
                 ( ( (X-{v}) \cup Flow({},r) ) - Block(r) )  // Flow( X-{v}, r )
                 \cup 
                 (X-{v}) 
              )
              -
              Block(r)
           )
        )
        - {v} 
     )
   = [((A - M) \cup B) - M = (A \cup B) - M]
     (X \cap {v})
     \cup
     ( 
        (
           ( (X \cup Flow({},r)) - Block(r) )
           \cap
           (
              (
                 (X-{v}) \cup Flow({},r)
              )
              -
              Block(r)
           )
        )
        - {v} 
     )
   = [(A - M) \cap (B - M) = (A \cap B) - M]
     (X \cap {v})
     \cup
     ( 
        (
           (
              (  X      \cup Flow({},r) )
              \cap
              ( (X-{v}) \cup Flow({},r) )
           )
           -
           Block(r)
        )
        - {v} 
     )
   = (X \cap {v})
     \cup
     ( 
        (
           (
              (X-{v}) \cup Flow({},r)
           )
           -
           Block(r)
        )
        - {v} 
     )
   = [Theorem 8.1]
     (X \cap {v})
     \cup
     ( 
        Flow(X-{v},r)
        - {v} 
     )


     Flow( X, ( t v; @(b) ((1,v=e) ##0 (r)) ) )
   = (X \cap {v})
     \cup
     ( Flow( X-{v},  @(b) ((1,v=e) ##0 (r))   ) - {v} )
   = (X \cap {v})
     \cup
     ( Flow( X-{v},       ((1,v=e) ##0 (r))   ) - {v} )
   = (X \cap {v})
     \cup
     ( 
        Flow( Flow( X-{v}, (1,v=e) ), (r) )
        - {v} 
     )
   = (X \cap {v})
     \cup
     ( 
        Flow( (X-{v}) \cup {v}, r )
        - {v} 
     )
   = (X \cap {v})
     \cup
     ( 
        Flow(X,r)
        - {v} 
     )
   = [Theorem 8.1]
     (X \cap {v})
     \cup
     ( 
        ( (X \cup Flow({},r)) - Block(r) ) // Flow(X,r)
        - {v} 
     )
   = (X \cap {v})
     \cup
     ( 
        ( ((X-{v}) \cup Flow({},r)) - Block(r) ) 
        - {v} 
     )
   = [Theorem 8.1]
     (X \cap {v})
     \cup
     ( 
        Flow(X-{v},r)
        - {v} 
     )


2. Assume that admits_empty(r) = 1.  By Claim 5, Flow(X,r) \subseteq X.

     Flow( X, ( t v; @(b) ( ((1,v=e) ##0 (r)) or 1[*0] ) ) )
   = (X \cap {v})
     \cup
     ( Flow( X-{v},  @(b) ( ((1,v=e) ##0 (r)) or 1[*0] )   ) - {v} )
   = (X \cap {v})
     \cup
     ( Flow( X-{v},       ( ((1,v=e) ##0 (r)) or 1[*0] )   ) - {v} )
   = (X \cap {v})
     \cup
     ( 
        (
           Flow( X-{v}, ((1,v=e) ##0 (r)) )
           \cap
           Flow( X-{v}, 1[*0] )
        )
        - {v} 
     )
   = (X \cap {v})
     \cup
     ( 
        (
           Flow( Flow( X-{v}, (1,v=e) ), (r) )
           \cap
           (X-{v})
        )
        - {v} 
     )
   = (X \cap {v})
     \cup
     ( 
        (
           Flow( (X-{v}) \cup {v}, r )
           \cap
           (X-{v})
        )
        - {v} 
     )
   = (X \cap {v})
     \cup
     ( 
        (
           Flow(X,r)
           \cap
           (X-{v})
        )
        - {v} 
     )
   = [(A \cap (B - M)) - M = (A \cap B) - M]
     (X \cap {v})
     \cup
     ( 
        (
           Flow(X,r)
           \cap
           X
        )
        - {v} 
     )
   = [Flow(X,r) \subseteq X]
     (X \cap {v})
     \cup
     ( 
        Flow(X,r)
        - {v} 
     )
   = [Theorem 8.1]
     (X \cap {v})
     \cup
     ( 
        ( (X \cup Flow({},r)) - Block(r) ) // Flow(X,r)
        - {v} 
     )
   = (X \cap {v})
     \cup
     ( 
        ( ((X-{v}) \cup Flow({},r)) - Block(r) ) 
        - {v} 
     )
   = [Theorem 8.1]
     (X \cap {v})
     \cup
     ( 
        Flow(X-{v},r)
        - {v} 
     )


////


REMARK 10:  Claim 6, 7, and 9 suggest that the following rewrite is
appropriate for any sequence r with unique semantic leading clock c.
If c is inherited, then let k(r) be the empty string.  Otherwise, let
k(r) = @(c).  Then

   (t v=e; r) 

is rewritten as

   ( k(r) ( ((1,v=e) ##0 (r)) or ((r) intersect 1[*0]) ) )

in all cases, regardless of admits_empty(r).  The claims show that the
rewrite preserves Sample, Block, and Flow.

Intuitively, k(r) ((1,v=e) ##0 (r)) gives the desired semantics for
non-empty matches of r, and ((r) intersect 1[*0]) preserves matching
by the emptyword in case the emptyword matches r.

The key insight leading to this rewrite is that by incorporating the
local variable declarations and declaration assignments into the
abstract syntax, we have been able to adapt the definitions of Sample,
Block, and Flow so that the previous theory continues to work and this
rewrite does not change these functions, even when r admits empty
match.

////


Next, we want to show that Sample, Block, Flow, and admits_empty do
not change under application of the clock rewrite rules.  This will
show that Sample, Block, and Flow descend to the original sample,
block, and flow after rewriting to eliminate local variable
declaration assignments and clocks.  It will also enable us to prove
that admits_empty faithfully represents, at the level of the abstract
syntax, the condition of being tightly satisfied by the empty word.

For this, a function notation for the rewrite rules is convenient,
so we change the notation to the following.  T^c denotes the function
that rewrites a sequence starting with clock c.  

[Recall that clock flow is not accounted for by the clock rewrite 
rules.  The clock rewrite rules assume that various explicit clocks
have been added to ensure that all terms are clocked in a way that 
the correct clock is obtained by recursive descent through the syntax.]


DEFINITION 11 (clock rewrite for sequences):
. T^c((t v[=e]; r)) = (t v[=e]; T^c(r))
. T^c((1,v=e)) = (T^c(1) ##0 (1,v=e))
. T^c(b) = (!c[*0:$] ##1 c && b)
. T^c((r)) = (T^c(r))
. T^c((r ##1 s)) = (T^c(r) ##1 T^c(s))
. T^c((r ##0 s)) = (T^c(r) ##0 T^c(s))
. T^c((r or s)) = (T^c(r) or T^c(s))
. T^c((r intersect s)) = (T^c(r) intersect T^c(s))
. T^c(first_match(r)) = first_match(T^c(r))
. T^c(r[*0]) = (T^c(r))[*0]
. T^c(r[*1:$]) = (T^c(r))[*1:$]
. T^c(@(b) r) = T^b(r)
////


Note that, for simplicity and generality, this definition includes 
sequences with local variable declaration assignments.  The 
correct sementics may not be obtained if clock rewrite rules are
applied before eliminating local variable declaration assignments.
Sample, Block, and Flow are oblivious to this distinction.

CLAIM 12:  Let r be a sequence.  Then for any c and X, 

   Sample(T^c(r))       = Sample(r)
   Block(T^c(r))        = Block(r)
   Flow(X,T^c(r))       = Flow(X,r)
   admits_empty(T^c(r)) = admits_empty(r)

PROOF:  By induction.

. r = (t v[=e]; s) 

  Sample( T^c((t v[=e]; s) ) 
  = Sample( (t v[=e]; T^c(s)) )
  = Sample(T^c(s)) - {v}
  = [induction]
    Sample(s) - {v}
  = Sample((t v[=e]; s))

  Block( T^c((t v[=e]; s)) ) 
  = Block((t v[=e]; T^c(s)))
  = Block(T^c(s)) - {v}
  = [induction]
    Block(s) - {v}
  = Block((t v[=e]; s))

  Flow( X, T^c((t v[=e]; s)) )
  = Flow( X, (t v[=e]; T^c(s)) )
  = (X\cap{v}) \cup ( Flow(X-{v},T^c(s)) - {v} )
  = [induction]
    (X\cap{v}) \cup ( Flow(X-{v},s) - {v} )
  = Flow(X,(t v[=e]; s))

  admits_empty( T^c((t v[=e]; s)) )
  = admits_empty( (t v[=e]; T^c(s)) )
  = admits_empty(T^c(s))
  = [induction]
    admits_empty(s)
  = admits_empty((t v[=e]; s))

. r = (1,v=e)

  Sample( T^c((1,v=e) ) 
  = Sample( (T^c(1) ##0 (1,v=e)) )
  = Sample(T^c(1)) \cup Sample((1,v=e))
  = [induction]
    Sample(1) \cup Sample((1,v=e))
  = {} \cup Sample((1,v=e))
  = Sample((1,v=e))

  Block( T^c((1,v=e) ) 
  = Block( (T^c(1) ##0 (1,v=e)) )
  = ( Block(T^c(1)) - Flow({},(1,v=e)) ) \cup Block((1,v=e))
  = [induction]
    ( Block(1) - Flow({},(1,v=e)) ) \cup Block((1,v=e))
  = ( {}       - {v}              ) \cup Block((1,v=e))
  = Block((1,v=e))

  Flow( X, T^c((1,v=e) ) 
  = Flow( X, (T^c(1) ##0 (1,v=e)) )
  = Flow( Flow(X,T^c(1)), (1,v=e) )
  = [induction]
    Flow( Flow(X,1), (1,v=e) )
  = Flow( X, (1,v=e) )

  admits_empty( T^c((1,v=e) ) 
  = admits_empty( (T^c(1) ##0 (1,v=e)) )
  = 0
  = admits_empty((1,v=e))

. r = b

  Sample(T^c(b))
  = Sample( (!c[*0:$] ##1 c && b) )
  = Sample(!c[*0:$]) \cup Sample(c && b)
  = Sample( (!c[*0] or !c[*1:$]) ) \cup {}
  = Sample(!c[*0]) \cup Sample(!c[*1:$])
  = {} or Sample(!c)
  = {}
  = Sample(b)

  Block(T^c(b))
  = Block( (!c[*0:$] ##1 c && b) )
  = ( Block(!c[*0:$]) - Flow({},c && b) ) \cup Block(c && b)
  = ( Block((!c[*0] or !c[*1:$])) - {}  ) \cup {}
  = Block(!c[*0]) \cup Block(!c[*1:$])
  = {}            \cup Block(!c)
  = {}
  = Block(b)

  Flow(X,T^c(b))
  = Flow( X, (!c[*0:$] ##1 c && b) )
  = Flow( Flow(X,!c[*0:$]), c && b )
  = Flow(X,!c[*0:$])
  = Flow( X, (!c[*0] or !c[*1:$]) )
  = Flow(X,!c[*0]) \cap Flow(X,!c[*1:$])
  = X              \cap Flow(X,!c)
  = X              \cap X
  = X
  = Flow(X,b)

  admits_empty(T^c(b))
  = admits_empty( (!c[*0:$] ##1 c && b) )
  = admits_empty(!c[*0:$]) && admits_empty(c && b)
  = admits_empty(!c[*0:$]) && 0
  = 0
  = admits_empty(b)

. r = (s)

  Sample(T^c((s)))
  = Sample((T^c(s)))
  = Sample(T^c(s))
  = [induction]
    Sample(s)
  = Sample((s))

  Block(T^c((s)))
  = Block((T^c(s)))
  = Block(T^c(s))
  = [induction]
    Block(s)
  = Block((s))

  Flow(X,T^c((s)))
  = Flow(X,(T^c(s)))
  = Flow(X,T^c(s))
  = [induction]
    Flow(X,s)
  = Flow(X,(s))

  admits_empty(T^c((s)))
  = admits_empty((T^c(s)))
  = admits_empty(T^c(s))
  = [induction]
    admits_empty(s)
  = admits_empty((s))

. r = (s ##1 s')

  Sample( T^c((s ##1 s')) )
  = Sample( (T^c(s) ##1 T^c(s')) )
  = Sample(T^c(s)) \cup Sample(T^c(s'))
  = [induction]
    Sample(s) \cup Sample(s')
  = Sample((s ##1 s'))

  Block( T^c((s ##1 s')) )
  = Block( (T^c(s) ##1 T^c(s')) )
  = ( Block(T^c(s)) - Flow({},T^c(s')) ) \cup Block(T^c(s'))
  = [induction]
    ( Block(s)      - Flow({},s')      ) \cup Block(s')
  = Block((s ##1 s'))

  Flow( X, T^c((s ##1 s')) )
  = Flow( X, (T^c(s) ##1 T^c(s')) )
  = Flow( Flow(X,T^c(s)), T^c(s') )
  = [induction]
    Flow( Flow(X,s), s')
  = Flow(X,(s ##1 s'))

  admits_empty( T^c((s ##1 s')) )
  = admits_empty( (T^c(s) ##1 T^c(s')) )
  = admits_empty(T^c(s)) && admits_empty(T^c(s'))
  = [induction]
    admits_empty(s) && admits_empty(s')
  = admits_empty((s ##1 s'))

. r = (s ##0 s')

  Sample( T^c((s ##0 s')) )
  = Sample( (T^c(s) ##0 T^c(s')) )
  = Sample(T^c(s)) \cup Sample(T^c(s'))
  = [induction]
    Sample(s) \cup Sample(s')
  = Sample((s ##0 s'))

  Block( T^c((s ##0 s')) )
  = Block( (T^c(s) ##0 T^c(s')) )
  = ( Block(T^c(s)) - Flow({},T^c(s')) ) \cup Block(T^c(s'))
  = [induction]
    ( Block(s)      - Flow({},s')      ) \cup Block(s')
  = Block((s ##0 s'))

  Flow( X, T^c((s ##0 s')) )
  = Flow( X, (T^c(s) ##0 T^c(s')) )
  = Flow( Flow(X,T^c(s)), T^c(s') )
  = [induction]
    Flow( Flow(X,s), s')
  = Flow(X,(s ##0 s'))

  admits_empty( T^c((s ##0 s')) )
  = admits_empty( (T^c(s) ##0 T^c(s')) )
  = 0
  = admits_empty((s ##0 s'))
  
. r = (s or s')

  Sample( T^c((s or s')) )
  = Sample( (T^c(s) or T^c(s')) )
  = Sample(T^c(s)) \cup Sample(T^c(s'))
  = [induction]
    Sample(s) \cup Sample(s')
  = Sample((s or s'))

  Block( T^c((s or s')) )
  = Block( (T^c(s) or T^c(s')) )
  = Block(T^c(s)) \cup Block(T^c(s'))
  = [induction]
    Block(s) \cup Block(s')
  = Block((s or s'))

  Flow( X, T^c((s or s')) )
  = Flow( X, (T^c(s) or T^c(s')) )
  = Flow(X,T^c(s)) \cap Flow(X,T^c(s'))
  = [induction]
    Flow(X,s) \cap Flow(X,s')
  = Flow(X,(s or s'))

  admits_empty( T^c((s or s')) )
  = admits_empty( (T^c(s) or T^c(s')) )
  = admits_empty(T^c(s)) || admits_empty(T^c(s'))
  = [induction]
    admits_empty(s) || admits_empty(s')
  = admits_empty((s or s'))

. r = (s intersect s')

  Sample( T^c((s intersect s')) )
  = Sample( (T^c(s) intersect T^c(s')) )
  = Sample(T^c(s)) \cup Sample(T^c(s'))
  = [induction]
    Sample(s) \cup Sample(s')
  = Sample((s intersect s'))

  Block( T^c((s intersect s')) )
  = Block( (T^c(s) intersect T^c(s')) )
  = Block(T^c(s)) \cup Block(T^c(s')) \cup ( Sample(T^c(s)) \cap Sample(T^c(s')) )
  = [induction]
    Block(s) \cup Block(s') \cup ( Sample(s) \cap Sample(s') )
  = Block((s intersect s'))

  Flow( X, T^c((s intersect s')) )
  = Flow( X, (T^c(s) intersect T^c(s')) )
  = ( Flow(X,T^c(s)) \cup Flow(X,T^c(s')) ) 
    - ( Block(T^c(s)) \cup Block(T^c(s')) \cup ( Sample(T^c(s)) \cap Sample(T^c(s')) ) )
  = [induction]
  = ( Flow(X,s) \cup Flow(X,s') ) 
    - ( Block(s) \cup Block(s') \cup ( Sample(s) \cap Sample(s') ) )
  = Flow(X,(s intersect s'))

  admits_empty( T^c((s intersect s')) )
  = admits_empty( (T^c(s) intersect T^c(s')) )
  = admits_empty(T^c(s)) && admits_empty(T^c(s'))
  = [induction]
    admits_empty(s) && admits_empty(s')
  = admits_empty((s intersect s'))

. r = first_match(s)

  Sample( T^c(first_match(s) )
  = Sample( first_match(T^c(s)) )
  = Sample(T^c(s))
  = [induction]
    Sample(s)
  = Sample(first_match(s))

  Block( T^c(first_match(s) )
  = Block( first_match(T^c(s)) )
  = Block(T^c(s))
  = [induction]
    Block(s)
  = Block(first_match(s))

  Flow( X, T^c(first_match(s) )
  = Flow( X, first_match(T^c(s)) )
  = Flow(X,T^c(s))
  = [induction]
    Flow(X,s)
  = Flow(X,first_match(s))

  admits_empty( T^c(first_match(s) )
  = admits_empty( first_match(T^c(s)) )
  = admits_empty(T^c(s))
  = [induction]
    admits_empty(s)
  = admits_empty(first_match(s))

. r = s[*0]

  Sample( T^c(s[*0]) )
  = Sample( (T^c(s))[*0] )
  = {}
  = Sample(s[*0])

  Block( T^c(s[*0]) )
  = Block( (T^c(s))[*0] )
  = {}
  = Block(s[*0])

  Flow( X, T^c(s[*0]) )
  = Flow( X, (T^c(s))[*0] )
  = X
  = Flow(X,s[*0])

  admits_empty( T^c(s[*0]) )
  = admits_empty( (T^c(s))[*0] )
  = 1
  = admits_empty(s[*0])

. r = s[*1:$]

  Sample( T^c(s[*1:$] )
  = Sample( (T^c(s))[*1:$] )
  = Sample(T^c(s))
  = [induction]
    Sample(s)
  = Sample(s[*1:$])

  Block( T^c(s[*1:$] )
  = Block( (T^c(s))[*1:$] )
  = Block(T^c(s))
  = [induction]
    Block(s)
  = Block(s[*1:$])

  Flow( X, T^c(s[*1:$] )
  = Flow( X, (T^c(s))[*1:$] )
  = Flow(X,T^c(s))
  = [induction]
    Flow(X,s)
  = Flow(X,s[*1:$])

  admits_empty( T^c(s[*1:$] )
  = admits_empty( (T^c(s))[*1:$] )
  = admits_empty(T^c(s))
  = [induction]
    admits_empty(s)
  = admits_empty(s[*1:$])

. r = @(b) s

  Sample( T^c(@(b) s) )
  = Sample(T^b(s))
  = [induction]
    Sample(s)
  = Sample(@(b) s)

  Block( T^c(@(b) s) )
  = Block(T^b(s))
  = [induction]
    Block(s)
  = Block(@(b) s)

  Flow( X, T^c(@(b) s) )
  = Flow(X,T^b(s))
  = [induction]
    Flow(X,s)
  = Flow(X,@(b) s)

////


In the LRM and the technical report, the notation L|_D is used only when 
D \subeteq dom(L).  We continue with this restriction to avoid confusion.

Part 1 of the next theorem is an analog of Claim 5 at the level of tight
satisfaction.  Part 2 confirms the intuitively reasonable expectation that
the outgoing local variable context from an empty match should be the 
restriction of the incoming local variable context to the variable that 
flow out.


THEOREM 13:  Let r be a sequence without local variable declaration
assignments and without clocks, and let L_0, L_1 be local variable
contexts.  If \emptyword,L_0,L_1 |== r, then

1. flow(dom(L_0),r) \subseteq dom(L_0).

2. L_1 = L_0|_{flow(dom(L_0),r)}.

PROOF:  By induction.  We use the abbreviation X/s = flow(X,s).

. r = (t v; s)

  1. \emptyword,L_0,L_1 |== (t v; s)
     =>  there exists L such that \emptyword,L_0\v,L |== s
     =>  [induction]
         dom(L_0\v)/s \subseteq dom(L_0)
     iff [dom(L\v) = dom(L) - {v}]
         A: (dom(L_0) - {v})/s \subseteq dom(L_0) 
     =>  [

            dom(L_0)/(t v; s)
            = (dom(L_0) \cap {v}) \cup ( ((dom(L_0) - {v})) / s) - {v} )
            \subseteq [by A] 
              (dom(L_0) \cap {v}) \cup ( dom(L_0)                - {v} )
            = dom(L_0)

         ]
         dom(L_0)/(t v; s) \subseteq dom(L_0)


  2. \emptyword,L_0,L_1 |== (t v; s)
     iff there exists L such that \emptyword,L_0\v,L |== s and
         L_1 = L_0[v] \cup (L\v)
     =>  [induction]
         L_1 = L_0[v] \cup ( L_0|_{dom(L_0\v)/s} \ v )
     iff [
     
              L_0[v] \cup ( L_0|_{ dom(L_0\v) / s } \ v )
            
            = [ dom(L\v) = dom(L) - {v} ]
            
              L_0[v] \cup ( L_0|_{ (dom(L_0) - {v}) / s } \ v )
            
            = [ L|_D \ v = L|_{D - {v}} ]
            
              L_0[v] \cup L_0|_{ ( (dom(L_0) - {v}) / s ) - {v} }
            
            = [ L[v] \cup L|_D = L|_{ (dom(L)\cap{v}) \cup D } ]
            
              L_0|_{ (dom(L_0) \cap {v}) \cup ( ( (dom(L_0) - {v}) / s ) - {v}) }
            = L_0|_{ dom(L_0) / (t v; s) } 
     
         ]
         L_1 = L_0|_{ dom(L_0) / (t v; s) }

. r = (1,v=e)

  \emptyword,L_0,L_1 |== (1,v=e)
  iff [w,L_0,L_1 |== (1,v=e) => |w| = 1]
      FALSE
      
. r = b

  \emptyword,L_0,L_1 |== b
  iff [w,L,L' |== b => |w| = 1]
      FALSE

. r = (s)

  1. \emptyword,L_0,L_1 |== (s)
     iff \emptyword,L_0,L_1 |== s
     =>  [induction]
         dom(L_0)/s \subseteq dom(L_0)
     iff [X/s = X/(s)]
         dom(L_0)/(s) \subseteq dom(L_0)

  2. \emptyword,L_0,L_1 |== (s)
     iff \emptyword,L_0,L_1 |== s
     =>  [induction]
         L_1 = L_0|_{dom(L_0)/s}
     iff L_1 = L_0|_{dom(L_0)/(s)}


. r = (s ##1 s')

  1. \emptyword,L_0,L_1 |== (s ##1 s')

     iff there exist x,y,L' such that \emptyword = xy and x,L_0,L' |== s
         and y,L',L_1 |== s'

     =>  [\emptyword = xy => x = y = \emptyword]
         there exists L' such that \emptyword,L_0,L' |== s and
         \emptyword,L',L_1 |== s'

     =>  [induction, including part 2]
         both
            dom(L_0)/s \subseteq dom(L_0) 
         and 
            there exists L' such that L' = L_0|_{dom(L_0)/s} and dom(L')/s' \subseteq dom(L')

     iff [L' = L_0|_{dom(L_0)/s}]
         both
            dom(L_0)/s \subseteq dom(L_0) 
         and 
            dom( L_0|_{dom(L_0)/s} ) / s' \subseteq dom( L_0|_{dom(L_0)/s} )

     iff [dom(L_0)/s \subseteq dom(L_0) => dom(L_0|_{dom(L_0)/s}) = dom(L_0)/s]

         (dom(L_0)/s)/s' \subseteq dom(L_0)/s \subseteq dom(L_0)

     =>  [dom(L_0)/(s ##1 s') = (dom(L_0)/s)/s']
         dom(L_0)/(s ##1 s') \subseteq dom(L_0)

  2. \emptyword,L_0,L_1 |== (s ##1 s')
     iff there exist x,y,L' such that \emptyword = xy and x,L_0,L' |== s
         and y,L',L_1 |== s'
     =>  [\emptyword = xy => x = y = \emptyword]
         there exists L' such that \emptyword,L_0,L' |== s and
         \emptyword,L',L_1 |== s'
     =>  [induction]
         there exists L' such that L' = L_0|_{dom(L_0)/s} and
         L_1 = L'|_{dom(L')/s'}
     iff L_1 = ( L_0|_{dom(L_0)/s} ) |_{ dom( L_0|_{dom(L_0)/s} ) / s' }
     iff [
     
              ( L_0|_{dom(L_0)/s} ) |_{ dom( L_0|_{dom(L_0)/s} ) / s' }
            = [
                 from the argument for part 1, dom(L_0)/s \subseteq dom(L_0), 
                 and so dom( L_0|_{dom(L_0)/s} ) = dom(L_0)/s
              ]
              ( L_0|_{dom(L_0)/s} ) |_{ (dom(L_0)/s)/s' }
            = 
              L_0|_{ (dom(L_0)/s) \cap ( (dom(L_0)/s)/s' ) }

            = [ 
                 from the argument for part 1, (dom(L_0)/s)/s' \subseteq dom(L_0)/s
              ]
              L_0|_{(dom(L_0)/s)s'}

            = [dom(L_0)/(s ##1 s') = (dom(L_0)/s)/s']
              L_0|_{dom(L_0)/(s ##1 s')}

         ]
         L_1 = L_0|_{dom(L_0)/(s ##1 s')}

. r = (s ##0 s')

  \emptyword,L_0,L_1 |== (s ##0 s')
  iff [w,L_0,L_1 |== (s ##0 s') => |w| > 0]
      FALSE

. r = (s or s')

  1. \emptyword,L_0,L_1 |== (s or s')
     iff there exists L' such that 
         both
            either \emptyword,L_0,L' |== s or \emptyword,L_0,L' |== s' 
         and
            L_1 = L'|_{flow(dom(L_0),(s or s'))}
     =>  [induction]
         either 
            dom(L_0)/s \subseteq dom(L_0) 
         or 
            dom(L_0)/s' \subseteq dom(L_0) 

     =>  [dom(L_0)/(s or s') = (dom(L_0)/s) \cap (dom(L_0)/s')]
         dom(L_0)/(s or s') \subseteq dom(L_0)

  2. \emptyword,L_0,L_1 |== (s or s')
     iff there exists L' such that 
         both
            either 
               \emptyword,L_0,L' |== s 
            or 
               \emptyword,L_0,L' |== s' 
         and
            L_1 = L'|_{dom(L_0)/(s or s'))}
     =>  [induction]
         there exists L' such that 
         both
            either 
               L' = L_0|_{dom(L_0)/s}
            or
               L' = L_0|_{dom(L_0)/s'}
         and
            L_1 = L'|_{dom(L_0)/(s or s')}
     =>  [
            Let s" be either s or s' such that if L' = L_0|_{dom(L_0)/s"}.  Then

               L_1 
            =  L_0|_{dom(L_0)/s"}|_{dom(L_0)/(s or s')}
            =  L_0|_{(dom(L_0)/s") \cap ( dom(L_0)/(s or s') )}
            =  [dom(L_0)/s" \subseteq dom(L_0)/(s or s')]
               L_0|_{ dom(L_0)/(s or s') }
         ]
         L_1 = L_0|_{ dom(L_0)/(s or s') }

. r = (s intersect s')

  1. \emptyword,L_0,L_1 |== (s intersect s')

     =>  there exist L, L' such that 
            \emptyword,L_0,L  |== s 
         and 
            \emptyword,L_0,L' |== s' 

     =>  [induction]
         A: dom(L_0)/s  \subseteq dom(L_0) and dom(L_0)/s' \subseteq dom(L_0)

     =>  [
            dom(L_0)/(s intersect s')
            = ( (dom(L_0)/s) \cup (dom(L_0)/s') ) - block((s intersect s'))
            \subseteq (dom(L_0)/s) \cup (dom(L_0)/s')
            \subseteq [by A]
              dom(L_0)
         ]
         dom(L_0)/(s intersect s') \subseteq dom(L_0)

  2. \emptyword,L_0,L_1 |== (s intersect s')
        
     =>  [Lemma 5.3 of the updated technical report]
         there exist L, L' such that 
            \emptyword,L_0,L  |== s 
         and 
            \emptyword,L_0,L' |== s' 
         and
            L_1 = L|_{ (dom(L_0)/s) - sample(s') } \cup L'|_{ (dom(L_0)/s') - sample(s) }
           
     =>  [induction]
         there exist L, L' such that 
            L  = L_0|_{dom(L_0)/s }
         and 
            L' = L_0|_{dom(L_0)/s'}
         and
            L_1 = L|_{ (dom(L_0)/s) - sample(s') } \cup L'|_{ (dom(L_0)/s') - sample(s) }

     iff L_1 = L_0|_{dom(L_0)/s } |_ { (dom(L_0)/s)  - sample(s') } 
               \cup 
               L_0|_{dom(L_0)/s'} |_ { (dom(L_0)/s') - sample(s)  }
     =>  [
              L_0|_{dom(L_0)/s } |_ { (dom(L_0)/s)  - sample(s') } 
              \cup 
              L_0|_{dom(L_0)/s'} |_ { (dom(L_0)/s') - sample(s)  }

            = L_0|_{ (dom(L_0)/s)  - sample(s') } 
              \cup
              L_0|_{ (dom(L_0)/s') - sample(s)  } 

            = L_0|_{ ((dom(L_0)/s)  - sample(s')) \cup ((dom(L_0)/s') - sample(s)) }

            = [Lemma 5.3 of the technical report]
       
              L_0|_{dom(L_0)/(s intersect s')}
         ]
         L_1 = L_0|_{dom(L_0)/(s intersect s')}

. r = first_match(s)

  1. \emptyword,L_0,L_1 |== first_match(s)
     =>  \emptyword,L_0,L_1 |== s
     =>  [induction]
         dom(L_0)/s \subseteq dom(L_0)
     iff dom(L_0)/first_match(s) \subseteq dom(L_0)

  2. \emptyword,L_0,L_1 |== first_match(s)
     =>  \emptyword,L_0,L_1 |== s
     =>  [induction]
         L_1 = L_0|_{dom(L_0)/s}
     iff L_1 = L_0|_{dom(L_0)/first_match(s)}

. r = s[*0]

  1. dom(L_0)/s[*0]
     = dom(L_0)

  2. \emptyword,L_0,L_1 |== s[*0]
     =>  L_1 = L_0
     iff [
              L_0|_{dom(L_0)/s[*0]}
            = L_0|_{dom(L_0)}
            = L_0
         ]
         L_1 = L_0|_{dom(L_0)/s[*0]}


. r = s[*1:$]

  1. \emptyword,L_0,L_1 |== s[*1:$]

     =>  there exists L such that \emptyword,L_0,L |== s

     =>  [induction]
         dom(L_0)/s \subseteq dom(L_0)

     iff dom(L_0)/s[*1:$] \subseteq dom(L_0)

  2. \emptyword,L_0,L_1 |== s[*1:$]

     iff there exist L_{(0)} = L_0,w_1,L_{(1)},w_2,...,w_j,L_{(j)} = L_1
         (j >= 1) such that \emptyword = w_1 ... w_j and for every i such
         that 1 <= i <= j, w_i,L_{(i-1)},L_{(i)} |== s

     iff there exist L_{(0)} = L_0,L_{(1)},...,L_{(j)} = L_1
         (j >= 1) such that for every i such that 1 <= i <= j, 
         \emptyword,L_{(i-1)},L_{(i)} |== s

     =>  [induction]
         there exist L_{(0)} = L_0,L_{(1)},...,L_{(j)} = L_1
         (j >= 1) such that for every i such that 1 <= i <= j, 
         L_{(i)} = L_{(i-1)}|_{dom(L_{(i-1)})/s}

     =>  [

            CLAIM:  For every i such that 1 <= i <= j, L_{(i)} = L_0|_{dom(L_0)/s}.
       
            PROOF:  By induction.

               L{(1)} 
               = L_{(0)}|_{dom(L_{(0)})/s}
               = L_0|_{dom(L_0)/s}

            For j >= i > 1,
         
               L{(i)} 
               = L_{(i-1)}|_{dom(L_{(i-1)})/s}
               = [induction]
                 L_0|_{dom(L_0)/s} |_ { dom(L_0|_{dom(L_0)/s}) / s }
               = [
                    by induction for part 1, dom(L_0)/s \subseteq dom(L_0),
                    so dom(L_0|_{dom(L_0)/s}) = dom(L_0)/s
                 ]
                 L_0|_{dom(L_0)/s} |_ { dom(L_0) / s / s }
               = [Proposition 4.4 of the technical report]
                 L_0|_{dom(L_0)/s} |_ { dom(L_0)/s       }
               = L_0|_{dom(L_0)/s}

            ////

         ]
         L_1 = L_0|_{dom(L_0)/s}
     iff L_1 = L_0|_{dom(L_0)/s[*1:$]}

////


The next theorem shows that admits_empty(r) = 1 corresponds to the notion
that r is tightly satisfiable by \emptyword.


THEOREM 14:  Let r be a sequence without local variable declaration assignments
and without clocks.  Then for any local variable context L_0, the following are 
equivalent:

1. admits_empty(r) = 1  

2. \emptyword,L_0,L_0|_{flow(dom(L_0),r)} |== r.

PROOF:  By induction.  We use the abbreviation X/s = flow(X,s).

. r = (t v; s)

  \emptyword,L_0,L_0|_{dom(L_0)/(t v; s)} |== (t v; s)
  iff there exists L such that \emptyword,L_0\v,L |== s and
      L_0|_{dom(L_0)/(t v; s)} = L_0[v] \cup (L\v)      
  iff [

         for =>, Theorem 13.2 implies that L = (L_0\v)|_{dom(L_0\v)/s} ;

         for <=, we can let L = (L_0\v)|_{dom(L_0\v)/s} because

           L_0[v] \cup ( (L_0\v)|_{dom(L_0\v)/s} \ v )

         = [ (L\v)|_D = L|_{D - {v}} = L|_D \ v ]

           L_0[v] \cup L_0|_{ (dom(L_0\v)/s) - {v} }

         = [ dom(L\v) = dom(L) - {v} ]

           L_0[v] \cup L_0|_{ ( (dom(L_0) - {v}) / s ) - {v} }
         
         = [ L[v] \cup L|_D = L|_{ (dom(L)\cap{v}) \cup D } ]
         
           L_0|_{ (dom(L_0) \cap {v}) \cup ( ( (dom(L_0) - {v}) / s ) - {v}) }

         = L_0|_{ dom(L_0) / (t v; s) } 

      ]
      \emptyword,L_0\v,(L_0\v)|_{dom(L_0\v)/s} |== s 
  iff [induction]
      admits_empty(s) = 1
  iff admits_empty((t v; s)) = 1
  
. r = (1,v=e)

  \emptyword,L_0,L_0|_{dom(L_0)/(1,v=e)} |== (1,v=e)
  iff [w,L,L' |== (1,v=e) => |w| = 1]
      FALSE
  iff admits_empty((1,v=e)) = 1
      
. r = b

  \emptyword,L_0,L_0|_{dom(L_0)/b} |== b
  iff [w,L,L' |== b => |w| = 1]
      FALSE
  iff admits_empty(b) = 1

. r = (s)

  \emptyword,L_0,L_0|_{dom(L_0)/(s)} |== (s)
  iff \emptyword,L_0,L_0|_{dom(L_0)/s} |== s
  iff [induction]
      admits_empty(s) = 1
  iff admits_empty((s)) = 1

. r = (s ##1 s')

  \emptyword,L_0,L_0|_{dom(L_0)/(s ##1 s')} |== (s ##1 s')

  iff there exist x,y,L' such that \emptyword = xy and x,L_0,L' |== s
      and y,L',L_0|_{dom(L_0)/(s ##1 s')} |== s'

  iff [xy = \emptyword iff x = y = \emptyword]
      there exists L' such that 
         \emptyword,L_0,L' |== s
      and 
         \emptyword,L',L_0|_{dom(L_0)/(s ##1 s')} |== s'

  iff [
         for =>, Theorem 13.2 implies that L' = L_0|_{dom(L_0)/s}
      ]
         \emptyword, L_0,               L_0|_{dom(L_0)/s}          |== s 
      and 
         \emptyword, L_0|_{dom(L_0)/s}, L_0|_{dom(L_0)/(s ##1 s')} |== s'

  iff [
           L_0|_{ dom(L_0|_{dom(L_0)/s})/(s ##1 s') }
         = L_0|_{ dom(L_0)/s/(s ##1 s') }
         = L_0|_{ dom(L_0)/s/s/s' }
         = [X/s/s = X/s]
           L_0|_{ dom(L_0)/s/s' }
         = L_0|_{ dom(L_0)/(s ##1 s') }
      ]   
         \emptyword, L_0,               L_0|_{dom(L_0)/s}                          |== s 
      and 
         \emptyword, L_0|_{dom(L_0)/s}, L_0|_{ dom(L_0|_{dom(L_0)/s})/(s ##1 s') } |== s'

  iff [induction]
      admits_empty(s) = 1 and admits_empty(s') = 1
  iff admits_empty(s) && admits_empty(s') = 1
  iff admits_empty((s ##1 s')) = 1
  
. r = (s ##0 s')

  \emptyword,L_0,L_1 |== (s ##0 s')
  iff [w,L_0,L_1 |== (s ##0 s') => |w| > 0]
      FALSE
  iff admits_empty((s ##0 s')) = 1

. r = (s or s')

  \emptyword,L_0,L_0|_{dom(L_0)/(s or s')} |== (s or s')

  iff there exists L' such that 
      both
         either \emptyword,L_0,L' |== s or \emptyword,L_0,L' |== s' 
      and
         L_0|_{dom(L_0)/(s or s')} = L'|_{dom(L_0)/(s or s')}

  iff either
         there exists L such that \emptyword,L_0,L |== s
         and L_0|_{dom(L_0)/(s or s')} = L|_{dom(L_0)/(s or s')}
      or
         there exists L' such that \emptyword,L_0,L |== s'
         and L_0|_{dom(L_0)/(s or s')} = L'|_{dom(L_0)/(s or s')}

  iff [Theorem 13.2]
      either
         \emptyword,L_0,L_0|_{dom(L_0)/s} |== s
         and L_0|_{dom(L_0)/(s or s')} = L_0|_{dom(L_0)/s}|_{dom(L_0)/(s or s')}
      or
         \emptyword,L_0,L_0|_{dom(L_0)/s'} |== s'
         and L_0|_{dom(L_0)/(s or s')} = L_0|_{dom(L_0)/s'}|_{dom(L_0)/(s or s')}

  iff [

           L_0|_{dom(L_0)/s}|_{dom(L_0)/(s or s') }

         = L_0|_{ (dom(L_0)/s) \cap (dom(L_0)/(s or s')) }

         = L_0|_{ (dom(L_0)/s) \cap (dom(L_0)/s) \cap (dom(L_0)/s') }

         = L_0|_{ (dom(L_0)/s) \cap (dom(L_0)/s') }

         = L_0|_{ dom(L_0)/(s or s') }

         Similarly, 

           L_0|_{dom(L_0)/s'}|_{dom(L_0)/(s or s') }

         = L_0|_{ dom(L_0)/(s or s') }

      ]
      either
         \emptyword,L_0,L_0|_{dom(L_0)/s} |== s
      or
         \emptyword,L_0,L_0|_{dom(L_0)/s'} |== s'

  iff [induction]
      either
         admits_empty(s) = 1
      or
         admits_empty(s') = 1

  iff admits_empty(s) || admits_empty(s') = 1

  iff admits_empty((s or s')) = 1

. r = (s intersect s')

  \emptyword,L_0,L_0|_{dom(L_0)/(s intersect s')} |== (s intersect s')

  iff [Lemma 5.3 in the technical report]
      there exist L, L' such that 
         \emptyword,L_0,L |== s
      and 
         \emptyword,L_0,L' |== s'
      and
         L_0|_{dom(L_0)/(s intersect s')} 
         = L|_{(dom(L_0)/s) - sample(s')} \cup L'|_{(dom(L_0)/s') - sample(s)}

  iff [Theorem 13.2]
         \emptyword,L_0,L_0|_{dom(L_0)/s} |== s
      and 
         \emptyword,L_0,L_0|_{dom(L_0)/s'} |== s'
      and
         L_0|_{dom(L_0)/(s intersect s')} 
         = L_0|_{dom(L_0)/s}|_{(dom(L_0)/s) - sample(s')} 
           \cup 
           L_0|_{dom(L_0)/s'}|_{(dom(L_0)/s') - sample(s)}

  iff [
           L_0|_{dom(L_0)/s} |_{(dom(L_0)/s)  - sample(s')} 
           \cup 
           L_0|_{dom(L_0)/s'}|_{(dom(L_0)/s') - sample(s) }

         = L_0|_{ (dom(L_0)/s)  \cap ( (dom(L_0)/s) - sample(s') ) }
           \cup 
           L_0|_{ (dom(L_0)/s') \cap ( (dom(L_0)/s') - sample(s) ) }

         = L_0|_{ (dom(L_0)/s) - sample(s') }
           \cup 
           L_0|_{ (dom(L_0)/s') - sample(s) }

         = L_0|_{ ((dom(L_0)/s) - sample(s')) \cup ((dom(L_0)/s') - sample(s)) }

         = [Lemma 5.3 in the technical report]
           L_0|_{dom(L_0)/(s intersect s')}  
      ]
         \emptyword,L_0,L_0|_{dom(L_0)/s} |== s
      and 
         \emptyword,L_0,L_0|_{dom(L_0)/s'} |== s'

  iff [induction]
      admits_empty(s) == 1 and admits_empty(s') = 1
 
  iff admits_empty(s) && admits_empty(s') = 1
 
  iff admits_empty((s intersect s')) = 1

. r = first_match(s)

  \emptyword,L_0,L_0|_{dom(L_0)/first_match(s) |== first_match(s)

  iff both
         \emptyword,L_0,L_0|_{dom(L_0)/first_match(s)} |== s
      and
         if there exist x,y,L such that \emptyword = xy and x,L_0,L |== s,
         then y is empty

  iff [\emptyword = xy implies x = y = \emptyword]
      \emptyword,L_0,L_0|_{dom(L_0)/first_match(s)} |== s

  iff \emptyword,L_0,L_0|_{dom(L_0)/s} |== s

  iff [induction]
      admits_empty(s) = 1
  
  iff admits_empty(first_match(s)) = 1

. r = s[*0]

  \emptyword,L_0,L_0|_{dom(L_0)/s[*0]} |== s[*0]
  
  iff [dom(L_0)/s[*0] = dom(L_0)]
      \emptyword,L_0,L_0 |== s[*0]

  iff TRUE

  iff admits_empty(s[*0]) = 1

. r = s[*1:$]

  \emptyword,L_0,L_0|_{dom(L_0)/s[*1:$]} |== s[*1:$]

  iff [dom(L_0)/s[*1:$] = dom(L_0)/s]
      \emptyword,L_0,L_0|_{dom(L_0)/s} |== s[*1:$]

  iff there exist L_{(0)} = L_0,w_1,L_{(1)},w_2,...,w_j,L_{(j)} = L_0|_{dom(L_0)/s}
      (j >= 1) such that \emptyword = w_1 ... w_j and for every i such that 
      1 <= i <= j, w_i,L_{(i-1)},L_{(i)} |== s

  iff [\emptyword = w_1 ... w_j iff \emptyword = w_1 = ... = w_j]
      there exist L_{(0)} = L_0,L_{(1)},...,L_{(j)} = L_0|_{dom(L_0)/s}
      (j >= 1) such that for every i such that 1 <= i <= j, 
      \emptyword,L_{(i-1)},L_{(i)} |== s

  iff [
         For <=, let j = 1.  For =>, use the following claim.

         CLAIM:  For every i such that 1 <= i <= j, L_{(i)} = L_0|_{dom(L_0)/s}.
       
         PROOF:  By induction.

            L{(1)} 
            = [Theorem 13.2]
              L_{(0)}|_{dom(L_{(0)})/s}
            = L_0|_{dom(L_0)/s}

         For j >= i > 1,
         
            L{(i)} 
            = [Theorem 13.2]
              L_{(i-1)}|_{dom(L_{(i-1)})/s}
            = [induction]
              L_0|_{dom(L_0)/s} |_ { dom(L_0|_{dom(L_0)/s}) / s }
            = [
                 by Theorem 13.1, dom(L_0)/s \subseteq dom(L_0),
                 so dom(L_0|_{dom(L_0)/s}) = dom(L_0)/s
              ]
              L_0|_{dom(L_0)/s} |_ { dom(L_0) / s / s }
            = [Proposition 4.4 of the technical report]
              L_0|_{dom(L_0)/s} |_ { dom(L_0)/s       }
            = L_0|_{dom(L_0)/s}

         ////

      ]
      \emptyword,L_0,L_0|_{dom(L_0)/s} |== s

  iff [induction]
      admits_empty(s) = 1

  iff admits_empty(s[*1:$]) = 1

////