Step
*
1
1
1
1
of Lemma
add-graph-decls-declares-tag
1. S : Id List@i'
2. d2 : {i:Id| (i ∈ S)} ⟶ x:Id fp-> Type@i'
3. d3 : i:{i:Id| (i ∈ S)} ⟶ k:{k:Knd| ↑hasloc(k;i)} fp-> Type@i'
4. G : Graph(S)@i
5. T : Type@i'
6. a : Id ⟶ Id ⟶ Id@i
7. b : Id@i
8. ∀i:Id. ((i ∈ S) ⇒ (∀k:Knd. ((k ∈ fpf-domain(d3 i)) ⇒ (↑isrcv(k)) ⇒ (tag(k) = b ∈ Id) ⇒ (d3 i(k) = T ∈ Type))))@i'
9. i : Id@i
10. (i ∈ S)@i
11. ∀k:Knd. ((k ∈ fpf-domain(d3 i)) ⇒ (↑isrcv(k)) ⇒ (tag(k) = b ∈ Id) ⇒ (d3 i(k) = T ∈ Type))
12. k : Knd@i
13. (k ∈ fpf-domain(d3 i)) ⇒ (↑isrcv(k)) ⇒ (tag(k) = b ∈ Id) ⇒ (d3 i(k) = T ∈ Type)
14. (k ∈ fpf-domain(graph-rcvs(S;G;a;b;i) |-fpf-> T)) ∨ (k ∈ fpf-domain(d3 i))
15. ↑isrcv(k)@i
16. tag(k) = b ∈ Id@i
17. v : 𝔹@i
18. ¬↑v
19. k ∈ dom(graph-rcvs(S;G;a;b;i) |-fpf-> T) = ff@i
20. False ⇒ (k ∈ graph-rcvs(S;G;a;b;i))@i
21. False ⇐ (k ∈ graph-rcvs(S;G;a;b;i))@i
⊢ d3 i(k) = T ∈ Type
BY
{ D 14 }
1
1. S : Id List@i'
2. d2 : {i:Id| (i ∈ S)} ⟶ x:Id fp-> Type@i'
3. d3 : i:{i:Id| (i ∈ S)} ⟶ k:{k:Knd| ↑hasloc(k;i)} fp-> Type@i'
4. G : Graph(S)@i
5. T : Type@i'
6. a : Id ⟶ Id ⟶ Id@i
7. b : Id@i
8. ∀i:Id. ((i ∈ S) ⇒ (∀k:Knd. ((k ∈ fpf-domain(d3 i)) ⇒ (↑isrcv(k)) ⇒ (tag(k) = b ∈ Id) ⇒ (d3 i(k) = T ∈ Type))))@i'
9. i : Id@i
10. (i ∈ S)@i
11. ∀k:Knd. ((k ∈ fpf-domain(d3 i)) ⇒ (↑isrcv(k)) ⇒ (tag(k) = b ∈ Id) ⇒ (d3 i(k) = T ∈ Type))
12. k : Knd@i
13. (k ∈ fpf-domain(d3 i)) ⇒ (↑isrcv(k)) ⇒ (tag(k) = b ∈ Id) ⇒ (d3 i(k) = T ∈ Type)
14. (k ∈ fpf-domain(graph-rcvs(S;G;a;b;i) |-fpf-> T))
15. ↑isrcv(k)@i
16. tag(k) = b ∈ Id@i
17. v : 𝔹@i
18. ¬↑v
19. k ∈ dom(graph-rcvs(S;G;a;b;i) |-fpf-> T) = ff@i
20. False ⇒ (k ∈ graph-rcvs(S;G;a;b;i))@i
21. False ⇐ (k ∈ graph-rcvs(S;G;a;b;i))@i
⊢ d3 i(k) = T ∈ Type
2
1. S : Id List@i'
2. d2 : {i:Id| (i ∈ S)} ⟶ x:Id fp-> Type@i'
3. d3 : i:{i:Id| (i ∈ S)} ⟶ k:{k:Knd| ↑hasloc(k;i)} fp-> Type@i'
4. G : Graph(S)@i
5. T : Type@i'
6. a : Id ⟶ Id ⟶ Id@i
7. b : Id@i
8. ∀i:Id. ((i ∈ S) ⇒ (∀k:Knd. ((k ∈ fpf-domain(d3 i)) ⇒ (↑isrcv(k)) ⇒ (tag(k) = b ∈ Id) ⇒ (d3 i(k) = T ∈ Type))))@i'
9. i : Id@i
10. (i ∈ S)@i
11. ∀k:Knd. ((k ∈ fpf-domain(d3 i)) ⇒ (↑isrcv(k)) ⇒ (tag(k) = b ∈ Id) ⇒ (d3 i(k) = T ∈ Type))
12. k : Knd@i
13. (k ∈ fpf-domain(d3 i)) ⇒ (↑isrcv(k)) ⇒ (tag(k) = b ∈ Id) ⇒ (d3 i(k) = T ∈ Type)
14. (k ∈ fpf-domain(d3 i))
15. ↑isrcv(k)@i
16. tag(k) = b ∈ Id@i
17. v : 𝔹@i
18. ¬↑v
19. k ∈ dom(graph-rcvs(S;G;a;b;i) |-fpf-> T) = ff@i
20. False ⇒ (k ∈ graph-rcvs(S;G;a;b;i))@i
21. False ⇐ (k ∈ graph-rcvs(S;G;a;b;i))@i
⊢ d3 i(k) = T ∈ Type
Latex:
Latex:
1. S : Id List@i'
2. d2 : \{i:Id| (i \mmember{} S)\} {}\mrightarrow{} x:Id fp-> Type@i'
3. d3 : i:\{i:Id| (i \mmember{} S)\} {}\mrightarrow{} k:\{k:Knd| \muparrow{}hasloc(k;i)\} fp-> Type@i'
4. G : Graph(S)@i
5. T : Type@i'
6. a : Id {}\mrightarrow{} Id {}\mrightarrow{} Id@i
7. b : Id@i
8. \mforall{}i:Id
((i \mmember{} S)
{}\mRightarrow{} (\mforall{}k:Knd. ((k \mmember{} fpf-domain(d3 i)) {}\mRightarrow{} (\muparrow{}isrcv(k)) {}\mRightarrow{} (tag(k) = b) {}\mRightarrow{} (d3 i(k) = T))))@i'
9. i : Id@i
10. (i \mmember{} S)@i
11. \mforall{}k:Knd. ((k \mmember{} fpf-domain(d3 i)) {}\mRightarrow{} (\muparrow{}isrcv(k)) {}\mRightarrow{} (tag(k) = b) {}\mRightarrow{} (d3 i(k) = T))
12. k : Knd@i
13. (k \mmember{} fpf-domain(d3 i)) {}\mRightarrow{} (\muparrow{}isrcv(k)) {}\mRightarrow{} (tag(k) = b) {}\mRightarrow{} (d3 i(k) = T)
14. (k \mmember{} fpf-domain(graph-rcvs(S;G;a;b;i) |-fpf-> T)) \mvee{} (k \mmember{} fpf-domain(d3 i))
15. \muparrow{}isrcv(k)@i
16. tag(k) = b@i
17. v : \mBbbB{}@i
18. \mneg{}\muparrow{}v
19. k \mmember{} dom(graph-rcvs(S;G;a;b;i) |-fpf-> T) = ff@i
20. False {}\mRightarrow{} (k \mmember{} graph-rcvs(S;G;a;b;i))@i
21. False \mLeftarrow{}{} (k \mmember{} graph-rcvs(S;G;a;b;i))@i
\mvdash{} d3 i(k) = T
By
Latex:
D 14
Home
Index