---

Step * 1 of Lemma find_transitions_wf


1. A : Type
2. f : A ⟶ A ⟶ 𝔹
3. u : A
4. v : A List
5. 1 < ||v|| + 1
6. z : Unit + ℤ
7. (inl ⋅) = z ∈ (Unit + ℤ)
⊢ snd(snd(list_accum'(λd,l. let i,b,p,q = d 
                            in if isr(p) ∧b isr(q)
                               then d
                               else let a,as = l 
                                    in eval i' = i + 1 in
                                       if null(as)
                                       then eval b' = f a u in
                                            if b ∧b (¬bb')
                                              then eval q' = if isl(q) then inr 0  else q fi  in
                                                   <i', b', inr i , q'>
                                            if b' ∧b (¬bb)
                                              then eval p' = if isl(p) then inr 0  else p fi  in
                                                   <i', b', p', inr i >
                                            if isr(p) then <i', b', p, inr 0 >
                                            if isr(q) then <i', b', inr 0 , q>
                                            else <i', b', p, q>
                                            fi 
                                       else eval b' = f a hd(as) in
                                            if b ∧b (¬bb') then <i', b', inr i , q>
                                            if b' ∧b (¬bb) then <i', b', p, inr i >
                                            else <i', b', p, q>
                                            fi 
                                       fi 
                               fi   ;<1, f u hd(v), z, z>;v))) ∈ Unit + ℤ × (Unit + ℤ)
BY
{ (RepeatFor 5 ((MemCD THEN Try (QuickAuto)))
   THEN D (-1)
   THEN D -2
   THEN ((Reduce -1 THEN Assert ⌜False⌝⋅ THEN Complete (Auto))
         ORELSE (Thin (-1) THEN RepeatFor 3 (D -3) THEN D -4 THEN D -3 THEN Reduce 0)
         ORELSE Auto)
   THEN D -1
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  f  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}
3.  u  :  A
4.  v  :  A  List
5.  1  <  ||v||  +  1
6.  z  :  Unit  +  \mBbbZ{}
7.  (inl  \mcdot{})  =  z
\mvdash{}  snd(snd(list\_accum'(\mlambda{}d,l.  let  i,b,p,q  =  d 
                                                        in  if  isr(p)  \mwedge{}\msubb{}  isr(q)
                                                              then  d
                                                              else  let  a,as  =  l 
                                                                        in  eval  i'  =  i  +  1  in
                                                                              if  null(as)
                                                                              then  eval  b'  =  f  a  u  in
                                                                                        if  b  \mwedge{}\msubb{}  (\mneg{}\msubb{}b')
                                                                                            then  eval  q'  =  if  isl(q)  then  inr  0    else  q  fi    in
                                                                                                      <i',  b',  inr  i  ,  q'>
                                                                                        if  b'  \mwedge{}\msubb{}  (\mneg{}\msubb{}b)
                                                                                            then  eval  p'  =  if  isl(p)  then  inr  0    else  p  fi    in
                                                                                                      <i',  b',  p',  inr  i  >
                                                                                        if  isr(p)  then  <i',  b',  p,  inr  0  >
                                                                                        if  isr(q)  then  <i',  b',  inr  0  ,  q>
                                                                                        else  <i',  b',  p,  q>
                                                                                        fi 
                                                                              else  eval  b'  =  f  a  hd(as)  in
                                                                                        if  b  \mwedge{}\msubb{}  (\mneg{}\msubb{}b')  then  <i',  b',  inr  i  ,  q>
                                                                                        if  b'  \mwedge{}\msubb{}  (\mneg{}\msubb{}b)  then  <i',  b',  p,  inr  i  >
                                                                                        else  <i',  b',  p,  q>
                                                                                        fi 
                                                                              fi 
                                                              fi      ;ə,  f  u  hd(v),  z,  z>v)))  \mmember{}  Unit  +  \mBbbZ{}  \mtimes{}  (Unit  +  \mBbbZ{})


By

---

Latex:
(RepeatFor  5  ((MemCD  THEN  Try  (QuickAuto)))
  THEN  D  (-1)
  THEN  D  -2
  THEN  ((Reduce  -1  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Complete  (Auto))
              ORELSE  (Thin  (-1)  THEN  RepeatFor  3  (D  -3)  THEN  D  -4  THEN  D  -3  THEN  Reduce  0)
              ORELSE  Auto)
  THEN  D  -1
  THEN  Reduce  0
  THEN  Auto)

---

Home Index