# Theory RG_Examples

Up to index of Isabelle/HOL/HoareParallel

theory RG_Examples
imports RG_Syntax
begin

    header {* \section{Examples} *}

    theory RG_Examples imports RG_Syntax begin

    lemmas definitions [simp]= stable_def Pre_def Rely_def Guar_def Post_def Com_def

    subsection {* Set Elements of an Array to Zero *}

    lemma le_less_trans2: "[|(j::nat)<k; i≤ j|] ==> i<k"
    by simp

    lemma add_le_less_mono: "[| (a::nat) < c; b≤d |] ==> a + b < c + d"
    by simp

    record Example1 =
      A :: "nat list"

    lemma Example1:
     "\<turnstile> COBEGIN
          SCHEME [0 ≤ i < n]
         (´A := ´A [i := 0],
         \<lbrace> n < length ´A \<rbrace>,
         \<lbrace> length ºA = length ªA ∧ ºA ! i = ªA ! i \<rbrace>,
         \<lbrace> length ºA = length ªA ∧ (∀j<n. i ≠ j --> ºA ! j = ªA ! j) \<rbrace>,
         \<lbrace> ´A ! i = 0 \<rbrace>)
        COEND
     SAT [\<lbrace> n < length ´A \<rbrace>, \<lbrace> ºA = ªA \<rbrace>, \<lbrace> True \<rbrace>, \<lbrace> ∀i < n. ´A ! i = 0 \<rbrace>]"
    apply(rule Parallel)
    apply (auto intro!: Basic)
    done

    lemma Example1_parameterized:
    "k < t ==>
      \<turnstile> COBEGIN
        SCHEME [k*n≤i<(Suc k)*n] (´A:=´A[i:=0],
       \<lbrace>t*n < length ´A\<rbrace>,
       \<lbrace>t*n < length ºA ∧ length ºA=length ªA ∧ ºA!i = ªA!i\<rbrace>,
       \<lbrace>t*n < length ºA ∧ length ºA=length ªA ∧ (∀j<length ºA . i≠j --> ºA!j = ªA!j)\<rbrace>,
       \<lbrace>´A!i=0\<rbrace>)
       COEND
     SAT [\<lbrace>t*n < length ´A\<rbrace>,
          \<lbrace>t*n < length ºA ∧ length ºA=length ªA ∧ (∀i<n. ºA!(k*n+i)=ªA!(k*n+i))\<rbrace>,
          \<lbrace>t*n < length ºA ∧ length ºA=length ªA ∧
          (∀i<length ºA . (i<k*n --> ºA!i = ªA!i) ∧ ((Suc k)*n ≤ i--> ºA!i = ªA!i))\<rbrace>,
          \<lbrace>∀i<n. ´A!(k*n+i) = 0\<rbrace>]"
    apply(rule Parallel)
        apply auto
      apply(erule_tac x="k*n +i" in allE)
      apply(subgoal_tac "k*n+i <length (A b)")
       apply force
      apply(erule le_less_trans2)
      apply(case_tac t,simp+)
      apply (simp add:add_commute)
      apply(simp add: add_le_mono)
    apply(rule Basic)
       apply simp
       apply clarify
       apply (subgoal_tac "k*n+i< length (A x)")
        apply simp
       apply(erule le_less_trans2)
       apply(case_tac t,simp+)
       apply (simp add:add_commute)
       apply(rule add_le_mono, auto)
    done

    subsection {* Increment a Variable in Parallel *}

    subsubsection {* Two components *}

    record Example2 =
      x  :: nat
      c_0 :: nat
      c_1 :: nat

    lemma Example2:
     "\<turnstile>  COBEGIN
        (⟨ ´x:=´x+1;; ´c_0:=´c_0 + 1 ⟩,
         \<lbrace>´x=´c_0 + ´c_1  ∧ ´c_0=0\<rbrace>,
         \<lbrace>ºc_0 = ªc_0 ∧
            (ºx=ºc_0 + ºc_1
            --> ªx = ªc_0 + ªc_1)\<rbrace>,
         \<lbrace>ºc_1 = ªc_1 ∧
             (ºx=ºc_0 + ºc_1
             --> ªx =ªc_0 + ªc_1)\<rbrace>,
         \<lbrace>´x=´c_0 + ´c_1 ∧ ´c_0=1 \<rbrace>)
      \<parallel>
          (⟨ ´x:=´x+1;; ´c_1:=´c_1+1 ⟩,
         \<lbrace>´x=´c_0 + ´c_1 ∧ ´c_1=0 \<rbrace>,
         \<lbrace>ºc_1 = ªc_1 ∧
            (ºx=ºc_0 + ºc_1
            --> ªx = ªc_0 + ªc_1)\<rbrace>,
         \<lbrace>ºc_0 = ªc_0 ∧
             (ºx=ºc_0 + ºc_1
            --> ªx =ªc_0 + ªc_1)\<rbrace>,
         \<lbrace>´x=´c_0 + ´c_1 ∧ ´c_1=1\<rbrace>)
     COEND
     SAT [\<lbrace>´x=0 ∧ ´c_0=0 ∧ ´c_1=0\<rbrace>,
          \<lbrace>ºx=ªx ∧  ºc_0= ªc_0 ∧ ºc_1=ªc_1\<rbrace>,
          \<lbrace>True\<rbrace>,
          \<lbrace>´x=2\<rbrace>]"
    apply(rule Parallel)
       apply simp_all
       apply clarify
       apply(case_tac i)
        apply simp
        apply(rule conjI)
         apply clarify
         apply simp
        apply clarify
        apply simp
        apply(case_tac j,simp)
        apply simp
       apply simp
       apply(rule conjI)
        apply clarify
        apply simp
       apply clarify
       apply simp
       apply(subgoal_tac "j=0")
        apply (rotate_tac -1)
        apply (simp (asm_lr))
       apply arith
      apply clarify
      apply(case_tac i,simp,simp)
     apply clarify
     apply simp
     apply(erule_tac x=0 in all_dupE)
     apply(erule_tac x=1 in allE,simp)
    apply clarify
    apply(case_tac i,simp)
     apply(rule Await)
      apply simp_all
     apply(clarify)
     apply(rule Seq)
      prefer 2
      apply(rule Basic)
       apply simp_all
      apply(rule subset_refl)
     apply(rule Basic)
     apply simp_all
     apply clarify
     apply simp
    apply(rule Await)
     apply simp_all
    apply(clarify)
    apply(rule Seq)
     prefer 2
     apply(rule Basic)
      apply simp_all
     apply(rule subset_refl)
    apply(auto intro!: Basic)
    done

    subsubsection {* Parameterized *}

    lemma Example2_lemma2_aux: "j<n ==>
     (∑i=0..<n. (b i::nat)) =
     (∑i=0..<j. b i) + b j + (∑i=0..<n-(Suc j) . b (Suc j + i))"
    apply(induct n)
     apply simp_all
    apply(simp add:less_Suc_eq)
     apply(auto)
    apply(subgoal_tac "n - j = Suc(n- Suc j)")
      apply simp
    apply arith
    done

    lemma Example2_lemma2_aux2:
      "j≤ s ==> (∑i::nat=0..<j. (b (s:=t)) i) = (∑i=0..<j. b i)"
    apply(induct j)
     apply (simp_all cong:setsum_cong)
    done

    lemma Example2_lemma2:
     "[|j<n; b j=0|] ==> Suc (∑i::nat=0..<n. b i)=(∑i=0..<n. (b (j := Suc 0)) i)"
    apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
    apply(erule_tac  t="setsum (b(j := (Suc 0))) {0..<n}" in ssubst)
    apply(frule_tac b=b in Example2_lemma2_aux)
    apply(erule_tac  t="setsum b {0..<n}" in ssubst)
    apply(subgoal_tac "Suc (setsum b {0..<j} + b j + (∑i=0..<n - Suc j. b (Suc j + i)))=(setsum b {0..<j} + Suc (b j) + (∑i=0..<n - Suc j. b (Suc j + i)))")
    apply(rotate_tac -1)
    apply(erule ssubst)
    apply(subgoal_tac "j≤j")
     apply(drule_tac b="b" and t="(Suc 0)" in Example2_lemma2_aux2)
    apply(rotate_tac -1)
    apply(erule ssubst)
    apply simp_all
    done

    lemma Example2_lemma2_Suc0: "[|j<n; b j=0|] ==>
     Suc (∑i::nat=0..< n. b i)=(∑i=0..< n. (b (j:=Suc 0)) i)"
    by(simp add:Example2_lemma2)

    record Example2_parameterized =
      C :: "nat => nat"
      y  :: nat

    lemma Example2_parameterized: "0<n ==>
      \<turnstile> COBEGIN SCHEME  [0≤i<n]
         (⟨ ´y:=´y+1;; ´C:=´C (i:=1) ⟩,
         \<lbrace>´y=(∑i=0..<n. ´C i) ∧ ´C i=0\<rbrace>,
         \<lbrace>ºC i = ªC i ∧
          (ºy=(∑i=0..<n. ºC i) --> ªy =(∑i=0..<n. ªC i))\<rbrace>,
         \<lbrace>(∀j<n. i≠j --> ºC j = ªC j) ∧
           (ºy=(∑i=0..<n. ºC i) --> ªy =(∑i=0..<n. ªC i))\<rbrace>,
         \<lbrace>´y=(∑i=0..<n. ´C i) ∧ ´C i=1\<rbrace>)
        COEND
     SAT [\<lbrace>´y=0 ∧ (∑i=0..<n. ´C i)=0 \<rbrace>, \<lbrace>ºC=ªC ∧ ºy=ªy\<rbrace>, \<lbrace>True\<rbrace>, \<lbrace>´y=n\<rbrace>]"
    apply(rule Parallel)
    apply force
    apply force
    apply(force)
    apply clarify
    apply simp
    apply(simp cong:setsum_ivl_cong)
    apply clarify
    apply simp
    apply(rule Await)
    apply simp_all
    apply clarify
    apply(rule Seq)
    prefer 2
    apply(rule Basic)
    apply(rule subset_refl)
    apply simp+
    apply(rule Basic)
    apply simp
    apply clarify
    apply simp
    apply(simp add:Example2_lemma2_Suc0 cong:if_cong)
    apply simp+
    done

    subsection {* Find Least Element *}

    text {* A previous lemma: *}

    lemma mod_aux :"[|i < (n::nat); a mod n = i;  j < a + n; j mod n = i; a < j|] ==> False"
    apply(subgoal_tac "a=a div n*n + a mod n" )
     prefer 2 apply (simp (no_asm_use))
    apply(subgoal_tac "j=j div n*n + j mod n")
     prefer 2 apply (simp (no_asm_use))
    apply simp
    apply(subgoal_tac "a div n*n < j div n*n")
    prefer 2 apply arith
    apply(subgoal_tac "j div n*n < (a div n + 1)*n")
    prefer 2 apply simp
    apply (simp only:mult_less_cancel2)
    apply arith
    done

    record Example3 =
      X :: "nat => nat"
      Y :: "nat => nat"

    lemma Example3: "m mod n=0 ==>
     \<turnstile> COBEGIN
     SCHEME [0≤i<n]
     (WHILE (∀j<n. ´X i < ´Y j)  DO
       IF P(B!(´X i)) THEN ´Y:=´Y (i:=´X i)
       ELSE ´X:= ´X (i:=(´X i)+ n) FI
      OD,
     \<lbrace>(´X i) mod n=i ∧ (∀j<´X i. j mod n=i --> ¬P(B!j)) ∧ (´Y i<m --> P(B!(´Y i)) ∧ ´Y i≤ m+i)\<rbrace>,
     \<lbrace>(∀j<n. i≠j --> ªY j ≤ ºY j) ∧ ºX i = ªX i ∧
       ºY i = ªY i\<rbrace>,
     \<lbrace>(∀j<n. i≠j --> ºX j = ªX j ∧ ºY j = ªY j) ∧
       ªY i ≤ ºY i\<rbrace>,
     \<lbrace>(´X i) mod n=i ∧ (∀j<´X i. j mod n=i --> ¬P(B!j)) ∧ (´Y i<m --> P(B!(´Y i)) ∧ ´Y i≤ m+i) ∧ (∃j<n. ´Y j ≤ ´X i) \<rbrace>)
     COEND
     SAT [\<lbrace> ∀i<n. ´X i=i ∧ ´Y i=m+i \<rbrace>,\<lbrace>ºX=ªX ∧ ºY=ªY\<rbrace>,\<lbrace>True\<rbrace>,
      \<lbrace>∀i<n. (´X i) mod n=i ∧ (∀j<´X i. j mod n=i --> ¬P(B!j)) ∧
        (´Y i<m --> P(B!(´Y i)) ∧ ´Y i≤ m+i) ∧ (∃j<n. ´Y j ≤ ´X i)\<rbrace>]"
    apply(rule Parallel)
    --{*5 subgoals left *}
    apply force+
    apply clarify
    apply simp
    apply(rule While)
        apply force
       apply force
      apply force
     apply(rule_tac pre'="\<lbrace> ´X i mod n = i ∧ (∀j. j<´X i --> j mod n = i --> ¬P(B!j)) ∧ (´Y i < n * q --> P (B!(´Y i))) ∧ ´X i<´Y i\<rbrace>" in Conseq)
         apply force
        apply(rule subset_refl)+
     apply(rule Cond)
        apply force
       apply(rule Basic)
          apply force
         apply fastsimp
        apply force
       apply force
      apply(rule Basic)
         apply simp
         apply clarify
         apply simp
         apply(case_tac "X x (j mod n)≤ j")
          apply(drule le_imp_less_or_eq)
          apply(erule disjE)
           apply(drule_tac j=j and n=n and i="j mod n" and a="X x (j mod n)" in mod_aux)
            apply assumption+
           apply simp+
        apply clarsimp
        apply fastsimp
    apply force+
    done

    text {* Same but with a list as auxiliary variable: *}

    record Example3_list =
      X :: "nat list"
      Y :: "nat list"

    lemma Example3_list: "m mod n=0 ==> \<turnstile> (COBEGIN SCHEME [0≤i<n]
     (WHILE (∀j<n. ´X!i < ´Y!j)  DO
         IF P(B!(´X!i)) THEN ´Y:=´Y[i:=´X!i] ELSE ´X:= ´X[i:=(´X!i)+ n] FI
      OD,
     \<lbrace>n<length ´X ∧ n<length ´Y ∧ (´X!i) mod n=i ∧ (∀j<´X!i. j mod n=i --> ¬P(B!j)) ∧ (´Y!i<m --> P(B!(´Y!i)) ∧ ´Y!i≤ m+i)\<rbrace>,
     \<lbrace>(∀j<n. i≠j --> ªY!j ≤ ºY!j) ∧ ºX!i = ªX!i ∧
       ºY!i = ªY!i ∧ length ºX = length ªX ∧ length ºY = length ªY\<rbrace>,
     \<lbrace>(∀j<n. i≠j --> ºX!j = ªX!j ∧ ºY!j = ªY!j) ∧
       ªY!i ≤ ºY!i ∧ length ºX = length ªX ∧ length ºY = length ªY\<rbrace>,
     \<lbrace>(´X!i) mod n=i ∧ (∀j<´X!i. j mod n=i --> ¬P(B!j)) ∧ (´Y!i<m --> P(B!(´Y!i)) ∧ ´Y!i≤ m+i) ∧ (∃j<n. ´Y!j ≤ ´X!i) \<rbrace>) COEND)
     SAT [\<lbrace>n<length ´X ∧ n<length ´Y ∧ (∀i<n. ´X!i=i ∧ ´Y!i=m+i) \<rbrace>,
          \<lbrace>ºX=ªX ∧ ºY=ªY\<rbrace>,
          \<lbrace>True\<rbrace>,
          \<lbrace>∀i<n. (´X!i) mod n=i ∧ (∀j<´X!i. j mod n=i --> ¬P(B!j)) ∧
            (´Y!i<m --> P(B!(´Y!i)) ∧ ´Y!i≤ m+i) ∧ (∃j<n. ´Y!j ≤ ´X!i)\<rbrace>]"
    apply(rule Parallel)
    --{* 5 subgoals left *}
    apply force+
    apply clarify
    apply simp
    apply(rule While)
        apply force
       apply force
      apply force
     apply(rule_tac pre'="\<lbrace>n<length ´X ∧ n<length ´Y ∧ ´X ! i mod n = i ∧ (∀j. j < ´X ! i --> j mod n = i --> ¬ P (B ! j)) ∧ (´Y ! i < n * q --> P (B ! (´Y ! i))) ∧ ´X!i<´Y!i\<rbrace>" in Conseq)
         apply force
        apply(rule subset_refl)+
     apply(rule Cond)
        apply force
       apply(rule Basic)
          apply force
         apply force
        apply force
       apply force
      apply(rule Basic)
         apply simp
         apply clarify
         apply simp
         apply(rule allI)
         apply(rule impI)+
         apply(case_tac "X x ! i≤ j")
          apply(drule le_imp_less_or_eq)
          apply(erule disjE)
           apply(drule_tac j=j and n=n and i=i and a="X x ! i" in mod_aux)
            apply assumption+
           apply simp
    apply force+
    done

    end

lemmas definitions:

      stable == %f g. ∀x y. x ∈ f --> (x, y) ∈ g --> y ∈ f

      Pre x == fst (snd x)

      Rely x == fst (snd (snd x))

      Guar x == fst (snd (snd (snd x)))

      Post x == snd (snd (snd (snd x)))

      Com x == fst x

lemmas definitions:

      stable == %f g. ∀x y. x ∈ f --> (x, y) ∈ g --> y ∈ f

      Pre x == fst (snd x)

      Rely x == fst (snd (snd x))

      Guar x == fst (snd (snd (snd x)))

      Post x == snd (snd (snd (snd x)))

      Com x == fst x

### Set Elements of an Array to Zero

lemma le_less_trans2:

      [| j < k; i ≤ j |] ==> i < k

lemma add_le_less_mono:

      [| a < c; b ≤ d |] ==> a + b < c + d

lemma Example1:

      \<turnstile> (SCHEME [0 ≤ i < n] (´A := ´A[i := 0], .{n < length ´A}.,
                                        .{length ºA = length ªA ∧ ºA ! i = ªA ! i}.,
                                        .{length ºA = length ªA ∧
                                          (∀j<n. i ≠ j --> ºA ! j = ªA ! j)}.,
                                        .{´A ! i =
                                          0}.)) SAT [.{n
               < length ´A}., .{ºA = ªA}., .{True}., .{∀i<n. ´A ! i = 0}.]

lemma Example1_parameterized:

      k < t
      ==> \<turnstile> (SCHEME [k * n ≤ i < Suc k *
                                            n] (´A := ´A[i := 0],
        .{t * n < length ´A}.,
        .{t * n < length ºA ∧ length ºA = length ªA ∧ ºA ! i = ªA ! i}.,
        .{t * n < length ºA ∧
          length ºA = length ªA ∧ (∀j<length ºA. i ≠ j --> ºA ! j = ªA ! j)}.,
        .{´A ! i =
          0}.)) SAT [.{t * n
                       < length
                          ´A}., .{t * n < length ºA ∧
                                  length ºA = length ªA ∧
                                  (∀i<n. ºA ! (k * n + i) =
                                         ªA !
                                         (k * n +
                                          i))}., .{t * n < length ºA ∧
           length ºA = length ªA ∧
           (∀i<length ºA.
               (i < k * n --> ºA ! i = ªA ! i) ∧
               (Suc k * n ≤ i --> ºA ! i = ªA ! i))}., .{∀i<n. ´A ! (k * n + i) = 0}.]

### Increment a Variable in Parallel

#### Two components

lemma Example2:

      \<turnstile> [(⟨´x := ´x + 1;; ´c_0 := ´c_0 + 1⟩,
                     .{´x = ´c_0 + ´c_1 ∧ ´c_0 = 0}.,
                     .{ºc_0 = ªc_0 ∧ (ºx = ºc_0 + ºc_1 --> ªx = ªc_0 + ªc_1)}.,
                     .{ºc_1 = ªc_1 ∧ (ºx = ºc_0 + ºc_1 --> ªx = ªc_0 + ªc_1)}.,
                     .{´x = ´c_0 + ´c_1 ∧ ´c_0 = 1}.),
                    (⟨´x := ´x + 1;; ´c_1 := ´c_1 + 1⟩,
                     .{´x = ´c_0 + ´c_1 ∧ ´c_1 = 0}.,
                     .{ºc_1 = ªc_1 ∧ (ºx = ºc_0 + ºc_1 --> ªx = ªc_0 + ªc_1)}.,
                     .{ºc_0 = ªc_0 ∧ (ºx = ºc_0 + ºc_1 --> ªx = ªc_0 + ªc_1)}.,
                     .{´x = ´c_0 + ´c_1 ∧
                       ´c_1 =
                       1}.)] SAT [.{´x = 0 ∧
                                    ´c_0 = 0 ∧
                                    ´c_1 =
                                    0}., .{ºx = ªx ∧
                                           ºc_0 = ªc_0 ∧
                                           ºc_1 = ªc_1}., .{True}., .{´x = 2}.]

#### Parameterized

lemma Example2_lemma2_aux:

      j < n
      ==> setsum b {0..<n} =
          setsum b {0..<j} + b j + (∑i = 0..<n - Suc j. b (Suc j + i))

lemma Example2_lemma2_aux2:

      j ≤ s ==> setsum (b(s := t)) {0..<j} = setsum b {0..<j}

lemma Example2_lemma2:

      [| j < n; b j = 0 |] ==> Suc (setsum b {0..<n}) = setsum (b(j := Suc 0)) {0..<n}

lemma Example2_lemma2_Suc0:

      [| j < n; b j = 0 |] ==> Suc (setsum b {0..<n}) = setsum (b(j := Suc 0)) {0..<n}

lemma Example2_parameterized:

      0 < n
      ==> \<turnstile> (SCHEME [0 ≤ i < n] (⟨´y := ´y + 1;; ´C := ´C(i := 1)⟩,
                                            .{´y = setsum ´C {0..<n} ∧ ´C i = 0}.,
                                            .{ºC i = ªC i ∧
      (ºy = setsum ºC {0..<n} --> ªy = setsum ªC {0..<n})}.,
                                            .{(∀j<n. i ≠ j --> ºC j = ªC j) ∧
      (ºy = setsum ºC {0..<n} --> ªy = setsum ªC {0..<n})}.,
                                            .{´y = setsum ´C {0..<n} ∧
      ´C i =
      1}.)) SAT [.{´y = 0 ∧
                   setsum ´C {0..<n} =
                   0}., .{ºC = ªC ∧ ºy = ªy}., .{True}., .{´y = n}.]

### Find Least Element

lemma mod_aux:

      [| i < n; a mod n = i; j < a + n; j mod n = i; a < j |] ==> False

lemma Example3:

      m mod n = 0
      ==> \<turnstile> (SCHEME [0 ≤ i < n] (_While_inv (∀j<n. ´X i < ´Y j)
                                             (IF P (B ! ´X i) THEN ´Y := ´Y(i := ´X i)
      ELSE ´X := ´X(i := ´X i + n)FI),
                                            .{´X i mod n = i ∧
      (∀j<´X i. j mod n = i --> ¬ P (B ! j)) ∧
      (´Y i < m --> P (B ! ´Y i) ∧ ´Y i ≤ m + i)}.,
                                            .{(∀j<n. i ≠ j --> ªY j ≤ ºY j) ∧
      ºX i = ªX i ∧ ºY i = ªY i}.,
                                            .{(∀j<n.
          i ≠ j --> ºX j = ªX j ∧ ºY j = ªY j) ∧
      ªY i ≤ ºY i}.,
                                            .{´X i mod n = i ∧
      (∀j<´X i. j mod n = i --> ¬ P (B ! j)) ∧
      (´Y i < m --> P (B ! ´Y i) ∧ ´Y i ≤ m + i) ∧
      (∃j<n. ´Y j
             ≤ ´X i)}.)) SAT [.{∀i<n. ´X i = i ∧
                                      ´Y i =
                                      m + i}., .{ºX = ªX ∧
         ºY =
         ªY}., .{True}., .{∀i<n. ´X i mod n = i ∧
                                 (∀j<´X i. j mod n = i --> ¬ P (B ! j)) ∧
                                 (´Y i < m --> P (B ! ´Y i) ∧ ´Y i ≤ m + i) ∧
                                 (∃j<n. ´Y j ≤ ´X i)}.]

lemma Example3_list:

      m mod n = 0
      ==> \<turnstile> (SCHEME [0 ≤ i < n] (_While_inv
                                             (∀j<n.
         ´Example3_list.X ! i < ´Example3_list.Y ! j)
                                             (IF P (B ! (´Example3_list.X ! i))
      THEN ´Example3_list.Y := ´Example3_list.Y[i := ´Example3_list.X ! i]
      ELSE ´Example3_list.X := ´Example3_list.X[i := ´Example3_list.X ! i + n]FI),
                                            .{n < length ´Example3_list.X ∧
      n < length ´Example3_list.Y ∧
      ´Example3_list.X ! i mod n = i ∧
      (∀j<´Example3_list.X ! i. j mod n = i --> ¬ P (B ! j)) ∧
      (´Example3_list.Y ! i < m -->
       P (B ! (´Example3_list.Y ! i)) ∧ ´Example3_list.Y ! i ≤ m + i)}.,
                                            .{(∀j<n.
          i ≠ j --> ªExample3_list.Y ! j ≤ ºExample3_list.Y ! j) ∧
      ºExample3_list.X ! i = ªExample3_list.X ! i ∧
      ºExample3_list.Y ! i = ªExample3_list.Y ! i ∧
      length ºExample3_list.X = length ªExample3_list.X ∧
      length ºExample3_list.Y = length ªExample3_list.Y}.,
                                            .{(∀j<n.
          i ≠ j -->
          ºExample3_list.X ! j = ªExample3_list.X ! j ∧
          ºExample3_list.Y ! j = ªExample3_list.Y ! j) ∧
      ªExample3_list.Y ! i ≤ ºExample3_list.Y ! i ∧
      length ºExample3_list.X = length ªExample3_list.X ∧
      length ºExample3_list.Y = length ªExample3_list.Y}.,
                                            .{´Example3_list.X ! i mod n = i ∧
      (∀j<´Example3_list.X ! i. j mod n = i --> ¬ P (B ! j)) ∧
      (´Example3_list.Y ! i < m -->
       P (B ! (´Example3_list.Y ! i)) ∧ ´Example3_list.Y ! i ≤ m + i) ∧
      (∃j<n. ´Example3_list.Y ! j
             ≤ ´Example3_list.X !
               i)}.)) SAT [.{n < length ´Example3_list.X ∧
                             n < length ´Example3_list.Y ∧
                             (∀i<n. ´Example3_list.X ! i = i ∧
                                    ´Example3_list.Y ! i =
                                    m + i)}., .{ºExample3_list.X = ªExample3_list.X ∧
        ºExample3_list.Y =
        ªExample3_list.Y}., .{True}., .{∀i<n. ´Example3_list.X ! i mod n = i ∧
      (∀j<´Example3_list.X ! i. j mod n = i --> ¬ P (B ! j)) ∧
      (´Example3_list.Y ! i < m -->
       P (B ! (´Example3_list.Y ! i)) ∧ ´Example3_list.Y ! i ≤ m + i) ∧
      (∃j<n. ´Example3_list.Y ! j ≤ ´Example3_list.X ! i)}.]