val of_fun (m:(r:reg -> t_reg r)) : Pure t
  (requires True)
  (ensures fun m' -> (forall (r:reg).{:pattern (m r) \/ (sel r m')} m r == sel r m'))
let of_fun m =
  reveal_opaque (`%sel) sel;
//  FStar.FunctionalExtensionality.on_dom reg m
  let m0_3 = ((m (Reg 0 0), m (Reg 0 1)), (m (Reg 0 2), m (Reg 0 3))) in
  let m4_7 = ((m (Reg 0 4), m (Reg 0 5)), (m (Reg 0 6), m (Reg 0 7))) in
  let m8_11 = ((m (Reg 0 8), m (Reg 0 9)), (m (Reg 0 10), m (Reg 0 11))) in
  let m12_15 = ((m (Reg 0 12), m (Reg 0 13)), (m (Reg 0 14), m (Reg 0 15))) in
  let m0 = ((m0_3, m4_7), (m8_11, m12_15)) in
  let m0_3 = ((m (Reg 1 0), m (Reg 1 1)), (m (Reg 1 2), m (Reg 1 3))) in
  let m4_7 = ((m (Reg 1 4), m (Reg 1 5)), (m (Reg 1 6), m (Reg 1 7))) in
  let m8_11 = ((m (Reg 1 8), m (Reg 1 9)), (m (Reg 1 10), m (Reg 1 11))) in
  let m12_15 = ((m (Reg 1 12), m (Reg 1 13)), (m (Reg 1 14), m (Reg 1 15))) in
  let m1 = ((m0_3, m4_7), (m8_11, m12_15)) in
  (m0, m1)
val of_fun (m:(r:reg -> t_reg r)) : Pure t
  (requires True)
  (ensures fun m' -> (forall (r:reg).{:pattern (m r) \/ (sel r m')} m r == sel r m'))
let of_fun m =
reveal_opaque (`%sel) sel;
let m0_3 = ((m (Reg 0 0), m (Reg 0 1)), (m (Reg 0 2), m (Reg 0 3))) in
let m4_7 = ((m (Reg 0 4), m (Reg 0 5)), (m (Reg 0 6), m (Reg 0 7))) in
let m8_11 = ((m (Reg 0 8), m (Reg 0 9)), (m (Reg 0 10), m (Reg 0 11))) in
let m12_15 = ((m (Reg 0 12), m (Reg 0 13)), (m (Reg 0 14), m (Reg 0 15))) in
let m0 = ((m0_3, m4_7), (m8_11, m12_15)) in
let m0_3 = ((m (Reg 1 0), m (Reg 1 1)), (m (Reg 1 2), m (Reg 1 3))) in
let m4_7 = ((m (Reg 1 4), m (Reg 1 5)), (m (Reg 1 6), m (Reg 1 7))) in
let m8_11 = ((m (Reg 1 8), m (Reg 1 9)), (m (Reg 1 10), m (Reg 1 11))) in
let m12_15 = ((m (Reg 1 12), m (Reg 1 13)), (m (Reg 1 14), m (Reg 1 15))) in
let m1 = ((m0_3, m4_7), (m8_11, m12_15)) in
(m0, m1)
Vale.X64.Regs.fst.checked
Vale.X64.Machine_s.fst.checked Vale.Lib.Map16.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.X64.Regs.fst
Vale.X64.Machine_s.reg Vale.X64.Machine_s.t_reg FStar.Pervasives.Native.Mktuple2 Vale.Lib.Map16.map16 Vale.X64.Machine_s.nat64 Vale.X64.Machine_s.quad32 FStar.Pervasives.Native.tuple2 Vale.Lib.Map16.map8 Vale.Def.Types_s.quad32 Vale.Lib.Map16.map4 Vale.Lib.Map16.map2 Vale.X64.Machine_s.Reg Vale.Def.Words_s.nat64 Prims.unit FStar.Pervasives.reveal_opaque Vale.X64.Regs.t Vale.X64.Regs.sel
module Vale.X64.Regs
open FStar.Mul
open Vale.X64.Machine_s
val of_fun (m:(r:reg -> t_reg r)) : Pure t
  (requires True)
  (ensures fun m' -> (forall (r:reg).{:pattern (m r) \/ (sel r m')} m r == sel r m'))
m: (r: Vale.X64.Machine_s.reg -> Vale.X64.Machine_s.t_reg r) -> Prims.Pure Vale.X64.Regs.t