Theory Replacement_Lepoll

section‹Lambda-replacements required for cardinal inequalities›

theory Replacement_Lepoll
  imports
    ZF_Library_Relative
begin

definition
  lepoll_assumptions1 :: "[io,i,[i,i]i,i,i,i,i,i,i]  o" where
  "lepoll_assumptions1(M,A,F,S,fa,K,x,f,r)  xS. strong_replacement(M, λy z. y  F(A, x)  z = {x, y})"

definition
  lepoll_assumptions2 :: "[io,i,[i,i]i,i,i,i,i,i,i]  o" where
  "lepoll_assumptions2(M,A,F,S,fa,K,x,f,r)  strong_replacement(M, λx z. z = Sigfun(x, F(A)))"

definition
  lepoll_assumptions3 :: "[io,i,[i,i]i,i,i,i,i,i,i]  o" where
  "lepoll_assumptions3(M,A,F,S,fa,K,x,f,r)  strong_replacement(M, λx y. y = F(A, x))"

definition
  lepoll_assumptions4 :: "[io,i,[i,i]i,i,i,i,i,i,i]  o" where
  "lepoll_assumptions4(M,A,F,S,fa,K,x,f,r)  strong_replacement(M, λx y. y = x, minimum(r, F(A, x)))"

definition
  lepoll_assumptions5 :: "[io,i,[i,i]i,i,i,i,i,i,i]  o" where
  "lepoll_assumptions5(M,A,F,S,fa,K,x,f,r) 
strong_replacement(M, λx y. y = x, μ i. x  F(A, i), f ` (μ i. x  F(A, i)) ` x)"

definition
  lepoll_assumptions6 :: "[io,i,[i,i]i,i,i,i,i,i,i]  o" where
  "lepoll_assumptions6(M,A,F,S,fa,K,x,f,r)  strong_replacement(M, λy z. y  inj⇗M⇖(F(A, x),S)  z = {x, y})"

definition
  lepoll_assumptions7 :: "[io,i,[i,i]i,i,i,i,i,i,i]  o" where
  "lepoll_assumptions7(M,A,F,S,fa,K,x,f,r)  strong_replacement(M, λx y. y = inj⇗M⇖(F(A, x),S))"

definition
  lepoll_assumptions8 :: "[io,i,[i,i]i,i,i,i,i,i,i]  o" where
  "lepoll_assumptions8(M,A,F,S,fa,K,x,f,r)  strong_replacement(M, λx z. z = Sigfun(x, λi. inj⇗M⇖(F(A, i),S)))"

definition
  lepoll_assumptions9 :: "[io,i,[i,i]i,i,i,i,i,i,i]  o" where
  "lepoll_assumptions9(M,A,F,S,fa,K,x,f,r)  strong_replacement(M, λx y. y = x, minimum(r, inj⇗M⇖(F(A, x),S)))"

definition
  lepoll_assumptions10 :: "[io,i,[i,i]i,i,i,i,i,i,i]  o" where
  "lepoll_assumptions10(M,A,F,S,fa,K,x,f,r)  strong_replacement
           (M, λx z. z = Sigfun(x, λk. if k  range(f) then F(A, converse(f) ` k) else 0))"

definition
  lepoll_assumptions11 :: "[io,i,[i,i]i,i,i,i,i,i,i]  o" where
  "lepoll_assumptions11(M,A,F,S,fa,K,x,f,r)  strong_replacement(M, λx y. y = (if x  range(f) then F(A, converse(f) ` x) else 0))"

definition
  lepoll_assumptions12 :: "[io,i,[i,i]i,i,i,i,i,i,i]  o" where
  "lepoll_assumptions12(M,A,F,S,fa,K,x,f,r)  strong_replacement(M, λy z. y  F(A, converse(f) ` x)  z = {x, y})"

