Step
*
1
1
3
of Lemma
rec-class-unique
.....subterm..... T:t
3:n
1. Info : Type
2. T : Type
3. G : es:EO+(Info) ─→ E ─→ bag(T)
4. F : es:EO+(Info) ─→ e':E ─→ T ─→ {e:E| (e' <loc e)} ─→ bag(T)
5. X : EClass(T)
6. ∀es:EO+(Info). ∀e:E.
((X es e) = if e ∈b prior(X) then let e' = prior(X)(e) in F[es;e';X(e');e] else G[es;e] fi ∈ bag(T))
7. RecClass(first e
G[es;e]
or next e after e' with value v
F[es;e';v;e]) ∈ EClass(T)
8. es : EO+(Info)
9. e : E@i
10. Z : EClass(T)@i'
11. ∀e1:E. ((e1 < e) ⇒ ((X es e1) = (Z es e1) ∈ bag(T)))@i
12. (X es e) = if e ∈b prior(X) then let e' = prior(X)(e) in F[es;e';X(e');e] else G[es;e] fi ∈ bag(T)
⊢ if e ∈b prior(Z) then let e' = prior(Z)(e) in F[es;e';Z(e');e] else G[es;e] fi
= if e ∈b prior(X) then let e' = prior(X)(e) in F[es;e';X(e');e] else G[es;e] fi
∈ bag(T)
BY
{ (RepUR ``let`` 0 THEN (BoolCase ⌈e ∈b prior(Z)⌉⋅ THENA Auto) THEN (BoolCase ⌈e ∈b prior(X)⌉⋅ THENA Auto)) }
1
1. Info : Type
2. T : Type
3. G : es:EO+(Info) ─→ E ─→ bag(T)
4. F : es:EO+(Info) ─→ e':E ─→ T ─→ {e:E| (e' <loc e)} ─→ bag(T)
5. X : EClass(T)
6. ∀es:EO+(Info). ∀e:E.
((X es e) = if e ∈b prior(X) then let e' = prior(X)(e) in F[es;e';X(e');e] else G[es;e] fi ∈ bag(T))
7. RecClass(first e
G[es;e]
or next e after e' with value v
F[es;e';v;e]) ∈ EClass(T)
8. es : EO+(Info)
9. e : E@i
10. Z : EClass(T)@i'
11. ∀e1:E. ((e1 < e) ⇒ ((X es e1) = (Z es e1) ∈ bag(T)))@i
12. (X es e) = if e ∈b prior(X) then let e' = prior(X)(e) in F[es;e';X(e');e] else G[es;e] fi ∈ bag(T)
13. ↑e ∈b prior(Z)
14. ↑e ∈b prior(X)
⊢ F[es;prior(Z)(e);Z(prior(Z)(e));e] = F[es;prior(X)(e);X(prior(X)(e));e] ∈ bag(T)
2
1. Info : Type
2. T : Type
3. G : es:EO+(Info) ─→ E ─→ bag(T)
4. F : es:EO+(Info) ─→ e':E ─→ T ─→ {e:E| (e' <loc e)} ─→ bag(T)
5. X : EClass(T)
6. ∀es:EO+(Info). ∀e:E.
((X es e) = if e ∈b prior(X) then let e' = prior(X)(e) in F[es;e';X(e');e] else G[es;e] fi ∈ bag(T))
7. RecClass(first e
G[es;e]
or next e after e' with value v
F[es;e';v;e]) ∈ EClass(T)
8. es : EO+(Info)
9. e : E@i
10. ¬↑e ∈b prior(X)
11. Z : EClass(T)@i'
12. ∀e1:E. ((e1 < e) ⇒ ((X es e1) = (Z es e1) ∈ bag(T)))@i
13. (X es e) = G[es;e] ∈ bag(T)
14. ↑e ∈b prior(Z)
⊢ F[es;prior(Z)(e);Z(prior(Z)(e));e] = G[es;e] ∈ bag(T)
3
1. Info : Type
2. T : Type
3. G : es:EO+(Info) ─→ E ─→ bag(T)
4. F : es:EO+(Info) ─→ e':E ─→ T ─→ {e:E| (e' <loc e)} ─→ bag(T)
5. X : EClass(T)
6. ∀es:EO+(Info). ∀e:E.
((X es e) = if e ∈b prior(X) then let e' = prior(X)(e) in F[es;e';X(e');e] else G[es;e] fi ∈ bag(T))
7. RecClass(first e
G[es;e]
or next e after e' with value v
F[es;e';v;e]) ∈ EClass(T)
8. es : EO+(Info)
9. e : E@i
10. Z : EClass(T)@i'
11. ¬↑e ∈b prior(Z)
12. ∀e1:E. ((e1 < e) ⇒ ((X es e1) = (Z es e1) ∈ bag(T)))@i
13. (X es e) = if e ∈b prior(X) then let e' = prior(X)(e) in F[es;e';X(e');e] else G[es;e] fi ∈ bag(T)
14. ↑e ∈b prior(X)
⊢ G[es;e] = F[es;prior(X)(e);X(prior(X)(e));e] ∈ bag(T)
4
1. Info : Type
2. T : Type
3. G : es:EO+(Info) ─→ E ─→ bag(T)
4. F : es:EO+(Info) ─→ e':E ─→ T ─→ {e:E| (e' <loc e)} ─→ bag(T)
5. X : EClass(T)
6. ∀es:EO+(Info). ∀e:E.
((X es e) = if e ∈b prior(X) then let e' = prior(X)(e) in F[es;e';X(e');e] else G[es;e] fi ∈ bag(T))
7. RecClass(first e
G[es;e]
or next e after e' with value v
F[es;e';v;e]) ∈ EClass(T)
8. es : EO+(Info)
9. e : E@i
10. ¬↑e ∈b prior(X)
11. Z : EClass(T)@i'
12. ¬↑e ∈b prior(Z)
13. ∀e1:E. ((e1 < e) ⇒ ((X es e1) = (Z es e1) ∈ bag(T)))@i
14. (X es e) = G[es;e] ∈ bag(T)
⊢ G[es;e] = G[es;e] ∈ bag(T)
Latex:
Latex:
.....subterm..... T:t
3:n
1. Info : Type
2. T : Type
3. G : es:EO+(Info) {}\mrightarrow{} E {}\mrightarrow{} bag(T)
4. F : es:EO+(Info) {}\mrightarrow{} e':E {}\mrightarrow{} T {}\mrightarrow{} \{e:E| (e' <loc e)\} {}\mrightarrow{} bag(T)
5. X : EClass(T)
6. \mforall{}es:EO+(Info). \mforall{}e:E.
((X es e) = if e \mmember{}\msubb{} prior(X) then let e' = prior(X)(e) in F[es;e';X(e');e] else G[es;e] fi )
7. RecClass(first e
G[es;e]
or next e after e' with value v
F[es;e';v;e]) \mmember{} EClass(T)
8. es : EO+(Info)
9. e : E@i
10. Z : EClass(T)@i'
11. \mforall{}e1:E. ((e1 < e) {}\mRightarrow{} ((X es e1) = (Z es e1)))@i
12. (X es e) = if e \mmember{}\msubb{} prior(X) then let e' = prior(X)(e) in F[es;e';X(e');e] else G[es;e] fi
\mvdash{} if e \mmember{}\msubb{} prior(Z) then let e' = prior(Z)(e) in F[es;e';Z(e');e] else G[es;e] fi
= if e \mmember{}\msubb{} prior(X) then let e' = prior(X)(e) in F[es;e';X(e');e] else G[es;e] fi
By
Latex:
(RepUR ``let`` 0
THEN (BoolCase \mkleeneopen{}e \mmember{}\msubb{} prior(Z)\mkleeneclose{}\mcdot{} THENA Auto)
THEN (BoolCase \mkleeneopen{}e \mmember{}\msubb{} prior(X)\mkleeneclose{}\mcdot{} THENA Auto))
Home
Index