Step * 1 1 1 2 1 of Lemma transitive-closure-minimal-uniform


1. Type
2. A ⟶ A ⟶ ℙ
3. A ⟶ A ⟶ ℙ
4. x:A ⟶ y:A ⟶ (x y) ⟶ (x y)
5. : ∀[a,b,c:A].  ((a b)  (b c)  (a c))
6. A
7. A
8. u2 b
9. (a:A × b:A × (R b)) List
10. ∀y,a,b:A.
      (rel_path(A;v;b;y)
       (∀q:a b
            (accumulate (with value and list item y):
              let b,c,r in 
              (F r)
             over list:
               v
             with starting value:
              q) ∈ y)))
11. A
12. a@0 A
13. b@0 A
14. b@0 ∈ A
15. rel_path(A;v;b;y)
16. a@0 b@0
⊢ (F u2) ∈ a@0 b
BY
GenConclAtAddr [2;2] }

1
1. Type
2. A ⟶ A ⟶ ℙ
3. A ⟶ A ⟶ ℙ
4. x:A ⟶ y:A ⟶ (x y) ⟶ (x y)
5. : ∀[a,b,c:A].  ((a b)  (b c)  (a c))
6. A
7. A
8. u2 b
9. (a:A × b:A × (R b)) List
10. ∀y,a,b:A.
      (rel_path(A;v;b;y)
       (∀q:a b
            (accumulate (with value and list item y):
              let b,c,r in 
              (F r)
             over list:
               v
             with starting value:
              q) ∈ y)))
11. A
12. a@0 A
13. b@0 A
14. b@0 ∈ A
15. rel_path(A;v;b;y)
16. a@0 b@0
17. v1 b
18. (F u2) v1 ∈ (a b)
⊢ v1 ∈ a@0 b


Latex:


Latex:

1.  A  :  Type
2.  R  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  Q  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
4.  F  :  x:A  {}\mrightarrow{}  y:A  {}\mrightarrow{}  (x  R  y)  {}\mrightarrow{}  (x  Q  y)
5.  g  :  \mforall{}[a,b,c:A].    ((a  Q  b)  {}\mRightarrow{}  (b  Q  c)  {}\mRightarrow{}  (a  Q  c))
6.  a  :  A
7.  b  :  A
8.  u2  :  R  a  b
9.  v  :  (a:A  \mtimes{}  b:A  \mtimes{}  (R  a  b))  List
10.  \mforall{}y,a,b:A.
            (rel\_path(A;v;b;y)
            {}\mRightarrow{}  (\mforall{}q:a  Q  b
                        (accumulate  (with  value  q  and  list  item  y):
                            let  b,c,r  =  y  in 
                            g  q  (F  b  c  r)
                          over  list:
                              v
                          with  starting  value:
                            q)  \mmember{}  a  Q  y)))
11.  y  :  A
12.  a@0  :  A
13.  b@0  :  A
14.  a  =  b@0
15.  rel\_path(A;v;b;y)
16.  q  :  a@0  Q  b@0
\mvdash{}  g  q  (F  a  b  u2)  \mmember{}  a@0  Q  b


By


Latex:
GenConclAtAddr  [2;2]




Home Index