Step
*
1
of Lemma
state-class3-fun-eq
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
BY
{ (Repeat ((RWO "member-parallel-class-bool" 0 THENA Auto))
THEN (RWO "member-eclass-eclass1" 0 THENA Auto)
THEN Repeat (AutoSplit)
THEN Try (Fold `state-class3` 0)) }
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)
21. ↑e ∈b X1
22. ↑first(e)
⊢ ((tr1 o X1) || (tr2 o X2) || (tr3 o X3)@e (init loc(e))) = (tr1 loc(e) X1@e (init loc(e))) ∈ B
2
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. ¬↑first(e)
16. single-valued-classrel(es;X3;A3)
17. single-valued-classrel(es;X2;A2)
18. single-valued-classrel(es;X1;A1)
19. disjoint-classrel(es;A2;X2;A3;X3)
20. disjoint-classrel(es;A1;X1;A3;X3)
21. disjoint-classrel(es;A1;X1;A2;X2)
22. ↑e ∈b X1
⊢ ((tr1 o X1) || (tr2 o X2) || (tr3 o X3)@e state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e)))
= (tr1 loc(e) X1@e state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e)))
∈ B
3
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. ¬↑e ∈b X1
16. single-valued-classrel(es;X3;A3)
17. single-valued-classrel(es;X2;A2)
18. single-valued-classrel(es;X1;A1)
19. disjoint-classrel(es;A2;X2;A3;X3)
20. disjoint-classrel(es;A1;X1;A3;X3)
21. disjoint-classrel(es;A1;X1;A2;X2)
22. ↑e ∈b X2
23. ↑first(e)
⊢ ((tr1 o X1) || (tr2 o X2) || (tr3 o X3)@e (init loc(e))) = (tr2 loc(e) X2@e (init loc(e))) ∈ B
4
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. ¬↑first(e)
16. ¬↑e ∈b X1
17. single-valued-classrel(es;X3;A3)
18. single-valued-classrel(es;X2;A2)
19. single-valued-classrel(es;X1;A1)
20. disjoint-classrel(es;A2;X2;A3;X3)
21. disjoint-classrel(es;A1;X1;A3;X3)
22. disjoint-classrel(es;A1;X1;A2;X2)
23. ↑e ∈b X2
⊢ ((tr1 o X1) || (tr2 o X2) || (tr3 o X3)@e state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e)))
= (tr2 loc(e) X2@e state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e)))
∈ B
5
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. ¬↑e ∈b X2
16. ¬↑e ∈b X1
17. single-valued-classrel(es;X3;A3)
18. single-valued-classrel(es;X2;A2)
19. single-valued-classrel(es;X1;A1)
20. disjoint-classrel(es;A2;X2;A3;X3)
21. disjoint-classrel(es;A1;X1;A3;X3)
22. disjoint-classrel(es;A1;X1;A2;X2)
23. ↑e ∈b X3
24. ↑first(e)
⊢ ((tr1 o X1) || (tr2 o X2) || (tr3 o X3)@e (init loc(e))) = (tr3 loc(e) X3@e (init loc(e))) ∈ B
6
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. ¬↑first(e)
16. ¬↑e ∈b X2
17. ¬↑e ∈b X1
18. single-valued-classrel(es;X3;A3)
19. single-valued-classrel(es;X2;A2)
20. single-valued-classrel(es;X1;A1)
21. disjoint-classrel(es;A2;X2;A3;X3)
22. disjoint-classrel(es;A1;X1;A3;X3)
23. disjoint-classrel(es;A1;X1;A2;X2)
24. ↑e ∈b X3
⊢ ((tr1 o X1) || (tr2 o X2) || (tr3 o X3)@e state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e)))
= (tr3 loc(e) X3@e state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e)))
∈ B
7
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. ¬↑first(e)
16. ¬↑e ∈b X3
17. ¬↑e ∈b X2
18. ¬↑e ∈b X1
19. single-valued-classrel(es;X3;A3)
20. single-valued-classrel(es;X2;A2)
21. single-valued-classrel(es;X1;A1)
22. disjoint-classrel(es;A2;X2;A3;X3)
23. disjoint-classrel(es;A1;X1;A3;X3)
24. disjoint-classrel(es;A1;X1;A2;X2)
⊢ state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e)) = state-class3(init;tr1;X1;tr2;X2;tr3;X3)(pred(e)) ∈ B
Latex:
Latex:
1. Info : Type
2. B : Type
3. A1 : Type
4. A2 : Type
5. A3 : Type
6. init : Id {}\mrightarrow{} B
7. tr1 : Id {}\mrightarrow{} A1 {}\mrightarrow{} B {}\mrightarrow{} B
8. tr2 : Id {}\mrightarrow{} A2 {}\mrightarrow{} B {}\mrightarrow{} B
9. tr3 : Id {}\mrightarrow{} A3 {}\mrightarrow{} B {}\mrightarrow{} 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)
\mvdash{} if e \mmember{}\msubb{} (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);\mlambda{}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);\mlambda{}loc.\{init loc\})(pred(e))
fi
= 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
By
Latex:
(Repeat ((RWO "member-parallel-class-bool" 0 THENA Auto))
THEN (RWO "member-eclass-eclass1" 0 THENA Auto)
THEN Repeat (AutoSplit)
THEN Try (Fold `state-class3` 0))
Home
Index