---

Step * of Lemma dl-sem_functionality1

∀x:dl-Obj()
  ∀[K:Type]. ∀[R:ℕ ⟶ K ⟶ K ⟶ ℙ]. ∀[P,P':ℕ ⟶ K ⟶ ℙ].
    ((∀n∈dl-prop-atoms() x.∀k:K. (P[n] k ⇐⇒ P'[n] k))
    ⇒ dl-same-sem(x;K;dl-sem(K;n.R[n];m.P[m]) x;dl-sem(K;n.R[n];m.P'[m]) x))
BY
{ ((InstLemma `dl-induction` [⌜λ2x.∀[K:Type]. ∀[R:ℕ ⟶ K ⟶ K ⟶ ℙ]. ∀[P,P':ℕ ⟶ K ⟶ ℙ].
                                     ((∀n∈dl-prop-atoms() x.∀k:K. (P[n] k ⇐⇒ P'[n] k))
                                     ⇒ dl-same-sem(x;K;dl-sem(K;n.R[n];m.P[m]) x;dl-sem(K;n.R[n];m.P'[m]) x))⌝]⋅
    THENW Auto
    )
   THEN (Trivial
        ORELSE (Intros
                THEN D 0
                THEN (D 0 THENA Auto)
                THEN Try (((Assert ⌜False⌝⋅ THEN Auto)
                           THEN RW (AddrC [2] (TagC (mk_tag_term 0))) (-1)
                           THEN Complete (Auto)))
                THEN DlSemReduce 0
                THEN Try (Complete (Auto))
                THEN ∀h:hyp. ((InstHyp [⌜K⌝;⌜R⌝;⌜P⌝;⌜P'⌝] h⋅
                               THENA (Auto
                                      THEN OnMaybeHyp 9 (\h. (Unfold `dl-prop-atoms` h
                                                              THEN Reduce h
                                                              THEN Fold `dl-prop-atoms` h
                                                              THEN (Trivial
                                                              ORELSE (RWO "l_all_append" h THEN Complete (Auto))
                                                              )))
                                      )
                               )
                              THEN D -1
                              THEN ((Thin (-2) THEN (D -1 THENA (Computation THEN Fold `member` 0 THEN Auto)))
                              ORELSE (Thin (-1) THEN (D -1 THENA (Computation THEN Fold `member` 0 THEN Auto)))
                              )) 
                THEN All (Folds ``dl-prog-sem dl-prop-sem``)
                THEN Try ((RWO "-1 -2" 0 THEN Auto)))
        )
   ) }

1
1. x : Prog
2. ∀[K:Type]. ∀[R:ℕ ⟶ K ⟶ K ⟶ ℙ]. ∀[P,P':ℕ ⟶ K ⟶ ℙ].
     ((∀n∈dl-prop-atoms() prog(x).∀k:K. (P[n] k ⇐⇒ P'[n] k)) ⇒ dl-same-sem(prog(x);K;[|x|];[|x|]))
3. [K] : Type
4. [R] : ℕ ⟶ K ⟶ K ⟶ ℙ
5. [P] : ℕ ⟶ K ⟶ ℙ
6. [P'] : ℕ ⟶ K ⟶ ℙ
7. (∀n∈dl-prop-atoms() prog((x)*).∀k:K. (P[n] k ⇐⇒ P'[n] k))
8. dl-kind(prog((x)*)) = "prog" ∈ Atom
9. ∀k,k':K.  ([|x|] k k' ⇐⇒ [|x|] k k')
⊢ ∀k,k':K.  (([|x|]^*) k k' ⇐⇒ ([|x|]^*) k k')

2
1. x : ℕ
2. [K] : Type
3. [R] : ℕ ⟶ K ⟶ K ⟶ ℙ
4. [P] : ℕ ⟶ K ⟶ ℙ
5. [P'] : ℕ ⟶ K ⟶ ℙ
6. (∀n∈dl-prop-atoms() prop(atm(x)).∀k:K. (P[n] k ⇐⇒ P'[n] k))
7. dl-kind(prop(atm(x))) = "prop" ∈ Atom
⊢ ∀k:K. (P[x] k ⇐⇒ P'[x] k)

---

Latex:

---

Latex:
\mforall{}x:dl-Obj()
    \mforall{}[K:Type].  \mforall{}[R:\mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[P,P':\mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}].
        ((\mforall{}n\mmember{}dl-prop-atoms()  x.\mforall{}k:K.  (P[n]  k  \mLeftarrow{}{}\mRightarrow{}  P'[n]  k))
        {}\mRightarrow{}  dl-same-sem(x;K;dl-sem(K;n.R[n];m.P[m])  x;dl-sem(K;n.R[n];m.P'[m])  x))


By

---

Latex:
((InstLemma  `dl-induction`  [\mkleeneopen{}\mlambda{}\msubtwo{}x.\mforall{}[K:Type].  \mforall{}[R:\mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[P,P':\mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}].
                                                                      ((\mforall{}n\mmember{}dl-prop-atoms()  x.\mforall{}k:K.  (P[n]  k  \mLeftarrow{}{}\mRightarrow{}  P'[n]  k))
                                                                      {}\mRightarrow{}  dl-same-sem(x;K;dl-sem(K;n.R[n];m.P[m]) 
                                                                                                            x;dl-sem(K;n.R[n];m.P'[m])  x))\mkleeneclose{}]\mcdot{}
    THENW  Auto
    )
  THEN  (Trivial
            ORELSE  (Intros
                            THEN  D  0
                            THEN  (D  0  THENA  Auto)
                            THEN  Try  (((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
                                                  THEN  RW  (AddrC  [2]  (TagC  (mk\_tag\_term  0)))  (-1)
                                                  THEN  Complete  (Auto)))
                            THEN  DlSemReduce  0
                            THEN  Try  (Complete  (Auto))
                            THEN  \mforall{}h:hyp.  ((InstHyp  [\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}P'\mkleeneclose{}]  h\mcdot{}
                                                          THENA  (Auto
                                                                        THEN  OnMaybeHyp  9  (\mbackslash{}h.  (Unfold  `dl-prop-atoms`  h
                                                                                                                        THEN  Reduce  h
                                                                                                                        THEN  Fold  `dl-prop-atoms`  h
                                                                                                                        THEN  (Trivial
                                                                                                                        ORELSE  (RWO  "l\_all\_append"  h
                                                                                                                                        THEN  Complete  (Auto)
                                                                                                                                        )
                                                                                                                        )))
                                                                        )
                                                          )
                                                        THEN  D  -1
                                                        THEN  ((Thin  (-2)
                                                                      THEN  (D  -1  THENA  (Computation  THEN  Fold  `member`  0  THEN  Auto))
                                                                      )
                                                        ORELSE  (Thin  (-1)
                                                                        THEN  (D  -1  THENA  (Computation  THEN  Fold  `member`  0  THEN  Auto))
                                                                        )
                                                        )) 
                            THEN  All  (Folds  ``dl-prog-sem  dl-prop-sem``)
                            THEN  Try  ((RWO  "-1  -2"  0  THEN  Auto)))
            )
  )

---

Home Index