Step
*
1
3
1
of Lemma
eq-Game_transitivity
1. g : Game
2. ∀m:Game. ((left-option{i:l}(g;m) ∨ right-option{i:l}(g;m)) ⇒ (∀H,K:Game. (m ≡ H ⇒ H ≡ K ⇒ m ≡ K)))
3. H : Game
4. K : Game
5. ∀i:left-indices(g). ∃j:left-indices(H). left-move(g;i) ≡ left-move(H;j)
6. ∀i:right-indices(g). ∃j:right-indices(H). right-move(g;i) ≡ right-move(H;j)
7. ∀i:left-indices(H). ∃j:left-indices(g). left-move(H;i) ≡ left-move(g;j)
8. ∀i:right-indices(H). ∃j:right-indices(g). right-move(H;i) ≡ right-move(g;j)
9. ∀i:left-indices(H). ∃j:left-indices(K). left-move(H;i) ≡ left-move(K;j)
10. ∀i:right-indices(H). ∃j:right-indices(K). right-move(H;i) ≡ right-move(K;j)
11. ∀i:right-indices(K). ∃j:right-indices(H). right-move(K;i) ≡ right-move(H;j)
12. ∀i:left-indices(g). ∃j:left-indices(K). left-move(g;i) ≡ left-move(K;j)
13. ∀i:right-indices(g). ∃j:right-indices(K). right-move(g;i) ≡ right-move(K;j)
14. i : left-indices(K)
15. j : left-indices(H)
16. left-move(K;i) ≡ left-move(H;j)
17. k : left-indices(g)
18. left-move(H;j) ≡ left-move(g;k)
⊢ left-move(K;i) ≡ left-move(g;k)
BY
{ ((FLemma `eq-Game_inversion` [-3] THENA Auto)
THEN (FLemma `eq-Game_inversion` [-2] THENA Auto)
THEN (BLemma `eq-Game_inversion` THENA Auto)) }
1
1. g : Game
2. ∀m:Game. ((left-option{i:l}(g;m) ∨ right-option{i:l}(g;m)) ⇒ (∀H,K:Game. (m ≡ H ⇒ H ≡ K ⇒ m ≡ K)))
3. H : Game
4. K : Game
5. ∀i:left-indices(g). ∃j:left-indices(H). left-move(g;i) ≡ left-move(H;j)
6. ∀i:right-indices(g). ∃j:right-indices(H). right-move(g;i) ≡ right-move(H;j)
7. ∀i:left-indices(H). ∃j:left-indices(g). left-move(H;i) ≡ left-move(g;j)
8. ∀i:right-indices(H). ∃j:right-indices(g). right-move(H;i) ≡ right-move(g;j)
9. ∀i:left-indices(H). ∃j:left-indices(K). left-move(H;i) ≡ left-move(K;j)
10. ∀i:right-indices(H). ∃j:right-indices(K). right-move(H;i) ≡ right-move(K;j)
11. ∀i:right-indices(K). ∃j:right-indices(H). right-move(K;i) ≡ right-move(H;j)
12. ∀i:left-indices(g). ∃j:left-indices(K). left-move(g;i) ≡ left-move(K;j)
13. ∀i:right-indices(g). ∃j:right-indices(K). right-move(g;i) ≡ right-move(K;j)
14. i : left-indices(K)
15. j : left-indices(H)
16. left-move(K;i) ≡ left-move(H;j)
17. k : left-indices(g)
18. left-move(H;j) ≡ left-move(g;k)
19. left-move(H;j) ≡ left-move(K;i)
20. left-move(g;k) ≡ left-move(H;j)
⊢ left-move(g;k) ≡ left-move(K;i)
Latex:
Latex:
1. g : Game
2. \mforall{}m:Game
((left-option\{i:l\}(g;m) \mvee{} right-option\{i:l\}(g;m)) {}\mRightarrow{} (\mforall{}H,K:Game. (m \mequiv{} H {}\mRightarrow{} H \mequiv{} K {}\mRightarrow{} m \mequiv{} K)))
3. H : Game
4. K : Game
5. \mforall{}i:left-indices(g). \mexists{}j:left-indices(H). left-move(g;i) \mequiv{} left-move(H;j)
6. \mforall{}i:right-indices(g). \mexists{}j:right-indices(H). right-move(g;i) \mequiv{} right-move(H;j)
7. \mforall{}i:left-indices(H). \mexists{}j:left-indices(g). left-move(H;i) \mequiv{} left-move(g;j)
8. \mforall{}i:right-indices(H). \mexists{}j:right-indices(g). right-move(H;i) \mequiv{} right-move(g;j)
9. \mforall{}i:left-indices(H). \mexists{}j:left-indices(K). left-move(H;i) \mequiv{} left-move(K;j)
10. \mforall{}i:right-indices(H). \mexists{}j:right-indices(K). right-move(H;i) \mequiv{} right-move(K;j)
11. \mforall{}i:right-indices(K). \mexists{}j:right-indices(H). right-move(K;i) \mequiv{} right-move(H;j)
12. \mforall{}i:left-indices(g). \mexists{}j:left-indices(K). left-move(g;i) \mequiv{} left-move(K;j)
13. \mforall{}i:right-indices(g). \mexists{}j:right-indices(K). right-move(g;i) \mequiv{} right-move(K;j)
14. i : left-indices(K)
15. j : left-indices(H)
16. left-move(K;i) \mequiv{} left-move(H;j)
17. k : left-indices(g)
18. left-move(H;j) \mequiv{} left-move(g;k)
\mvdash{} left-move(K;i) \mequiv{} left-move(g;k)
By
Latex:
((FLemma `eq-Game\_inversion` [-3] THENA Auto)
THEN (FLemma `eq-Game\_inversion` [-2] THENA Auto)
THEN (BLemma `eq-Game\_inversion` THENA Auto))
Home
Index