---

Step * of Lemma state-class3-fun-eq

∀[Info,B,A1,A2,A3:Type]. ∀[init:Id ─→ B]. ∀[tr1:Id ─→ A1 ─→ B ─→ B]. ∀[tr2:Id ─→ A2 ─→ B ─→ B].
∀[tr3:Id ─→ A3 ─→ B ─→ B]. ∀[X1:EClass(A1)]. ∀[X2:EClass(A2)]. ∀[X3:EClass(A3)]. ∀[es:EO+(Info)]. ∀[e:E].
  (state-class3(init;tr1;X1;tr2;X2;tr3;X3)(e)
     = if e ∈b X1
         then if first(e)
              then tr1 loc(e) X1@e (init loc(e))
              else tr1 loc(e) X1@e state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e))
              fi 
       if e ∈b X2
         then if first(e)
              then tr2 loc(e) X2@e (init loc(e))
              else tr2 loc(e) X2@e state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e))
              fi 
       if e ∈b X3
         then if first(e)
              then tr3 loc(e) X3@e (init loc(e))
              else tr3 loc(e) X3@e state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e))
              fi 
       if first(e) then init loc(e)
       else state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e))
       fi 
     ∈ B) supposing 
     (disjoint-classrel(es;A1;X1;A2;X2) and 
     disjoint-classrel(es;A1;X1;A3;X3) and 
     disjoint-classrel(es;A2;X2;A3;X3) and 
     single-valued-classrel(es;X1;A1) and 
     single-valued-classrel(es;X2;A2) and 
     single-valued-classrel(es;X3;A3))
BY
{ ((UnivCD THENA Auto)
   THEN UnfoldAtAddr [2;2] 0
   THEN (RWO "loop-class-state-fun-eq" 0 THENA Auto)
   THEN ProveFunctional
   THEN Auto) }

1
1. Info : Type
2. B : Type
3. A1 : Type
4. A2 : Type
5. A3 : Type
6. init : Id ─→ B
7. tr1 : Id ─→ A1 ─→ B ─→ B
8. tr2 : Id ─→ A2 ─→ B ─→ B
9. tr3 : Id ─→ A3 ─→ B ─→ B
10. X1 : EClass(A1)
11. X2 : EClass(A2)
12. X3 : EClass(A3)
13. es : EO+(Info)
14. e : E
15. single-valued-classrel(es;X3;A3)
16. single-valued-classrel(es;X2;A2)
17. single-valued-classrel(es;X1;A1)
18. disjoint-classrel(es;A2;X2;A3;X3)
19. disjoint-classrel(es;A1;X1;A3;X3)
20. disjoint-classrel(es;A1;X1;A2;X2)
⊢ if e ∈b (tr1 o X1) || (tr2 o X2) || (tr3 o X3)
    then if first(e)
         then (tr1 o X1) || (tr2 o X2) || (tr3 o X3)@e (init loc(e))
         else (tr1 o X1) || (tr2 o X2) || (tr3 o X3)@e 
              loop-class-state((tr1 o X1) || (tr2 o X2) || (tr3 o X3);λloc.{init loc})(pred(e))
         fi 
if first(e) then init loc(e)
else loop-class-state((tr1 o X1) || (tr2 o X2) || (tr3 o X3);λloc.{init loc})(pred(e))
fi 
= if e ∈b X1
    then if first(e)
         then tr1 loc(e) X1@e (init loc(e))
         else tr1 loc(e) X1@e state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e))
         fi 
  if e ∈b X2
    then if first(e)
         then tr2 loc(e) X2@e (init loc(e))
         else tr2 loc(e) X2@e state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e))
         fi 
  if e ∈b X3
    then if first(e)
         then tr3 loc(e) X3@e (init loc(e))
         else tr3 loc(e) X3@e state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e))
         fi 
  if first(e) then init loc(e)
  else state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e))
  fi 
∈ B

---

Latex:

---

Latex:
\mforall{}[Info,B,A1,A2,A3:Type].  \mforall{}[init:Id  {}\mrightarrow{}  B].  \mforall{}[tr1:Id  {}\mrightarrow{}  A1  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[tr2:Id  {}\mrightarrow{}  A2  {}\mrightarrow{}  B  {}\mrightarrow{}  B].
\mforall{}[tr3:Id  {}\mrightarrow{}  A3  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[X1:EClass(A1)].  \mforall{}[X2:EClass(A2)].  \mforall{}[X3:EClass(A3)].  \mforall{}[es:EO+(Info)].
\mforall{}[e:E].
    (state-class3(init;tr1;X1;tr2;X2;tr3;X3)(e)
          =  if  e  \mmember{}\msubb{}  X1
                  then  if  first(e)
                            then  tr1  loc(e)  X1@e  (init  loc(e))
                            else  tr1  loc(e)  X1@e  state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e))
                            fi 
              if  e  \mmember{}\msubb{}  X2
                  then  if  first(e)
                            then  tr2  loc(e)  X2@e  (init  loc(e))
                            else  tr2  loc(e)  X2@e  state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e))
                            fi 
              if  e  \mmember{}\msubb{}  X3
                  then  if  first(e)
                            then  tr3  loc(e)  X3@e  (init  loc(e))
                            else  tr3  loc(e)  X3@e  state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e))
                            fi 
              if  first(e)  then  init  loc(e)
              else  state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e))
              fi  )  supposing 
          (disjoint-classrel(es;A1;X1;A2;X2)  and 
          disjoint-classrel(es;A1;X1;A3;X3)  and 
          disjoint-classrel(es;A2;X2;A3;X3)  and 
          single-valued-classrel(es;X1;A1)  and 
          single-valued-classrel(es;X2;A2)  and 
          single-valued-classrel(es;X3;A3))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  UnfoldAtAddr  [2;2]  0
  THEN  (RWO  "loop-class-state-fun-eq"  0  THENA  Auto)
  THEN  ProveFunctional
  THEN  Auto)

---

Home Index