---

Step * of Lemma state-class2-fun-eq

∀[Info,B,A1,A2:Type]. ∀[init:Id ─→ B]. ∀[tr1:Id ─→ A1 ─→ B ─→ B]. ∀[tr2:Id ─→ A2 ─→ B ─→ B]. ∀[X1:EClass(A1)].
∀[X2:EClass(A2)]. ∀[es:EO+(Info)]. ∀[e:E].
  (state-class2(init;tr1;X1;tr2;X2)(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-class2(init;tr1;X1;tr2;X2)(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-class2(init;tr1;X1;tr2;X2)(pred(e))
              fi 
       if first(e) then init loc(e)
       else state-class2(init;tr1;X1;tr2;X2)(pred(e))
       fi 
     ∈ B) supposing 
     (disjoint-classrel(es;A1;X1;A2;X2) and 
     single-valued-classrel(es;X1;A1) and 
     single-valued-classrel(es;X2;A2))
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. init : Id ─→ B
6. tr1 : Id ─→ A1 ─→ B ─→ B
7. tr2 : Id ─→ A2 ─→ B ─→ B
8. X1 : EClass(A1)
9. X2 : EClass(A2)
10. es : EO+(Info)
11. e : E
12. single-valued-classrel(es;X2;A2)
13. single-valued-classrel(es;X1;A1)
14. disjoint-classrel(es;A1;X1;A2;X2)
⊢ if e ∈b (tr1 o X1) || (tr2 o X2)
    then if first(e)
         then (tr1 o X1) || (tr2 o X2)@e (init loc(e))
         else (tr1 o X1) || (tr2 o X2)@e loop-class-state((tr1 o X1) || (tr2 o X2);λloc.{init loc})(pred(e))
         fi 
if first(e) then init loc(e)
else loop-class-state((tr1 o X1) || (tr2 o X2);λ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-class2(init;tr1;X1;tr2;X2)(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-class2(init;tr1;X1;tr2;X2)(pred(e))
         fi 
  if first(e) then init loc(e)
  else state-class2(init;tr1;X1;tr2;X2)(pred(e))
  fi 
∈ B

---

Latex:

---

Latex:
\mforall{}[Info,B,A1,A2: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{}[X1:EClass(A1)].  \mforall{}[X2:EClass(A2)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    (state-class2(init;tr1;X1;tr2;X2)(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-class2(init;tr1;X1;tr2;X2)(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-class2(init;tr1;X1;tr2;X2)(pred(e))
                            fi 
              if  first(e)  then  init  loc(e)
              else  state-class2(init;tr1;X1;tr2;X2)(pred(e))
              fi  )  supposing 
          (disjoint-classrel(es;A1;X1;A2;X2)  and 
          single-valued-classrel(es;X1;A1)  and 
          single-valued-classrel(es;X2;A2))


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