---

Step * 2 of Lemma awf-solution_wf


1. A : Type
2. I : Type
3. G : awf-system{i:l}(I;A)@i'
⊢ TERMOF{unique-awf:o, i:l, i:l} G ∈ {s:I ⟶ awf(A)| 
                                      (∀i:I. ((s i) = (G s i) ∈ awf(A)))
                                      ∧ (∀s':I ⟶ awf(A)
                                           ((∀i:I. ((s' i) = (G s' i) ∈ awf(A))) ⇒ (s' = s ∈ (I ⟶ awf(A)))))} 
BY
{ ((Fold `sq_exists` 0 THEN Auto)
   THEN (DoSubsume THEN Auto)
   THEN GenConclAtAddrType (I1 ⟶ awf(A1)) ⟶ I1 ⟶ awf(A1) [2;1;1]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  I  :  Type
3.  G  :  awf-system\{i:l\}(I;A)@i'
\mvdash{}  TERMOF\{unique-awf:o,  i:l,  i:l\}  G  \mmember{}  \{s:I  {}\mrightarrow{}  awf(A)| 
                                                                            (\mforall{}i:I.  ((s  i)  =  (G  s  i)))
                                                                            \mwedge{}  (\mforall{}s':I  {}\mrightarrow{}  awf(A)
                                                                                      ((\mforall{}i:I.  ((s'  i)  =  (G  s'  i)))  {}\mRightarrow{}  (s'  =  s)))\} 


By

---

Latex:
((Fold  `sq\_exists`  0  THEN  Auto)
  THEN  (DoSubsume  THEN  Auto)
  THEN  GenConclAtAddrType  (I1  {}\mrightarrow{}  awf(A1))  {}\mrightarrow{}  I1  {}\mrightarrow{}  awf(A1)  [2;1;1]\mcdot{}
  THEN  Auto)

---

Home Index