Lemma Triple_left_rotate: forall t p,
    SPEC (left_rotate p)
    PRE (p ~> MTree t)
    POST (fun (r: loc) => r ~> MTree (leftRotate t)).
A: Type
EA: Enc A
forall t p,
SPEC (Trm_apps left_rotate ((Dyn p) :: nil))
⟬*PRE@⟬PointsTo┆p┆⟦$MTree ┆ t⟧⟭*⟭
⟬*POST@fun r : loc => ⟬PointsTo┆r┆⟦$MTree ┆ leftRotate t⟧⟭*⟭
  Proof.
A: Type
EA: Enc A
forall t p,
SPEC (Trm_apps left_rotate ((Dyn p) :: nil))
⟬*PRE@⟬PointsTo┆p┆⟦$MTree ┆ t⟧⟭*⟭
⟬*POST@fun r : loc => ⟬PointsTo┆r┆⟦$MTree ┆ leftRotate t⟧⟭*⟭
    xwp.
A: Type
EA: Enc A
t: tree A
p: loc
⟬*PRE@⟬PointsTo┆p┆⟦$MTree ┆ t⟧⟭*⟭
CODE (`Let b0 := `Let {A1 EA1} V1 := `App is_empty (dyn_to_val (Dyn p)) in
                  `App val_neg (``V1) in
       `If_ b0 Then 
          `Let {A0 _} _ := `App (val_get_field ltree) (dyn_to_val (Dyn p)) in
           `Let {A1 EA0} X := `App (val_get_field rtree) (dyn_to_val (Dyn p)) in
            `Let b1 := `Let {A2 EA1} V1 := `App is_empty (``X) in
                        `App val_neg (``V1) in
             `If_ b1 Then 
                `Let {A2 EA1} X0 := `App (val_get_field ltree) (``X) in
                 `Let {A3 _} _ := `App (val_get_field rtree) (``X) in
                  `(`App (val_set_field rtree) (dyn_to_val (Dyn p)) (``X0)) ;
                   `(`App (val_set_field ltree) (``X) (dyn_to_val (Dyn p))) ;
                    `$(``X)
              Else
                `$(dyn_to_val (Dyn p))
        Else
          `$(dyn_to_val (Dyn p)))
⟬*POST@ fun x : loc =>
        ⟬Star┆⟬PointsTo┆x┆⟦$MTree ┆ leftRotate t⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ mxapp* Triple_is_empty.
A: Type
EA: Enc A
t: tree A
p: loc
⟬*PRE@⟬PointsTo┆p┆⟦$MTree ┆ t⟧⟭*⟭
CODE (`App val_neg (``(isTrue (t = leaf))))
⟬*POST@ Bind X : bool In
        `(If_ X Then 
            `Let {A0 _} _ := `App (val_get_field ltree) (``p) in
             `Let {A1 EA0} X0 := `App (val_get_field rtree) (``p) in
              `Let b0 := `Let {A2 EA1} V1 := `App is_empty (``X0) in
                          `App val_neg (``V1) in
               `If_ b0 Then 
                  `Let {A2 EA1} X1 := `App (val_get_field ltree) (``X0) in
                   `Let {A3 _} _ := `App (val_get_field rtree) (``X0) in
                    `(`App (val_set_field rtree) (``p) (``X1)) ;
                     `(`App (val_set_field ltree) (``X0) (``p)) ;
                      `$(``X0)
                Else
                  `$(``p)
          Else
            `$(``p))
        ;
        fun x : loc =>
        ⟬Star┆⟬PointsTo┆x┆⟦$MTree ┆ leftRotate t⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ mxapp Triple_neg.
A: Type
EA: Enc A
t: tree A
p: loc
⟬*PRE@⟬PointsTo┆p┆⟦$MTree ┆ t⟧⟭*⟭
CODE (`If_ ! isTrue (t = leaf) Then 
         `Let {A0 _} _ := `App (val_get_field ltree) (``p) in
          `Let {A1 EA0} X := `App (val_get_field rtree) (``p) in
           `Let b0 := `Let {A2 EA1} V1 := `App is_empty (``X) in
                       `App val_neg (``V1) in
            `If_ b0 Then 
               `Let {A2 EA1} X0 := `App (val_get_field ltree) (``X) in
                `Let {A3 _} _ := `App (val_get_field rtree) (``X) in
                 `(`App (val_set_field rtree) (``p) (``X0)) ;
                  `(`App (val_set_field ltree) (``X) (``p)) ;
                   `$(``X)
             Else
               `$(``p)
       Else
         `$(``p))
⟬*POST@ fun x : loc =>
        ⟬Star┆⟬PointsTo┆x┆⟦$MTree ┆ leftRotate t⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
    destruct t as [| x tl tr];
      xif; try easy; intros _.
A: Type
EA: Enc A
p: loc
⟬*PRE@⟬PointsTo┆p┆⟦$MTree ┆ leaf⟧⟭*⟭
CODE (`$(``p))
⟬*POST@ fun x : loc =>
        ⟬Star┆⟬PointsTo┆x┆⟦$MTree ┆ leftRotate leaf⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
A: Type
EA: Enc A
x: A
tl, tr: tree A
p: loc
⟬*PRE@⟬PointsTo┆p┆⟦$MTree ┆ node x tl tr⟧⟭*⟭
CODE (`Let {A0 _} _ := `App (val_get_field ltree) (``p) in
       `Let {A1 EA0} X := `App (val_get_field rtree) (``p) in
        `Let b0 := `Let {A2 EA1} V1 := `App is_empty (``X) in
                    `App val_neg (``V1) in
         `If_ b0 Then 
            `Let {A2 EA1} X0 := `App (val_get_field ltree) (``X) in
             `Let {A3 _} _ := `App (val_get_field rtree) (``X) in
              `(`App (val_set_field rtree) (``p) (``X0)) ;
               `(`App (val_set_field ltree) (``X) (``p)) ;
                `$(``X)
          Else
            `$(``p))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ leftRotate (node x tl tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
    - (* t = leaf *)
A: Type
EA: Enc A
p: loc
⟬*PRE@⟬PointsTo┆p┆⟦$MTree ┆ leaf⟧⟭*⟭
CODE (`$(``p))
⟬*POST@ fun x : loc =>
        ⟬Star┆⟬PointsTo┆x┆⟦$MTree ┆ leftRotate leaf⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ mxvals*.
    - (* t = node *)
A: Type
EA: Enc A
x: A
tl, tr: tree A
p: loc
⟬*PRE@⟬PointsTo┆p┆⟦$MTree ┆ node x tl tr⟧⟭*⟭
CODE (`Let {A0 _} _ := `App (val_get_field ltree) (``p) in
       `Let {A1 EA0} X := `App (val_get_field rtree) (``p) in
        `Let b0 := `Let {A2 EA1} V1 := `App is_empty (``X) in
                    `App val_neg (``V1) in
         `If_ b0 Then 
            `Let {A2 EA1} X0 := `App (val_get_field ltree) (``X) in
             `Let {A3 _} _ := `App (val_get_field rtree) (``X) in
              `(`App (val_set_field rtree) (``p) (``X0)) ;
               `(`App (val_set_field ltree) (``X) (``p)) ;
                `$(``X)
          Else
            `$(``p))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ leftRotate (node x tl tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ xchange MTree_node; intros pl pr.
A: Type
EA: Enc A
x: A
tl, tr: tree A
p, pl, pr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p┆⟦$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬Star┆⟬PointsTo┆pl┆⟦
$MTree ┆ tl⟧⟭┆⟬PointsTo┆pr┆⟦$MTree ┆ tr⟧⟭⟭⟭*⟭
CODE (`Let {A0 _} _ := `App (val_get_field ltree) (``p) in
       `Let {A1 EA0} X := `App (val_get_field rtree) (``p) in
        `Let b0 := `Let {A2 EA1} V1 := `App is_empty (``X) in
                    `App val_neg (``V1) in
         `If_ b0 Then 
            `Let {A2 EA1} X0 := `App (val_get_field ltree) (``X) in
             `Let {A3 _} _ := `App (val_get_field rtree) (``X) in
              `(`App (val_set_field rtree) (``p) (``X0)) ;
               `(`App (val_set_field ltree) (``X) (``p)) ;
                `$(``X)
          Else
            `$(``p))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ leftRotate (node x tl tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
      mxapp NodeSpecs.Triple_get_field_ltree.
A: Type
EA: Enc A
x: A
tl, tr: tree A
p, pl, pr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p┆⟦$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬Star┆⟬PointsTo┆pl┆⟦
$MTree ┆ tl⟧⟭┆⟬PointsTo┆pr┆⟦$MTree ┆ tr⟧⟭⟭⟭*⟭
CODE (`Let {A0 EA0} X := `App (val_get_field rtree) (``p) in
       `Let b0 := `Let {A1 EA1} V1 := `App is_empty (``X) in
                   `App val_neg (``V1) in
        `If_ b0 Then 
           `Let {A1 EA1} X0 := `App (val_get_field ltree) (``X) in
            `Let {A2 _} _ := `App (val_get_field rtree) (``X) in
             `(`App (val_set_field rtree) (``p) (``X0)) ;
              `(`App (val_set_field ltree) (``X) (``p)) ;
               `$(``X)
         Else
           `$(``p))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ leftRotate (node x tl tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
      mxapp NodeSpecs.Triple_get_field_rtree.
A: Type
EA: Enc A
x: A
tl, tr: tree A
p, pl, pr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p┆⟦$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬Star┆⟬PointsTo┆pl┆⟦
$MTree ┆ tl⟧⟭┆⟬PointsTo┆pr┆⟦$MTree ┆ tr⟧⟭⟭⟭*⟭
CODE (`Let b0 := `Let {A1 EA1} V1 := `App is_empty (``pr) in
                  `App val_neg (``V1) in
       `If_ b0 Then 
          `Let {A0 EA0} X := `App (val_get_field ltree) (``pr) in
           `Let {A1 _} _ := `App (val_get_field rtree) (``pr) in
            `(`App (val_set_field rtree) (``p) (``X)) ;
             `(`App (val_set_field ltree) (``pr) (``p)) ;
              `$(``pr)
        Else
          `$(``p))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ leftRotate (node x tl tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
      mxapp Triple_is_empty.
A: Type
EA: Enc A
x: A
tl, tr: tree A
p, pl, pr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆pr┆⟦$MTree ┆ tr⟧⟭┆⟬Star┆⟬PointsTo┆p┆⟦
$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬PointsTo┆pl┆⟦$MTree ┆ tl⟧⟭⟭⟭*⟭
CODE (`App val_neg (``(isTrue (tr = leaf))))
⟬*POST@ Bind X : bool In
        `(If_ X Then 
            `Let {A0 EA0} X0 := `App (val_get_field ltree) (``pr) in
             `Let {A1 _} _ := `App (val_get_field rtree) (``pr) in
              `(`App (val_set_field rtree) (``p) (``X0)) ;
               `(`App (val_set_field ltree) (``pr) (``p)) ;
                `$(``pr)
          Else
            `$(``p))
        ;
        fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ leftRotate (node x tl tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ mxapp Triple_neg.
A: Type
EA: Enc A
x: A
tl, tr: tree A
p, pl, pr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆pr┆⟦$MTree ┆ tr⟧⟭┆⟬Star┆⟬PointsTo┆p┆⟦
$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬PointsTo┆pl┆⟦$MTree ┆ tl⟧⟭⟭⟭*⟭
CODE (`If_ ! isTrue (tr = leaf) Then 
         `Let {A0 EA0} X := `App (val_get_field ltree) (``pr) in
          `Let {A1 _} _ := `App (val_get_field rtree) (``pr) in
           `(`App (val_set_field rtree) (``p) (``X)) ;
            `(`App (val_set_field ltree) (``pr) (``p)) ;
             `$(``pr)
       Else
         `$(``p))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ leftRotate (node x tl tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
      destruct tr as [| xr trl trr];
        xif; try easy; intros _.
A: Type
EA: Enc A
x: A
tl: tree A
p, pl, pr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆pr┆⟦$MTree ┆ leaf⟧⟭┆⟬Star┆⟬PointsTo┆p┆⟦
$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬PointsTo┆pl┆⟦$MTree ┆ tl⟧⟭⟭⟭*⟭
CODE (`$(``p))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ leftRotate (node x tl leaf)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
A: Type
EA: Enc A
x: A
tl: tree A
xr: A
trl, trr: tree A
p, pl, pr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆pr┆⟦$MTree ┆ node xr trl trr⟧⟭┆⟬Star┆⟬PointsTo┆p┆⟦
$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬PointsTo┆pl┆⟦$MTree ┆ tl⟧⟭⟭⟭*⟭
CODE (`Let {A0 EA0} X := `App (val_get_field ltree) (``pr) in
       `Let {A1 _} _ := `App (val_get_field rtree) (``pr) in
        `(`App (val_set_field rtree) (``p) (``X)) ;
         `(`App (val_set_field ltree) (``pr) (``p)) ;
          `$(``pr))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ leftRotate (node x tl (node xr trl trr))⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
      + (* tr = leaf *)
A: Type
EA: Enc A
x: A
tl: tree A
p, pl, pr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆pr┆⟦$MTree ┆ leaf⟧⟭┆⟬Star┆⟬PointsTo┆p┆⟦
$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬PointsTo┆pl┆⟦$MTree ┆ tl⟧⟭⟭⟭*⟭
CODE (`$(``p))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ leftRotate (node x tl leaf)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ xchange <- MTree_node.
A: Type
EA: Enc A
x: A
tl: tree A
p, pl, pr: loc
⟬*PRE@⟬PointsTo┆p┆⟦$MTree ┆ node x tl leaf⟧⟭*⟭
CODE (`$(``p))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ leftRotate (node x tl leaf)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ mxvals*.
      + (* tr = node *)
A: Type
EA: Enc A
x: A
tl: tree A
xr: A
trl, trr: tree A
p, pl, pr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆pr┆⟦$MTree ┆ node xr trl trr⟧⟭┆⟬Star┆⟬PointsTo┆p┆⟦
$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬PointsTo┆pl┆⟦$MTree ┆ tl⟧⟭⟭⟭*⟭
CODE (`Let {A0 EA0} X := `App (val_get_field ltree) (``pr) in
       `Let {A1 _} _ := `App (val_get_field rtree) (``pr) in
        `(`App (val_set_field rtree) (``p) (``X)) ;
         `(`App (val_set_field ltree) (``pr) (``p)) ;
          `$(``pr))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ leftRotate (node x tl (node xr trl trr))⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ xchange MTree_node; intros prl prr.
A: Type
EA: Enc A
x: A
tl: tree A
xr: A
trl, trr: tree A
p, pl, pr, prl, prr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆pr┆⟦$MNode ┆ xr ┆ prl ┆ prr⟧⟭┆⟬Star┆⟬PointsTo┆prl┆⟦
$MTree ┆ trl⟧⟭┆⟬Star┆⟬PointsTo┆prr┆⟦$MTree ┆ trr⟧⟭┆⟬Star┆⟬PointsTo┆p┆⟦
$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬PointsTo┆pl┆⟦$MTree ┆ tl⟧⟭⟭⟭⟭⟭*⟭
CODE (`Let {A0 EA0} X := `App (val_get_field ltree) (``pr) in
       `Let {A1 _} _ := `App (val_get_field rtree) (``pr) in
        `(`App (val_set_field rtree) (``p) (``X)) ;
         `(`App (val_set_field ltree) (``pr) (``p)) ;
          `$(``pr))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ leftRotate (node x tl (node xr trl trr))⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
        mxapp NodeSpecs.Triple_get_field_ltree.
A: Type
EA: Enc A
x: A
tl: tree A
xr: A
trl, trr: tree A
p, pl, pr, prl, prr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆pr┆⟦$MNode ┆ xr ┆ prl ┆ prr⟧⟭┆⟬Star┆⟬PointsTo┆prl┆⟦
$MTree ┆ trl⟧⟭┆⟬Star┆⟬PointsTo┆prr┆⟦$MTree ┆ trr⟧⟭┆⟬Star┆⟬PointsTo┆p┆⟦
$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬PointsTo┆pl┆⟦$MTree ┆ tl⟧⟭⟭⟭⟭⟭*⟭
CODE (`Let {A0 _} _ := `App (val_get_field rtree) (``pr) in
       `(`App (val_set_field rtree) (``p) (``prl)) ;
        `(`App (val_set_field ltree) (``pr) (``p)) ;
         `$(``pr))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ leftRotate (node x tl (node xr trl trr))⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
        mxapp NodeSpecs.Triple_get_field_rtree.
A: Type
EA: Enc A
x: A
tl: tree A
xr: A
trl, trr: tree A
p, pl, pr, prl, prr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆pr┆⟦$MNode ┆ xr ┆ prl ┆ prr⟧⟭┆⟬Star┆⟬PointsTo┆prl┆⟦
$MTree ┆ trl⟧⟭┆⟬Star┆⟬PointsTo┆prr┆⟦$MTree ┆ trr⟧⟭┆⟬Star┆⟬PointsTo┆p┆⟦
$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬PointsTo┆pl┆⟦$MTree ┆ tl⟧⟭⟭⟭⟭⟭*⟭
CODE (`(`App (val_set_field rtree) (``p) (``prl)) ;
       `(`App (val_set_field ltree) (``pr) (``p)) ;
        `$(``pr))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ leftRotate (node x tl (node xr trl trr))⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
        mxapp NodeSpecs.Triple_set_field_rtree.
A: Type
EA: Enc A
x: A
tl: tree A
xr: A
trl, trr: tree A
p, pl, pr, prl, prr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p┆⟦$MNode ┆ x ┆ pl ┆ prl⟧⟭┆⟬Star┆⟬PointsTo┆pr┆⟦
$MNode ┆ xr ┆ prl ┆ prr⟧⟭┆⟬Star┆⟬PointsTo┆prl┆⟦$MTree ┆ trl⟧⟭┆⟬Star┆⟬PointsTo┆prr┆⟦
$MTree ┆ trr⟧⟭┆⟬PointsTo┆pl┆⟦$MTree ┆ tl⟧⟭⟭⟭⟭⟭*⟭
CODE (`(`App (val_set_field ltree) (``pr) (``p)) ;
       `$(``pr))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ leftRotate (node x tl (node xr trl trr))⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
        mxapp NodeSpecs.Triple_set_field_ltree.
A: Type
EA: Enc A
x: A
tl: tree A
xr: A
trl, trr: tree A
p, pl, pr, prl, prr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆pr┆⟦$MNode ┆ xr ┆ p ┆ prr⟧⟭┆⟬Star┆⟬PointsTo┆p┆⟦
$MNode ┆ x ┆ pl ┆ prl⟧⟭┆⟬Star┆⟬PointsTo┆prl┆⟦$MTree ┆ trl⟧⟭┆⟬Star┆⟬PointsTo┆prr┆⟦
$MTree ┆ trr⟧⟭┆⟬PointsTo┆pl┆⟦$MTree ┆ tl⟧⟭⟭⟭⟭⟭*⟭
CODE (`$(``pr))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ leftRotate (node x tl (node xr trl trr))⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
        xchange <- MTree_node.
A: Type
EA: Enc A
x: A
tl: tree A
xr: A
trl, trr: tree A
p, pl, pr, prl, prr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p┆⟦$MTree ┆ node x tl trl⟧⟭┆⟬Star┆⟬PointsTo┆pr┆⟦
$MNode ┆ xr ┆ p ┆ prr⟧⟭┆⟬PointsTo┆prr┆⟦$MTree ┆ trr⟧⟭⟭⟭*⟭
CODE (`$(``pr))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ leftRotate (node x tl (node xr trl trr))⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ xchange <- MTree_node.
A: Type
EA: Enc A
x: A
tl: tree A
xr: A
trl, trr: tree A
p, pl, pr, prl, prr: loc
⟬*PRE@⟬PointsTo┆pr┆⟦$MTree ┆ node xr (node x tl trl) trr⟧⟭*⟭
CODE (`$(``pr))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ leftRotate (node x tl (node xr trl trr))⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
        mxvals.
  Qed.

  Lemma Triple_right_rotate: forall t p,
    SPEC (right_rotate p)
    PRE (p ~> MTree t)
    POST (fun (r: loc) => r ~> MTree (rightRotate t)).
A: Type
EA: Enc A
forall t p,
SPEC (Trm_apps right_rotate ((Dyn p) :: nil))
⟬*PRE@⟬PointsTo┆p┆⟦$MTree ┆ t⟧⟭*⟭
⟬*POST@fun r : loc => ⟬PointsTo┆r┆⟦$MTree ┆ rightRotate t⟧⟭*⟭
  Proof.
A: Type
EA: Enc A
forall t p,
SPEC (Trm_apps right_rotate ((Dyn p) :: nil))
⟬*PRE@⟬PointsTo┆p┆⟦$MTree ┆ t⟧⟭*⟭
⟬*POST@fun r : loc => ⟬PointsTo┆r┆⟦$MTree ┆ rightRotate t⟧⟭*⟭
    xwp.
A: Type
EA: Enc A
t: tree A
p: loc
⟬*PRE@⟬PointsTo┆p┆⟦$MTree ┆ t⟧⟭*⟭
CODE (`Let b0 := `Let {A1 EA1} V1 := `App is_empty (dyn_to_val (Dyn p)) in
                  `App val_neg (``V1) in
       `If_ b0 Then 
          `Let {A0 EA0} X := `App (val_get_field ltree) (dyn_to_val (Dyn p)) in
           `Let {A1 _} _ := `App (val_get_field rtree) (dyn_to_val (Dyn p)) in
            `Let b1 := `Let {A2 EA1} V1 := `App is_empty (``X) in
                        `App val_neg (``V1) in
             `If_ b1 Then 
                `Let {A2 _} _ := `App (val_get_field ltree) (``X) in
                 `Let {A3 EA1} X0 := `App (val_get_field rtree) (``X) in
                  `(`App (val_set_field rtree) (``X) (dyn_to_val (Dyn p))) ;
                   `(`App (val_set_field ltree) (dyn_to_val (Dyn p)) (``X0)) ;
                    `$(``X)
              Else
                `$(dyn_to_val (Dyn p))
        Else
          `$(dyn_to_val (Dyn p)))
⟬*POST@ fun x : loc =>
        ⟬Star┆⟬PointsTo┆x┆⟦$MTree ┆ rightRotate t⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ mxapp* Triple_is_empty.
A: Type
EA: Enc A
t: tree A
p: loc
⟬*PRE@⟬PointsTo┆p┆⟦$MTree ┆ t⟧⟭*⟭
CODE (`App val_neg (``(isTrue (t = leaf))))
⟬*POST@ Bind X : bool In
        `(If_ X Then 
            `Let {A0 EA0} X0 := `App (val_get_field ltree) (``p) in
             `Let {A1 _} _ := `App (val_get_field rtree) (``p) in
              `Let b0 := `Let {A2 EA1} V1 := `App is_empty (``X0) in
                          `App val_neg (``V1) in
               `If_ b0 Then 
                  `Let {A2 _} _ := `App (val_get_field ltree) (``X0) in
                   `Let {A3 EA1} X1 := `App (val_get_field rtree) (``X0) in
                    `(`App (val_set_field rtree) (``X0) (``p)) ;
                     `(`App (val_set_field ltree) (``p) (``X1)) ;
                      `$(``X0)
                Else
                  `$(``p)
          Else
            `$(``p))
        ;
        fun x : loc =>
        ⟬Star┆⟬PointsTo┆x┆⟦$MTree ┆ rightRotate t⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ mxapp Triple_neg.
A: Type
EA: Enc A
t: tree A
p: loc
⟬*PRE@⟬PointsTo┆p┆⟦$MTree ┆ t⟧⟭*⟭
CODE (`If_ ! isTrue (t = leaf) Then 
         `Let {A0 EA0} X := `App (val_get_field ltree) (``p) in
          `Let {A1 _} _ := `App (val_get_field rtree) (``p) in
           `Let b0 := `Let {A2 EA1} V1 := `App is_empty (``X) in
                       `App val_neg (``V1) in
            `If_ b0 Then 
               `Let {A2 _} _ := `App (val_get_field ltree) (``X) in
                `Let {A3 EA1} X0 := `App (val_get_field rtree) (``X) in
                 `(`App (val_set_field rtree) (``X) (``p)) ;
                  `(`App (val_set_field ltree) (``p) (``X0)) ;
                   `$(``X)
             Else
               `$(``p)
       Else
         `$(``p))
⟬*POST@ fun x : loc =>
        ⟬Star┆⟬PointsTo┆x┆⟦$MTree ┆ rightRotate t⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
    destruct t as [| x tl tr];
      xif; try easy; intros _.
A: Type
EA: Enc A
p: loc
⟬*PRE@⟬PointsTo┆p┆⟦$MTree ┆ leaf⟧⟭*⟭
CODE (`$(``p))
⟬*POST@ fun x : loc =>
        ⟬Star┆⟬PointsTo┆x┆⟦$MTree ┆ rightRotate leaf⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
A: Type
EA: Enc A
x: A
tl, tr: tree A
p: loc
⟬*PRE@⟬PointsTo┆p┆⟦$MTree ┆ node x tl tr⟧⟭*⟭
CODE (`Let {A0 EA0} X := `App (val_get_field ltree) (``p) in
       `Let {A1 _} _ := `App (val_get_field rtree) (``p) in
        `Let b0 := `Let {A2 EA1} V1 := `App is_empty (``X) in
                    `App val_neg (``V1) in
         `If_ b0 Then 
            `Let {A2 _} _ := `App (val_get_field ltree) (``X) in
             `Let {A3 EA1} X0 := `App (val_get_field rtree) (``X) in
              `(`App (val_set_field rtree) (``X) (``p)) ;
               `(`App (val_set_field ltree) (``p) (``X0)) ;
                `$(``X)
          Else
            `$(``p))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ rightRotate (node x tl tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
    - (* t = leaf *)
A: Type
EA: Enc A
p: loc
⟬*PRE@⟬PointsTo┆p┆⟦$MTree ┆ leaf⟧⟭*⟭
CODE (`$(``p))
⟬*POST@ fun x : loc =>
        ⟬Star┆⟬PointsTo┆x┆⟦$MTree ┆ rightRotate leaf⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ mxvals*.
    - (* t = node *)
A: Type
EA: Enc A
x: A
tl, tr: tree A
p: loc
⟬*PRE@⟬PointsTo┆p┆⟦$MTree ┆ node x tl tr⟧⟭*⟭
CODE (`Let {A0 EA0} X := `App (val_get_field ltree) (``p) in
       `Let {A1 _} _ := `App (val_get_field rtree) (``p) in
        `Let b0 := `Let {A2 EA1} V1 := `App is_empty (``X) in
                    `App val_neg (``V1) in
         `If_ b0 Then 
            `Let {A2 _} _ := `App (val_get_field ltree) (``X) in
             `Let {A3 EA1} X0 := `App (val_get_field rtree) (``X) in
              `(`App (val_set_field rtree) (``X) (``p)) ;
               `(`App (val_set_field ltree) (``p) (``X0)) ;
                `$(``X)
          Else
            `$(``p))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ rightRotate (node x tl tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ xchange MTree_node; intros pl pr.
A: Type
EA: Enc A
x: A
tl, tr: tree A
p, pl, pr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p┆⟦$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬Star┆⟬PointsTo┆pl┆⟦
$MTree ┆ tl⟧⟭┆⟬PointsTo┆pr┆⟦$MTree ┆ tr⟧⟭⟭⟭*⟭
CODE (`Let {A0 EA0} X := `App (val_get_field ltree) (``p) in
       `Let {A1 _} _ := `App (val_get_field rtree) (``p) in
        `Let b0 := `Let {A2 EA1} V1 := `App is_empty (``X) in
                    `App val_neg (``V1) in
         `If_ b0 Then 
            `Let {A2 _} _ := `App (val_get_field ltree) (``X) in
             `Let {A3 EA1} X0 := `App (val_get_field rtree) (``X) in
              `(`App (val_set_field rtree) (``X) (``p)) ;
               `(`App (val_set_field ltree) (``p) (``X0)) ;
                `$(``X)
          Else
            `$(``p))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ rightRotate (node x tl tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
      mxapp NodeSpecs.Triple_get_field_ltree.
A: Type
EA: Enc A
x: A
tl, tr: tree A
p, pl, pr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p┆⟦$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬Star┆⟬PointsTo┆pl┆⟦
$MTree ┆ tl⟧⟭┆⟬PointsTo┆pr┆⟦$MTree ┆ tr⟧⟭⟭⟭*⟭
CODE (`Let {A0 _} _ := `App (val_get_field rtree) (``p) in
       `Let b0 := `Let {A1 EA1} V1 := `App is_empty (``pl) in
                   `App val_neg (``V1) in
        `If_ b0 Then 
           `Let {A1 _} _ := `App (val_get_field ltree) (``pl) in
            `Let {A2 EA0} X := `App (val_get_field rtree) (``pl) in
             `(`App (val_set_field rtree) (``pl) (``p)) ;
              `(`App (val_set_field ltree) (``p) (``X)) ;
               `$(``pl)
         Else
           `$(``p))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ rightRotate (node x tl tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
      mxapp NodeSpecs.Triple_get_field_rtree.
A: Type
EA: Enc A
x: A
tl, tr: tree A
p, pl, pr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p┆⟦$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬Star┆⟬PointsTo┆pl┆⟦
$MTree ┆ tl⟧⟭┆⟬PointsTo┆pr┆⟦$MTree ┆ tr⟧⟭⟭⟭*⟭
CODE (`Let b0 := `Let {A1 EA1} V1 := `App is_empty (``pl) in
                  `App val_neg (``V1) in
       `If_ b0 Then 
          `Let {A0 _} _ := `App (val_get_field ltree) (``pl) in
           `Let {A1 EA0} X := `App (val_get_field rtree) (``pl) in
            `(`App (val_set_field rtree) (``pl) (``p)) ;
             `(`App (val_set_field ltree) (``p) (``X)) ;
              `$(``pl)
        Else
          `$(``p))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ rightRotate (node x tl tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
      mxapp Triple_is_empty.
A: Type
EA: Enc A
x: A
tl, tr: tree A
p, pl, pr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆pl┆⟦$MTree ┆ tl⟧⟭┆⟬Star┆⟬PointsTo┆p┆⟦
$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬PointsTo┆pr┆⟦$MTree ┆ tr⟧⟭⟭⟭*⟭
CODE (`App val_neg (``(isTrue (tl = leaf))))
⟬*POST@ Bind X : bool In
        `(If_ X Then 
            `Let {A0 _} _ := `App (val_get_field ltree) (``pl) in
             `Let {A1 EA0} X0 := `App (val_get_field rtree) (``pl) in
              `(`App (val_set_field rtree) (``pl) (``p)) ;
               `(`App (val_set_field ltree) (``p) (``X0)) ;
                `$(``pl)
          Else
            `$(``p))
        ;
        fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ rightRotate (node x tl tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ mxapp Triple_neg.
A: Type
EA: Enc A
x: A
tl, tr: tree A
p, pl, pr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆pl┆⟦$MTree ┆ tl⟧⟭┆⟬Star┆⟬PointsTo┆p┆⟦
$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬PointsTo┆pr┆⟦$MTree ┆ tr⟧⟭⟭⟭*⟭
CODE (`If_ ! isTrue (tl = leaf) Then 
         `Let {A0 _} _ := `App (val_get_field ltree) (``pl) in
          `Let {A1 EA0} X := `App (val_get_field rtree) (``pl) in
           `(`App (val_set_field rtree) (``pl) (``p)) ;
            `(`App (val_set_field ltree) (``p) (``X)) ;
             `$(``pl)
       Else
         `$(``p))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ rightRotate (node x tl tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
      destruct tl as [| xl tll tlr];
        xif; try easy; intros _.
A: Type
EA: Enc A
x: A
tr: tree A
p, pl, pr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆pl┆⟦$MTree ┆ leaf⟧⟭┆⟬Star┆⟬PointsTo┆p┆⟦
$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬PointsTo┆pr┆⟦$MTree ┆ tr⟧⟭⟭⟭*⟭
CODE (`$(``p))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ rightRotate (node x leaf tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
A: Type
EA: Enc A
x, xl: A
tll, tlr, tr: tree A
p, pl, pr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆pl┆⟦$MTree ┆ node xl tll tlr⟧⟭┆⟬Star┆⟬PointsTo┆p┆⟦
$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬PointsTo┆pr┆⟦$MTree ┆ tr⟧⟭⟭⟭*⟭
CODE (`Let {A0 _} _ := `App (val_get_field ltree) (``pl) in
       `Let {A1 EA0} X := `App (val_get_field rtree) (``pl) in
        `(`App (val_set_field rtree) (``pl) (``p)) ;
         `(`App (val_set_field ltree) (``p) (``X)) ;
          `$(``pl))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree
                            ┆ rightRotate (node x (node xl tll tlr) tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
      + (* tr = leaf *)
A: Type
EA: Enc A
x: A
tr: tree A
p, pl, pr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆pl┆⟦$MTree ┆ leaf⟧⟭┆⟬Star┆⟬PointsTo┆p┆⟦
$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬PointsTo┆pr┆⟦$MTree ┆ tr⟧⟭⟭⟭*⟭
CODE (`$(``p))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ rightRotate (node x leaf tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ xchange <- MTree_node.
A: Type
EA: Enc A
x: A
tr: tree A
p, pl, pr: loc
⟬*PRE@⟬PointsTo┆p┆⟦$MTree ┆ node x leaf tr⟧⟭*⟭
CODE (`$(``p))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree ┆ rightRotate (node x leaf tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ mxvals*.
      + (* tr = node *)
A: Type
EA: Enc A
x, xl: A
tll, tlr, tr: tree A
p, pl, pr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆pl┆⟦$MTree ┆ node xl tll tlr⟧⟭┆⟬Star┆⟬PointsTo┆p┆⟦
$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬PointsTo┆pr┆⟦$MTree ┆ tr⟧⟭⟭⟭*⟭
CODE (`Let {A0 _} _ := `App (val_get_field ltree) (``pl) in
       `Let {A1 EA0} X := `App (val_get_field rtree) (``pl) in
        `(`App (val_set_field rtree) (``pl) (``p)) ;
         `(`App (val_set_field ltree) (``p) (``X)) ;
          `$(``pl))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree
                            ┆ rightRotate (node x (node xl tll tlr) tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ xchange MTree_node; intros pll plr.
A: Type
EA: Enc A
x, xl: A
tll, tlr, tr: tree A
p, pl, pr, pll, plr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆pl┆⟦$MNode ┆ xl ┆ pll ┆ plr⟧⟭┆⟬Star┆⟬PointsTo┆pll┆⟦
$MTree ┆ tll⟧⟭┆⟬Star┆⟬PointsTo┆plr┆⟦$MTree ┆ tlr⟧⟭┆⟬Star┆⟬PointsTo┆p┆⟦
$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬PointsTo┆pr┆⟦$MTree ┆ tr⟧⟭⟭⟭⟭⟭*⟭
CODE (`Let {A0 _} _ := `App (val_get_field ltree) (``pl) in
       `Let {A1 EA0} X := `App (val_get_field rtree) (``pl) in
        `(`App (val_set_field rtree) (``pl) (``p)) ;
         `(`App (val_set_field ltree) (``p) (``X)) ;
          `$(``pl))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree
                            ┆ rightRotate (node x (node xl tll tlr) tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
        mxapp NodeSpecs.Triple_get_field_ltree.
A: Type
EA: Enc A
x, xl: A
tll, tlr, tr: tree A
p, pl, pr, pll, plr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆pl┆⟦$MNode ┆ xl ┆ pll ┆ plr⟧⟭┆⟬Star┆⟬PointsTo┆pll┆⟦
$MTree ┆ tll⟧⟭┆⟬Star┆⟬PointsTo┆plr┆⟦$MTree ┆ tlr⟧⟭┆⟬Star┆⟬PointsTo┆p┆⟦
$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬PointsTo┆pr┆⟦$MTree ┆ tr⟧⟭⟭⟭⟭⟭*⟭
CODE (`Let {A0 EA0} X := `App (val_get_field rtree) (``pl) in
       `(`App (val_set_field rtree) (``pl) (``p)) ;
        `(`App (val_set_field ltree) (``p) (``X)) ;
         `$(``pl))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree
                            ┆ rightRotate (node x (node xl tll tlr) tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
        mxapp NodeSpecs.Triple_get_field_rtree.
A: Type
EA: Enc A
x, xl: A
tll, tlr, tr: tree A
p, pl, pr, pll, plr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆pl┆⟦$MNode ┆ xl ┆ pll ┆ plr⟧⟭┆⟬Star┆⟬PointsTo┆pll┆⟦
$MTree ┆ tll⟧⟭┆⟬Star┆⟬PointsTo┆plr┆⟦$MTree ┆ tlr⟧⟭┆⟬Star┆⟬PointsTo┆p┆⟦
$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬PointsTo┆pr┆⟦$MTree ┆ tr⟧⟭⟭⟭⟭⟭*⟭
CODE (`(`App (val_set_field rtree) (``pl) (``p)) ;
       `(`App (val_set_field ltree) (``p) (``plr)) ;
        `$(``pl))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree
                            ┆ rightRotate (node x (node xl tll tlr) tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
        mxapp NodeSpecs.Triple_set_field_rtree.
A: Type
EA: Enc A
x, xl: A
tll, tlr, tr: tree A
p, pl, pr, pll, plr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆pl┆⟦$MNode ┆ xl ┆ pll ┆ p⟧⟭┆⟬Star┆⟬PointsTo┆pll┆⟦
$MTree ┆ tll⟧⟭┆⟬Star┆⟬PointsTo┆plr┆⟦$MTree ┆ tlr⟧⟭┆⟬Star┆⟬PointsTo┆p┆⟦
$MNode ┆ x ┆ pl ┆ pr⟧⟭┆⟬PointsTo┆pr┆⟦$MTree ┆ tr⟧⟭⟭⟭⟭⟭*⟭
CODE (`(`App (val_set_field ltree) (``p) (``plr)) ;
       `$(``pl))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree
                            ┆ rightRotate (node x (node xl tll tlr) tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
        mxapp NodeSpecs.Triple_set_field_ltree.
A: Type
EA: Enc A
x, xl: A
tll, tlr, tr: tree A
p, pl, pr, pll, plr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p┆⟦$MNode ┆ x ┆ plr ┆ pr⟧⟭┆⟬Star┆⟬PointsTo┆pl┆⟦
$MNode ┆ xl ┆ pll ┆ p⟧⟭┆⟬Star┆⟬PointsTo┆pll┆⟦$MTree ┆ tll⟧⟭┆⟬Star┆⟬PointsTo┆plr┆⟦
$MTree ┆ tlr⟧⟭┆⟬PointsTo┆pr┆⟦$MTree ┆ tr⟧⟭⟭⟭⟭⟭*⟭
CODE (`$(``pl))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree
                            ┆ rightRotate (node x (node xl tll tlr) tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
        xchange <- (@MTree_node A EA p).
A: Type
EA: Enc A
x, xl: A
tll, tlr, tr: tree A
p, pl, pr, pll, plr: loc
⟬*PRE@⟬Star┆⟬PointsTo┆p┆⟦$MTree ┆ node x tlr tr⟧⟭┆⟬Star┆⟬PointsTo┆pl┆⟦
$MNode ┆ xl ┆ pll ┆ p⟧⟭┆⟬PointsTo┆pll┆⟦$MTree ┆ tll⟧⟭⟭⟭*⟭
CODE (`$(``pl))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree
                            ┆ rightRotate (node x (node xl tll tlr) tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭ xchange <- MTree_node.
A: Type
EA: Enc A
x, xl: A
tll, tlr, tr: tree A
p, pl, pr, pll, plr: loc
⟬*PRE@⟬PointsTo┆pl┆⟦$MTree ┆ node xl tll (node x tlr tr)⟧⟭*⟭
CODE (`$(``pl))
⟬*POST@ fun x0 : loc =>
        ⟬Star┆⟬PointsTo┆x0┆⟦$MTree
                            ┆ rightRotate (node x (node xl tll tlr) tr)⟧⟭┆⟬Opaque┆GC⟭⟭*⟭
        mxvals.
  Qed.