lemma nta_ind_rest_cnv (h) (Q:relation4 …):
(∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
(∀G,K,V,W,U.
- â¦\83G,Kâ¦\84 â\8a¢ V :[h,ð\9d\9f\90] W â\86\92 â¬\86*[1] W ≘ U →
+ â¦\83G,Kâ¦\84 â\8a¢ V :[h,ð\9d\9f\90] W â\86\92 â\87§*[1] W ≘ U →
Q G K V W → Q G (K.ⓓV) (#0) U
) →
- (â\88\80G,K,W,U. â¦\83G,Kâ¦\84 â\8a¢ W ![h,ð\9d\9f\90] â\86\92 â¬\86*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
+ (â\88\80G,K,W,U. â¦\83G,Kâ¦\84 â\8a¢ W ![h,ð\9d\9f\90] â\86\92 â\87§*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
(∀I,G,K,W,U,i.
- â¦\83G,Kâ¦\84 â\8a¢ #i :[h,ð\9d\9f\90] W â\86\92 â¬\86*[1] W ≘ U →
+ â¦\83G,Kâ¦\84 â\8a¢ #i :[h,ð\9d\9f\90] W â\86\92 â\87§*[1] W ≘ U →
Q G K (#i) W → Q G (K.ⓘ{I}) (#↑i) U
) →
(∀p,I,G,K,V,T,U.
lemma nta_ind_ext_cnv_mixed (h) (Q:relation4 …):
(∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
(∀G,K,V,W,U.
- â¦\83G,Kâ¦\84 â\8a¢ V :[h,ð\9d\9b\9a] W â\86\92 â¬\86*[1] W ≘ U →
+ â¦\83G,Kâ¦\84 â\8a¢ V :[h,ð\9d\9b\9a] W â\86\92 â\87§*[1] W ≘ U →
Q G K V W → Q G (K.ⓓV) (#0) U
) →
- (â\88\80G,K,W,U. â¦\83G,Kâ¦\84 â\8a¢ W ![h,ð\9d\9b\9a] â\86\92 â¬\86*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
+ (â\88\80G,K,W,U. â¦\83G,Kâ¦\84 â\8a¢ W ![h,ð\9d\9b\9a] â\86\92 â\87§*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
(∀I,G,K,W,U,i.
- â¦\83G,Kâ¦\84 â\8a¢ #i :[h,ð\9d\9b\9a] W â\86\92 â¬\86*[1] W ≘ U →
+ â¦\83G,Kâ¦\84 â\8a¢ #i :[h,ð\9d\9b\9a] W â\86\92 â\87§*[1] W ≘ U →
Q G K (#i) W → Q G (K.ⓘ{I}) (#↑i) U
) →
(∀p,I,G,K,V,T,U.
lemma nta_ind_ext_cnv (h) (Q:relation4 …):
(∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
(∀G,K,V,W,U.
- â¦\83G,Kâ¦\84 â\8a¢ V :[h,ð\9d\9b\9a] W â\86\92 â¬\86*[1] W ≘ U →
+ â¦\83G,Kâ¦\84 â\8a¢ V :[h,ð\9d\9b\9a] W â\86\92 â\87§*[1] W ≘ U →
Q G K V W → Q G (K.ⓓV) (#0) U
) →
- (â\88\80G,K,W,U. â¦\83G,Kâ¦\84 â\8a¢ W ![h,ð\9d\9b\9a] â\86\92 â¬\86*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
+ (â\88\80G,K,W,U. â¦\83G,Kâ¦\84 â\8a¢ W ![h,ð\9d\9b\9a] â\86\92 â\87§*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
(∀I,G,K,W,U,i.
- â¦\83G,Kâ¦\84 â\8a¢ #i :[h,ð\9d\9b\9a] W â\86\92 â¬\86*[1] W ≘ U →
+ â¦\83G,Kâ¦\84 â\8a¢ #i :[h,ð\9d\9b\9a] W â\86\92 â\87§*[1] W ≘ U →
Q G K (#i) W → Q G (K.ⓘ{I}) (#↑i) U
) →
(∀p,I,G,K,V,T,U.