diff --git a/resources/type-system/flow-analysis.md b/resources/type-system/flow-analysis.md
index f4f5dee3c6..2c625bc222 100644
--- a/resources/type-system/flow-analysis.md
+++ b/resources/type-system/flow-analysis.md
@@ -108,8 +108,8 @@ that assignment).
 - Lists
   - We use the notation `[a, b]` to denote a list containing elements `a` and
     `b`.
-  - We use the notation `a::l` where `l` is a list to denote a list beginning
-    with `a` and followed by all of the elements of `l`.
+  - We use the notation `[...l, a]` where `l` is a list to denote a list
+    beginning with all the elements of `l` and followed by `a`.
 
 - Stacks
   - We use the notation `push(s, x)` to mean pushing `x` onto the top of the
@@ -118,8 +118,8 @@ that assignment).
     the top element of `s`.  If `s` is empty, the result is undefined.
   - We use the notation `top(s)` to mean the top element of the stack `s`.  If
     `s` is empty, the result is undefined.
-  - Informally, we also use `a::t` to describe a stack `s` such that `top(s)` is
-    `a` and `pop(s)` is `t`.
+  - Informally, we also use `[...t, a]` to describe a stack `s` such that
+    `top(s)` is `a` and `pop(s)` is `t`.
 
 ### Models
 
@@ -131,10 +131,10 @@ source code.
 - `declaredType` is the type assigned to the variable at its declaration site
   (either explicitly or by type inference).
 
-- `promotedTypes` is an ordered set of types that the variable has been promoted
-  to, with the final entry in the ordered set being the current promoted type of
-  the variable.  Note that each entry in the ordered set must be a subtype of
-  all previous entries, and of the declared type.
+- `promotedTypes` is a list of types that the variable has been promoted to,
+  with the final type in the list being the current promoted type of the
+  variable. Note that each type in the list must be a subtype of all previous
+  types, and of the declared type.
 
 - `tested` is a set of types which are considered "of interest" for the purposes
   of promotion, generally because the variable in question has been tested
@@ -238,9 +238,14 @@ We also make use of the following auxiliary functions:
   - `VM3 = VariableModel(d3, p3, s3, a3, u3, c3)` where
    - `d3 = d1 = d2`
      - Note that all models must agree on the declared type of a variable
-   - `p3 = p1 ^ p2`
-     - `p1` and `p2` are totally ordered subsets of a global partial order.
-  Their intersection is a subset of each, and as such is also totally ordered.
+   - `p3` is a list formed by taking all the types that are in both `p1` and
+     `p2`, and ordering them such that each type in the list is a subtype of all
+     previous types.
+     - _Note: it is not specified how to order elements of this list that are
+       mutual subtypes of each other. This will soon be addressed by changing
+       the behavior of flow analysis so that each type in the list is a proper
+       subtype of the previous. (See
+       https://github.com/dart-lang/language/issues/4368.)
    - `s3 = s1 U s2`
      - The set of test sites is the union of the test sites on either path
    - `a3 = a1 && a2`
@@ -258,14 +263,14 @@ We also make use of the following auxiliary functions:
   where `r2` is `r` with `true` pushed as the top element of the stack.
 
 - `drop(M)`, where `M = FlowModel(r, VM)` is defined as `FlowModel(r1, VM)`
-  where `r` is of the form `n0::r1`.  This is the flow model which drops
+  where `r` is of the form `[...r1, n0]`.  This is the flow model which drops
   the reachability information encoded in the top entry in the stack.
 
 - `unsplit(M)`, where `M = FlowModel(r, VM)` is defined as `M1 = FlowModel(r1,
-  VM)` where `r` is of the form `n0::n1::s` and `r1 = (n0&&n1)::s`. The model
-  `M1` is a flow model which collapses the top two elements of the reachability
-  model from `M` into a single boolean which conservatively summarizes the
-  reachability information present in `M`.
+  VM)` where `r` is of the form `[...s, n1, n0]` and `r1 = [...s, n0&&n1]`. The
+  model `M1` is a flow model which collapses the top two elements of the
+  reachability model from `M` into a single boolean which conservatively
+  summarizes the reachability information present in `M`.
 
 - `merge(M1, M2)`, where `M1` and `M2` are flow models is the inverse of `split`
   and represents the result of joining two flow models at the merge of two
@@ -393,7 +398,7 @@ Promotion policy is defined by the following operations on flow models.
 
 We say that the **current type** of a variable `x` in variable model `VM` is `S` where:
   - `VM = VariableModel(declared, promoted, tested, assigned, unassigned, captured)`
-  - `promoted = S::l` or (`promoted = []` and `declared = S`)
+  - `promoted = [...l, S]` or (`promoted = []` and `declared = S`)
 
 Policy:
   - We say that at type `T` is a type of interest for a variable `x` in a set of
@@ -421,8 +426,8 @@ Policy:
     type `T` given variable model `VM` if
     - `VM = VariableModel(declared, promoted, tested, assigned, unassigned, captured)`
     - and `captured` is false
-    - and declared::promoted contains a type `S` such that `T` is `S` or `T` is
-      **NonNull(`S`)**.
+    - and [...promoted, declared] contains a type `S` such that `T` is `S` or
+      `T` is **NonNull(`S`)**.
 
 Definitions:
 
@@ -433,13 +438,14 @@ Definitions:
     - if `captured` is true then:
       - `VM = VariableModel(declared, promoted, tested, true, false, captured)`.
     - otherwise if `x` is promotable via assignment of `E` given `VM`
-      - `VM = VariableModel(declared, T::promoted, tested, true, false, captured)`.
+      - `VM = VariableModel(declared, [...promoted, T], tested, true, false,
+        captured)`.
     - otherwise if `x` is demotable via assignment of `E` given `VM`
       - `VM = VariableModel(declared, demoted, tested, true, false, captured)`.
-      - where `previous` is the suffix of `promoted` starting with the first type
+      - where `previous` is the prefix of `promoted` ending with the first type
         `S` such that `T <: S`, and:
-        - if `S`is nullable and if `T <: Q` where `Q` is **NonNull(`S`)** then
-          `demoted` is `Q::previous`
+        - if `S` is nullable and if `T <: Q` where `Q` is **NonNull(`S`)** then
+          `demoted` is `[...previous, Q]`
         - otherwise `demoted` is `previous`
 
 - `stripParens(E1)`, where `E1` is an expression, is the result of stripping
@@ -467,8 +473,8 @@ Definitions:
       - Else if `S` is `X extends R` then let `T1` = `X & T`
       - Else If `S` is `X & R` then let `T1` = `X & T`
       - Else `x` is not promotable (shouldn't happen since we checked above)
-      - Let `VM2 = VariableModel(declared, T1::promoted, T::tested, assigned,
-      unassigned, captured)`
+      - Let `VM2 = VariableModel(declared, [...promoted, T1], [...tested, T],
+        assigned, unassigned, captured)`
       - Let `M2 = FlowModel(r, VI[x -> VM2])`
       - If `T1 <: Never` then `M3` = `unreachable(M2)`, otherwise `M3` = `M2`
 - `promoteToNonNull(E, M)` where `E` is an expression and `M` is a flow model is