---

Step * of Lemma es-interface-pair-prior-programmable

∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  X;Y
  = eclass-compose2(λys,xs. if (#(ys) =z 1)
                           then if (#(xs) =z 1) then {<only(xs), only(ys)>} else {} fi 
                           else {}
                           fi ;Y;Prior(X))
  ∈ EClass(A × B) 
  supposing Singlevalued(X)
BY
{ (Auto
   THEN ((BLemma `es-interface-extensionality` THENA Auto) THEN Try ((ProveSV THEN Auto)))
   THEN RepeatFor 2 ((D 0 THENA Auto))) }

1
1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. Y : EClass(B)
6. Singlevalued(X)
7. ys : bag(B)@i
8. xs : bag(A)@i
9. (#(ys) =z 1) ∈ 𝔹
10. #(ys) = 1 ∈ ℤ
11. (#(xs) =z 1) ∈ 𝔹
12. #(xs) = 1 ∈ ℤ
13. x : A@i
14. y : A@i
⊢ x ↓∈ xs ⇒ y ↓∈ xs ⇒ (x = y ∈ A)

2
1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. Y : EClass(B)
6. Singlevalued(X)
7. ys : bag(B)@i
8. xs : bag(A)@i
9. (#(ys) =z 1) ∈ 𝔹
10. #(ys) = 1 ∈ ℤ
11. (#(xs) =z 1) ∈ 𝔹
12. #(xs) = 1 ∈ ℤ
13. x : B@i
14. y : B@i
⊢ x ↓∈ ys ⇒ y ↓∈ ys ⇒ (x = y ∈ B)

3
1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. Y : EClass(B)
6. Singlevalued(X)
7. es : EO+(Info)@i'
8. e : E@i
⊢ ↑e ∈b X;Y
⇐⇒ ↑e
    ∈b eclass-compose2(λys,xs. if (#(ys) =z 1)
                              then if (#(xs) =z 1) then {<only(xs), only(ys)>} else {} fi 
                              else {}
                              fi ;Y;Prior(X))

4
1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. Y : EClass(B)
6. Singlevalued(X)
7. es : EO+(Info)@i'
8. e : E@i
⊢ (↑e ∈b X;Y)
⇒ (↑e
   ∈b eclass-compose2(λys,xs. if (#(ys) =z 1)
                             then if (#(xs) =z 1) then {<only(xs), only(ys)>} else {} fi 
                             else {}
                             fi ;Y;Prior(X)))
⇒ (X;Y(e)
   = eclass-compose2(λys,xs. if (#(ys) =z 1)
                            then if (#(xs) =z 1) then {<only(xs), only(ys)>} else {} fi 
                            else {}
                            fi ;Y;Prior(X))(e)
   ∈ (A × B))

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].
    X;Y
    =  eclass-compose2(\mlambda{}ys,xs.  if  (\#(ys)  =\msubz{}  1)
                                                      then  if  (\#(xs)  =\msubz{}  1)  then  \{<only(xs),  only(ys)>\}  else  \{\}  fi 
                                                      else  \{\}
                                                      fi  ;Y;Prior(X)) 
    supposing  Singlevalued(X)


By

---

Latex:
(Auto
  THEN  ((BLemma  `es-interface-extensionality`  THENA  Auto)  THEN  Try  ((ProveSV  THEN  Auto)))
  THEN  RepeatFor  2  ((D  0  THENA  Auto)))

---

Home Index