definition
  lepoll_assumptions13 :: "[io,i,[i,i]i,i,i,i,i,i,i]  o" where
  "lepoll_assumptions13(M,A,F,S,fa,K,x,f,r)  strong_replacement
         (M, λx y. y = x, minimum(r, if x  range(f) then F(A,converse(f) ` x) else 0))"

definition
  lepoll_assumptions14 :: "[io,i,[i,i]i,i,i,i,i,i,i]  o" where
  "lepoll_assumptions14(M,A,F,S,fa,K,x,f,r)  strong_replacement
         (M, λx y. y = x, μ i. x  (if i  range(f) then F(A, converse(f) ` i) else 0),
                        fa ` (μ i. x  (if i  range(f) then F(A, converse(f) ` i) else 0)) ` x)"

definition
  lepoll_assumptions15 :: "[io,i,[i,i]i,i,i,i,i,i,i]  o" where
  "lepoll_assumptions15(M,A,F,S,fa,K,x,f,r)  strong_replacement
         (M, λy z. y  inj⇗M⇖(if x  range(f) then F(A, converse(f) ` x) else 0,K)  z = {x, y})"

definition
  lepoll_assumptions16 :: "[io,i,[i,i]i,i,i,i,i,i,i]  o" where
  "lepoll_assumptions16(M,A,F,S,fa,K,x,f,r)  strong_replacement(M, λx y. y = inj⇗M⇖(if x  range(f) then F(A, converse(f) ` x) else 0,K))"

definition
  lepoll_assumptions17 :: "[io,i,[i,i]i,i,i,i,i,i,i]  o" where
  "lepoll_assumptions17(M,A,F,S,fa,K,x,f,r)  strong_replacement
             (M, λx z. z = Sigfun(x, λi. inj⇗M⇖(if i  range(f) then F(A, converse(f) ` i) else 0,K)))"

definition
  lepoll_assumptions18 :: "[io,i,[i,i]i,i,i,i,i,i,i]  o" where
  "lepoll_assumptions18(M,A,F,S,fa,K,x,f,r)  strong_replacement
         (M, λx y. y = x, minimum(r, inj⇗M⇖(if x  range(f) then F(A, converse(f) ` x) else 0,K)))"

lemmas lepoll_assumptions_defs[simp] = lepoll_assumptions1_def
  lepoll_assumptions2_def lepoll_assumptions3_def lepoll_assumptions4_def
  lepoll_assumptions5_def lepoll_assumptions6_def lepoll_assumptions7_def
  lepoll_assumptions8_def lepoll_assumptions9_def lepoll_assumptions10_def
  lepoll_assumptions11_def lepoll_assumptions12_def lepoll_assumptions13_def
  lepoll_assumptions14_def lepoll_assumptions15_def lepoll_assumptions16_def
  lepoll_assumptions17_def lepoll_assumptions18_def

definition if_range_F where
  [simp]: "if_range_F(H,f,i)  if i  range(f) then H(converse(f) ` i) else 0"

definition if_range_F_else_F where
  "if_range_F_else_F(H,b,f,i)  if b=0 then if_range_F(H,f,i) else H(i)"

lemma (in M_basic) lam_Least_assumption_general:
  assumes
    separations:
    "A'[M]. separation(M, λy. xA'. y = x, μ i. x  if_range_F_else_F(F(A),b,f,i))"
    and
    mem_F_bound:"x c. xF(A,c)  c  range(f)  U(A)"
    and
    types:"M(A)" "M(b)" "M(f)" "M(U(A))"
  shows "lam_replacement(M,λx . μ i. x  if_range_F_else_F(F(A),b,f,i))"
proof -
  have "xX. (μ i. x  if_range_F_else_F(F(A),b,f,i)) 
    Pow⇗M⇖((X  range(f)  U(A)))" if "M(X)" for X
  proof
    fix x
    assume "xX"
    moreover
    note M(X)
    moreover from calculation
    have "M(x)" by (auto dest:transM)
    moreover
    note assms
    ultimately
    show "(μ i. x  if_range_F_else_F(F(A),b,f,i)) 
        Pow⇗M⇖((X  range(f)  U(A)))"
    proof (rule_tac Least_in_Pow_rel_Union, cases "b=0", simp_all)
      case True
      fix c
      assume asm:"x  if_range_F_else_F(F(A), 0, f, c)"
      with mem_F_bound
      show "cX  c  range(f)  c  U(A)"
        unfolding if_range_F_else_F_def if_range_F_def by (cases "crange(f)") auto
    next
      case False
      fix c
      assume "x  if_range_F_else_F(F(A), b, f, c)"
      with False mem_F_bound[of x c]
      show "cX  c  range(f)  cU(A)"
        unfolding if_range_F_else_F_def if_range_F_def by auto
    qed
  qed
  with assms
  show ?thesis
    using bounded_lam_replacement[of "λx.(μ i. x  if_range_F_else_F(F(A),b,f,i))"
        "λX. Pow⇗M⇖((X  range(f)  U(A)))"] by simp
