---

Step * 1 1 of Lemma rec-class-unique


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
⊢ (X es e) = if e ∈b prior(Z) then let e' = prior(Z)(e) in F[es;e';Z(e');e] else G[es;e] fi  ∈ bag(T)
BY
{ ((InstHyp [⌈es⌉;⌈e⌉] 6⋅ THENA Auto) THEN NthHypEq (-1) THEN EqCD) }

1
.....subterm..... T:t
1: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)
⊢ bag(T) = bag(T) ∈ Type

2
.....subterm..... T:t
2: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)
⊢ (X es e) = (X es e) ∈ bag(T)

3
.....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)

4
.....antecedent..... 
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)
⊢ True

---

Latex:

---

Latex:

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
\mvdash{}  (X  es  e)  =  if  e  \mmember{}\msubb{}  prior(Z)  then  let  e'  =  prior(Z)(e)  in  F[es;e';Z(e');e]  else  G[es;e]  fi 


By

---

Latex:
((InstHyp  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]  6\mcdot{}  THENA  Auto)  THEN  NthHypEq  (-1)  THEN  EqCD)

---

Home Index