---

Step * of Lemma find_transitions_wf

∀[A:Type]. ∀[f:A ⟶ A ⟶ 𝔹]. ∀[L:A List].  find_transitions(f;L) ∈ Unit + ℤ × (Unit + ℤ) supposing 1 < ||L||
BY
{ (Auto
   THEN DVar `L'
   THEN Reduce -1
   THEN Auto
   THEN RepUR ``find_transitions`` 0
   THEN (CallByValueReduce 0⋅ THENA Auto)
   THEN (GenConcl ⌜(inl ⋅) = z ∈ (Unit + ℤ)⌝ ⋅ THENA Auto)) }

1
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 + ℤ)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:A  List].
    find\_transitions(f;L)  \mmember{}  Unit  +  \mBbbZ{}  \mtimes{}  (Unit  +  \mBbbZ{})  supposing  1  <  ||L||


By

---

Latex:
(Auto
  THEN  DVar  `L'
  THEN  Reduce  -1
  THEN  Auto
  THEN  RepUR  ``find\_transitions``  0
  THEN  (CallByValueReduce  0\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(inl  \mcdot{})  =  z\mkleeneclose{}  \mcdot{}  THENA  Auto))

---

Home Index