qed

lemma (in M_basic) lam_Least_assumption_ifM_b0:
  fixes F
  defines "F  λ_ x. if M(x) then x else 0"
  assumes
    separations:
    "A'[M]. separation(M, λy. xA'. y = x, μ i. x  if_range_F_else_F(F(A),0,f,i))"
    and
    types:"M(A)" "M(f)"
  shows "lam_replacement(M,λx . μ i. x  if_range_F_else_F(F(A),0,f,i))"
    (is "lam_replacement(M,λx . Least(?P(x)))")
proof -
  {
    fix x X
    assume "M(X)" "xX" "(μ i. ?P(x,i))  0"
    moreover from this
    obtain m where "Ord(m)" "?P(x,m)"
      using Least_0[of "?P(_)"] by auto
    moreover
    note assms
    moreover
    have "?P(x,i)  (M(converse(f) ` i)  i  range(f)  x  converse(f) ` i)"  for i
      unfolding F_def if_range_F_else_F_def if_range_F_def by auto
    ultimately
    have "(μ i. ?P(x,i))  range (f)"
      unfolding F_def if_range_F_else_F_def if_range_F_def
      by (rule_tac LeastI2) auto
  }
  with assms
  show ?thesis
    by (rule_tac bounded_lam_replacement[of _ "λX. range(f)  {0}"]) auto
qed

lemma (in M_replacement) lam_Least_assumption_ifM_bnot0:
  fixes F
  defines "F  λ_ x. if M(x) then x else 0"
  assumes
    lam_replacement_minimum:"lam_replacement(M, λp. minimum(fst(p),snd(p)))"
    and
    separations:
    "A'[M]. separation(M, λy. xA'. y = x, μ i. x  if_range_F_else_F(F(A),b,f,i))"
    "separation(M,Ord)"
    and
    types:"M(A)" "M(f)"
    and
    "b0"
  shows "lam_replacement(M,λx . μ i. x  if_range_F_else_F(F(A),b,f,i))"
    (is "lam_replacement(M,λx . Least(?P(x)))")
proof -
  have "M(x) (μ i. (M(i)  x  i)  M(i)) = (if Ord(x) then succ(x) else 0)" for x
    using Ord_in_Ord
    apply (auto intro:Least_0, rule_tac Least_equality, simp_all)
    by (frule lt_Ord) (auto dest:le_imp_not_lt[of _ x] intro:ltI[of x])
  moreover
  have "lam_replacement(M, λx. if Ord(x) then succ(x) else 0)"
    using lam_replacement_if[OF _ _ separations(2)] lam_replacement_identity
      lam_replacement_constant lam_replacement_hcomp lam_replacement_succ
    by simp
  moreover
  note types b0
  ultimately
  show ?thesis
    using lam_replacement_cong
    unfolding F_def if_range_F_else_F_def if_range_F_def
    by auto
qed

lemma (in M_replacement) lam_Least_assumption_drSR_Y:
  fixes F r' D
  defines "F  drSR_Y(r',D)"
  assumes "A'[M]. separation(M, λy. xA'. y = x, μ i. x  if_range_F_else_F(F(A),b,f,i))"
    "M(A)" "M(b)" "M(f)" "M(r')"
    and
    lam_replacement_minimum:"lam_replacement(M, λp. minimum(fst(p),snd(p)))"
  shows "lam_replacement(M,λx . μ i. x  if_range_F_else_F(F(A),b,f,i))"
