---

Step * 3 2 1 1 of Lemma dl-program-eq-equiv


1. b : Prog
2. a : Prog
3. i : ℤ
4. i = 2 ∈ ℤ
5. p : ℕ
6. ¬(p ∈ dl-prop-atoms() prog(b))
7. ¬(p ∈ dl-prop-atoms() prog(a))
8. ∀K:Type. ∀R:ℕ ⟶ K ⟶ K ⟶ ℙ. ∀P:ℕ ⟶ K ⟶ ℙ. ∀k:K.  ([|<b> atm(p) ⇒ <a> atm(p)|] k)
9. ∀K:Type. ∀R:ℕ ⟶ K ⟶ K ⟶ ℙ. ∀P:ℕ ⟶ K ⟶ ℙ. ∀k:K.  ([|<a> atm(p) ⇒ <b> atm(p)|] k)
10. K : Type
11. R : ℕ ⟶ K ⟶ K ⟶ ℙ
12. P : ℕ ⟶ K ⟶ ℙ
13. k1 : K
14. k2 : K
15. λ2a.λs.if (a =z p) then s = k2 ∈ K else P a s fi  ∈ ℕ ⟶ K ⟶ ℙ
16. [|a|] k1 k2
⊢ [|a|] k1 k2
BY
{ (InstLemma `dl-prog-sem_functionality` [⌜a⌝;⌜K⌝;⌜R⌝;⌜P⌝;⌜λ2a.λs.if (a =z p) then s = k2 ∈ K else P a s fi ⌝;⌜k1⌝;⌜k2⌝]
   ⋅
   THENA Auto
   ) }

1
.....antecedent..... 
1. b : Prog
2. a : Prog
3. i : ℤ
4. i = 2 ∈ ℤ
5. p : ℕ
6. ¬(p ∈ dl-prop-atoms() prog(b))
7. ¬(p ∈ dl-prop-atoms() prog(a))
8. ∀K:Type. ∀R:ℕ ⟶ K ⟶ K ⟶ ℙ. ∀P:ℕ ⟶ K ⟶ ℙ. ∀k:K.  ([|<b> atm(p) ⇒ <a> atm(p)|] k)
9. ∀K:Type. ∀R:ℕ ⟶ K ⟶ K ⟶ ℙ. ∀P:ℕ ⟶ K ⟶ ℙ. ∀k:K.  ([|<a> atm(p) ⇒ <b> atm(p)|] k)
10. K : Type
11. R : ℕ ⟶ K ⟶ K ⟶ ℙ
12. P : ℕ ⟶ K ⟶ ℙ
13. k1 : K
14. k2 : K
15. λ2a.λs.if (a =z p) then s = k2 ∈ K else P a s fi  ∈ ℕ ⟶ K ⟶ ℙ
16. [|a|] k1 k2
⊢ (∀n∈dl-prop-atoms() prog(a).∀k:K. (P[n] k ⇐⇒ (λs.if (n =z p) then s = k2 ∈ K else P n s fi ) k))

2
1. b : Prog
2. a : Prog
3. i : ℤ
4. i = 2 ∈ ℤ
5. p : ℕ
6. ¬(p ∈ dl-prop-atoms() prog(b))
7. ¬(p ∈ dl-prop-atoms() prog(a))
8. ∀K:Type. ∀R:ℕ ⟶ K ⟶ K ⟶ ℙ. ∀P:ℕ ⟶ K ⟶ ℙ. ∀k:K.  ([|<b> atm(p) ⇒ <a> atm(p)|] k)
9. ∀K:Type. ∀R:ℕ ⟶ K ⟶ K ⟶ ℙ. ∀P:ℕ ⟶ K ⟶ ℙ. ∀k:K.  ([|<a> atm(p) ⇒ <b> atm(p)|] k)
10. K : Type
11. R : ℕ ⟶ K ⟶ K ⟶ ℙ
12. P : ℕ ⟶ K ⟶ ℙ
13. k1 : K
14. k2 : K
15. λ2a.λs.if (a =z p) then s = k2 ∈ K else P a s fi  ∈ ℕ ⟶ K ⟶ ℙ
16. [|a|] k1 k2
17. [|a|] k1 k2 ⇐⇒ [|a|] k1 k2
⊢ [|a|] k1 k2

---

Latex:

---

Latex:

1.  b  :  Prog
2.  a  :  Prog
3.  i  :  \mBbbZ{}
4.  i  =  2
5.  p  :  \mBbbN{}
6.  \mneg{}(p  \mmember{}  dl-prop-atoms()  prog(b))
7.  \mneg{}(p  \mmember{}  dl-prop-atoms()  prog(a))
8.  \mforall{}K:Type.  \mforall{}R:\mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}.  \mforall{}P:\mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}.  \mforall{}k:K.    ([|<b>  atm(p)  {}\mRightarrow{}  <a>  atm(p)|]  k)
9.  \mforall{}K:Type.  \mforall{}R:\mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}.  \mforall{}P:\mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}.  \mforall{}k:K.    ([|<a>  atm(p)  {}\mRightarrow{}  <b>  atm(p)|]  k)
10.  K  :  Type
11.  R  :  \mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}
12.  P  :  \mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}
13.  k1  :  K
14.  k2  :  K
15.  \mlambda{}\msubtwo{}a.\mlambda{}s.if  (a  =\msubz{}  p)  then  s  =  k2  else  P  a  s  fi    \mmember{}  \mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}
16.  [|a|]  k1  k2
\mvdash{}  [|a|]  k1  k2


By

---

Latex:
(InstLemma  `dl-prog-sem\_functionality`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}a.\mlambda{}s.if  (a  =\msubz{}  p)
                                                                                                                                then  s  =  k2
                                                                                                                                else  P  a  s
                                                                                                                                fi  \mkleeneclose{};\mkleeneopen{}k1\mkleeneclose{};\mkleeneopen{}k2\mkleeneclose{}]\mcdot{}
  THENA  Auto
  )

---

Home Index