proof -
  from assms(2-)
  have [simp]: "M(X)  M(X  range(f)  {domain(x) . x  A})"
    "M(r')  M(X)  M({restrict(x,r') . x  A})"
    for X r'
    using lam_replacement_domain[THEN lam_replacement_imp_strong_replacement,
        THEN RepFun_closed, of A]
      lam_replacement_restrict'[THEN lam_replacement_imp_strong_replacement,
        THEN RepFun_closed, of r' A] by (auto dest:transM)
  have "xX. (μ i. x  if_range_F_else_F(F(A),b,f,i)) 
    Pow⇗M⇖((X  range(f)  {domain(x). xA}  {restrict(x,r'). xA}  domain(A)  range(A)  A))" if "M(X)" for X
  proof
    fix x
    assume "xX"
    moreover
    note M(X)
    moreover from calculation
    have "M(x)" by (auto dest:transM)
    moreover
    note assms(2-)
    ultimately
    show "(μ i. x  if_range_F_else_F(F(A),b,f,i)) 
        Pow⇗M⇖((X  range(f)  {domain(x). xA}  {restrict(x,r'). xA}  domain(A)  range(A)  A))"
      unfolding if_range_F_else_F_def if_range_F_def
    proof (rule_tac Least_in_Pow_rel_Union, simp_all,cases "b=0", simp_all)
      case True
      fix c
      assume asm:"x  (if c  range(f) then F(A, converse(f) ` c) else 0)"
      then
      show "cX  crange(f)  (xA. c = domain(x))  (xA. c = restrict(x,r'))  c  domain(A)  c  range(A)  (xA. cx)" by auto
    next
      case False
      fix c
      assume "x  F(A, c)"
      then
      show "cX  crange(f)  (xA. c = domain(x))  (xA. c = restrict(x,r'))  c  domain(A)  c  range(A)  (xA. cx)"
        using apply_0
        by (cases "M(c)", auto simp:F_def drSR_Y_def dC_F_def)
    qed
  qed
  with assms(2-)
  show ?thesis
    using bounded_lam_replacement[of "λx.(μ i. x  if_range_F_else_F(F(A),b,f,i))"
        "λX. Pow⇗M⇖((X  range(f)  {domain(x). xA}  {restrict(x,r'). xA}  domain(A)  range(A)  A))"] by simp
qed

locale M_replacement_lepoll = M_replacement + M_inj +
  fixes F
  assumes
    F_type[simp]: "M(A)  x[M]. M(F(A,x))"
    and
    lam_lepoll_assumption_F:"M(A)  lam_replacement(M,F(A))"
    and
    ― ‹Here b is a Boolean.›
    lam_Least_assumption:"M(A)  M(b)  M(f) 
        lam_replacement(M,λx . μ i. x  if_range_F_else_F(F(A),b,f,i))"
    and
    F_args_closed: "M(A)  M(x)  x  F(A,i)  M(i)"
    and
    lam_replacement_inj_rel:"lam_replacement(M, λp. inj⇗M⇖(fst(p),snd(p)))"
    and
    lam_replacement_minimum:"lam_replacement(M, λp. minimum(fst(p),snd(p)))"
begin

declare if_range_F_else_F_def[simp]

lemma lepoll_assumptions1:
  assumes types[simp]:"M(A)" "M(S)"
  shows "lepoll_assumptions1(M,A,F,S,fa,K,x,f,r)"
  using strong_replacement_separation[OF lam_replacement_sing_const_id separation_in_constant]
    transM[of _ S]
  by simp

lemma lepoll_assumptions2:
  assumes types[simp]:"M(A)" "M(S)"
  shows "lepoll_assumptions2(M,A,F,S,fa,K,x,f,r)"
  using lam_replacement_Sigfun lam_replacement_imp_strong_replacement
    assms lam_lepoll_assumption_F
  by simp

lemma lepoll_assumptions3:
  assumes types[simp]:"M(A)"
  shows "lepoll_assumptions3(M,A,F,S,fa,K,x,f,r)"
  using lam_lepoll_assumption_F[THEN lam_replacement_imp_strong_replacement]
  by simp

lemma lepoll_assumptions4:
  assumes types[simp]:"M(A)" "M(r)"
  shows "lepoll_assumptions4(M,A,F,S,fa,K,x,f,r)"
  using lam_replacement_minimum lam_replacement_constant lam_lepoll_assumption_F
  unfolding lepoll_assumptions_defs
    lam_replacement_def[symmetric]
  by (rule_tac lam_replacement_hcomp2[of _ _ minimum])
    (force intro: lam_replacement_identity)+

lemma lam_Least_closed :
  assumes "M(A)" "M(b)" "M(f)"
  shows "x[M]. M(μ i. x  if_range_F_else_F(F(A),b,f,i))"
proof -
  have "x  (if i  range(f) then F(A, converse(f) ` i) else 0)  M(i)" for x i
  proof (cases "irange(f)")
    case True
    with M(f)
    show ?thesis by (auto dest:transM)
  next
    case False
    moreover
    assume "x  (if i  range(f) then F(A, converse(f) ` i) else 0)"
    ultimately
    show ?thesis
      by auto
  qed
  with assms
  show ?thesis
    using F_args_closed[of A] unfolding if_range_F_else_F_def if_range_F_def
    by (clarify, rule_tac Least_closed', cases "b=0") simp_all
qed

lemma lepoll_assumptions5:
  assumes
    types[simp]:"M(A)" "M(f)"
  shows "lepoll_assumptions5(M,A,F,S,fa,K,x,f,r)"
  using
    lam_replacement_apply2[THEN [5] lam_replacement_hcomp2]
    lam_replacement_hcomp[OF _ lam_replacement_apply[of f]]
    lam_replacement_identity
    lam_replacement_product lam_Least_closed[where b=1]
    assms lam_Least_assumption[where b=1,OF M(A) _ M(f)]
  unfolding lepoll_assumptions_defs
    lam_replacement_def[symmetric]
  by simp

lemma lepoll_assumptions6:
  assumes types[simp]:"M(A)" "M(S)" "M(x)"
  shows "lepoll_assumptions6(M,A,F,S,fa,K,x,f,r)"
  using strong_replacement_separation[OF lam_replacement_sing_const_id separation_in_constant]
    lam_replacement_inj_rel
  by simp

lemma lepoll_assumptions7:
  assumes types[simp]:"M(A)" "M(S)" "M(x)"
  shows "lepoll_assumptions7(M,A,F,S,fa,K,x,f,r)"
  using lam_replacement_constant lam_lepoll_assumption_F lam_replacement_inj_rel
  unfolding lepoll_assumptions_defs
  by (rule_tac lam_replacement_imp_strong_replacement)
    (rule_tac lam_replacement_hcomp2[of _ _ "inj_rel(M)"], simp_all)

lemma lepoll_assumptions8:
  assumes types[simp]:"M(A)" "M(S)"
  shows "lepoll_assumptions8(M,A,F,S,fa,K,x,f,r)"
  using lam_replacement_Sigfun lam_replacement_imp_strong_replacement
    lam_replacement_inj_rel lam_replacement_constant
    lam_replacement_hcomp2[of _ _ "inj_rel(M)",OF lam_lepoll_assumption_F[of A]]
  by simp

lemma lepoll_assumptions9:
  assumes types[simp]:"M(A)" "M(S)" "M(r)"
  shows "lepoll_assumptions9(M,A,F,S,fa,K,x,f,r)"
  using lam_replacement_minimum lam_replacement_constant lam_lepoll_assumption_F
    lam_replacement_hcomp2[of _ _ "inj_rel(M)"] lam_replacement_inj_rel lepoll_assumptions4
  unfolding lepoll_assumptions_defs lam_replacement_def[symmetric]
  by (rule_tac lam_replacement_hcomp2[of _ _ minimum])
    (force intro: lam_replacement_identity)+

lemma lepoll_assumptions10:
  assumes types[simp]:"M(A)" "M(f)"
  shows "lepoll_assumptions10(M,A,F,S,fa,K,x,f,r)"
  using lam_replacement_Sigfun lam_replacement_imp_strong_replacement
    lam_replacement_constant[OF nonempty]
    lam_replacement_if[OF _ _ separation_in_constant]
    lam_replacement_hcomp
    lam_replacement_apply[OF converse_closed[OF M(f)]]
    lam_lepoll_assumption_F[of A]
  by simp

lemma lepoll_assumptions11:
  assumes types[simp]:"M(A)" "M(f)"
  shows "lepoll_assumptions11(M, A, F, S, fa, K, x, f, r)"
  using lam_replacement_imp_strong_replacement
    lam_replacement_if[OF _ _ separation_in_constant[of "range(f)"]]
    lam_replacement_constant
    lam_replacement_hcomp lam_replacement_apply
    lam_lepoll_assumption_F
  by simp

lemma lepoll_assumptions12:
  assumes types[simp]:"M(A)" "M(x)" "M(f)"
  shows "lepoll_assumptions12(M,A,F,S,fa,K,x,f,r)"
  using strong_replacement_separation[OF lam_replacement_sing_const_id separation_in_constant]
  by simp

lemma lepoll_assumptions13:
  assumes types[simp]:"M(A)" "M(r)" "M(f)"
  shows "lepoll_assumptions13(M,A,F,S,fa,K,x,f,r)"
  using  lam_replacement_constant[OF nonempty] lam_lepoll_assumption_F
    lam_replacement_hcomp lam_replacement_apply
    lam_replacement_hcomp2[OF lam_replacement_constant[OF M(r)]
      lam_replacement_if[OF _ _ separation_in_constant[of "range(f)"]] _ _
      lam_replacement_minimum] assms
  unfolding lepoll_assumptions_defs
    lam_replacement_def[symmetric]
  by simp

lemma lepoll_assumptions14:
  assumes types[simp]:"M(A)" "M(f)" "M(fa)"
  shows "lepoll_assumptions14(M,A,F,S,fa,K,x,f,r)"
  using
    lam_replacement_apply2[THEN [5] lam_replacement_hcomp2]
    lam_replacement_hcomp[OF _ lam_replacement_apply[of fa]]
    lam_replacement_identity
    lam_replacement_product  lam_Least_closed[where b=0]
    assms lam_Least_assumption[where b=0,OF M(A) _ M(f)]
  unfolding lepoll_assumptions_defs
    lam_replacement_def[symmetric]
  by simp

lemma lepoll_assumptions15:
  assumes types[simp]:"M(A)" "M(x)" "M(f)" "M(K)"
  shows "lepoll_assumptions15(M,A,F,S,fa,K,x,f,r)"
  using strong_replacement_separation[OF lam_replacement_sing_const_id separation_in_constant]
  by simp

lemma lepoll_assumptions16:
  assumes types[simp]:"M(A)" "M(f)" "M(K)"
  shows "lepoll_assumptions16(M,A,F,S,fa,K,x,f,r)"
  using lam_replacement_imp_strong_replacement
    lam_replacement_inj_rel lam_replacement_constant
    lam_replacement_hcomp2[of _ _ "inj_rel(M)"]
    lam_replacement_constant[OF nonempty]
    lam_replacement_if[OF _ _ separation_in_constant]
    lam_replacement_hcomp
    lam_replacement_apply[OF converse_closed[OF M(f)]]
    lam_lepoll_assumption_F[of A]
  by simp

lemma lepoll_assumptions17:
  assumes types[simp]:"M(A)" "M(f)" "M(K)"
  shows "lepoll_assumptions17(M,A,F,S,fa,K,x,f,r)"
  using lam_replacement_Sigfun lam_replacement_imp_strong_replacement
    lam_replacement_inj_rel lam_replacement_constant
    lam_replacement_hcomp2[of _ _ "inj_rel(M)"]
    lam_replacement_constant[OF nonempty]
    lam_replacement_if[OF _ _ separation_in_constant]
    lam_replacement_hcomp
    lam_replacement_apply[OF converse_closed[OF M(f)]]
    lam_lepoll_assumption_F[of A]
  by simp

lemma lepoll_assumptions18:
  assumes types[simp]:"M(A)" "M(K)" "M(f)" "M(r)"
  shows "lepoll_assumptions18(M,A,F,S,fa,K,x,f,r)"
  using lam_replacement_constant lam_replacement_inj_rel lam_lepoll_assumption_F
    lam_replacement_minimum lam_replacement_identity lam_replacement_apply2 separation_in_constant
  unfolding lepoll_assumptions18_def lam_replacement_def[symmetric]
  by (rule_tac lam_replacement_hcomp2[of _ _ minimum], simp_all,
      rule_tac lam_replacement_hcomp2[of _ _ "inj_rel(M)"], simp_all)
    (rule_tac lam_replacement_if, rule_tac lam_replacement_hcomp[of _ "F(A)"],
      rule_tac lam_replacement_hcomp2[of _ _ "(`)"], simp_all)

lemmas lepoll_assumptions = lepoll_assumptions1 lepoll_assumptions2
  lepoll_assumptions3 lepoll_assumptions4 lepoll_assumptions5
  lepoll_assumptions6 lepoll_assumptions7 lepoll_assumptions8
  lepoll_assumptions9 lepoll_assumptions10 lepoll_assumptions11
  lepoll_assumptions12 lepoll_assumptions13 lepoll_assumptions14
  lepoll_assumptions15 lepoll_assumptions16
  lepoll_assumptions17 lepoll_assumptions18

end ― ‹localeM_replacement_lepoll

end