author  huffman 
Mon, 30 Jun 2008 22:16:47 +0200  
changeset 27402  253a06dfadce 
parent 27310  d0229bc6c461 
child 28234  fc420a5cf72e 
permissions  rwrr 
25903  1 
(* Title: HOLCF/Bifinite.thy 
2 
ID: $Id$ 

3 
Author: Brian Huffman 

4 
*) 

5 

6 
header {* Bifinite domains and approximation *} 

7 

8 
theory Bifinite 

27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

9 
imports Deflation 
25903  10 
begin 
11 

26407
562a1d615336
rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite
huffman
parents:
25923
diff
changeset

12 
subsection {* Omegaprofinite and bifinite domains *} 
25903  13 

26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

14 
class profinite = cpo + 
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

15 
fixes approx :: "nat \<Rightarrow> 'a \<rightarrow> 'a" 
27310  16 
assumes chain_approx [simp]: "chain approx" 
26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

17 
assumes lub_approx_app [simp]: "(\<Squnion>i. approx i\<cdot>x) = x" 
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

18 
assumes approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x" 
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

19 
assumes finite_fixes_approx: "finite {x. approx i\<cdot>x = x}" 
25903  20 

26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

21 
class bifinite = profinite + pcpo 
25909
6b96b9392873
add class bifinite_cpo for possiblyunpointed bifinite domains
huffman
parents:
25903
diff
changeset

22 

27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

23 
lemma approx_less: "approx i\<cdot>x \<sqsubseteq> x" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

24 
proof  
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

25 
have "chain (\<lambda>i. approx i\<cdot>x)" by simp 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

26 
hence "approx i\<cdot>x \<sqsubseteq> (\<Squnion>i. approx i\<cdot>x)" by (rule is_ub_thelub) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

27 
thus "approx i\<cdot>x \<sqsubseteq> x" by simp 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

28 
qed 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

29 

253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

30 
lemma finite_deflation_approx: "finite_deflation (approx i)" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

31 
proof 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

32 
fix x :: 'a 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

33 
show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

34 
by (rule approx_idem) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

35 
show "approx i\<cdot>x \<sqsubseteq> x" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

36 
by (rule approx_less) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

37 
show "finite {x. approx i\<cdot>x = x}" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

38 
by (rule finite_fixes_approx) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

39 
qed 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

40 

253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

41 
interpretation approx: finite_deflation ["approx i"] 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

42 
by (rule finite_deflation_approx) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

43 

253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

44 
lemma deflation_approx: "deflation (approx i)" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

45 
by (rule approx.deflation_axioms) 
25903  46 

27186
416d66c36d8f
add lemma finite_image_approx; remove unnecessary sort annotations
huffman
parents:
26962
diff
changeset

47 
lemma lub_approx [simp]: "(\<Squnion>i. approx i) = (\<Lambda> x. x)" 
25903  48 
by (rule ext_cfun, simp add: contlub_cfun_fun) 
49 

27309  50 
lemma approx_strict [simp]: "approx i\<cdot>\<bottom> = \<bottom>" 
25903  51 
by (rule UU_I, rule approx_less) 
52 

53 
lemma approx_approx1: 

27186
416d66c36d8f
add lemma finite_image_approx; remove unnecessary sort annotations
huffman
parents:
26962
diff
changeset

54 
"i \<le> j \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx i\<cdot>x" 
27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

55 
apply (rule deflation_less_comp1 [OF deflation_approx deflation_approx]) 
25922
cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
25909
diff
changeset

56 
apply (erule chain_mono [OF chain_approx]) 
25903  57 
done 
58 

59 
lemma approx_approx2: 

27186
416d66c36d8f
add lemma finite_image_approx; remove unnecessary sort annotations
huffman
parents:
26962
diff
changeset

60 
"j \<le> i \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx j\<cdot>x" 
27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

61 
apply (rule deflation_less_comp2 [OF deflation_approx deflation_approx]) 
25922
cb04d05e95fb
rename lemma chain_mono3 > chain_mono, chain_mono > chain_mono_less
huffman
parents:
25909
diff
changeset

62 
apply (erule chain_mono [OF chain_approx]) 
25903  63 
done 
64 

65 
lemma approx_approx [simp]: 

27186
416d66c36d8f
add lemma finite_image_approx; remove unnecessary sort annotations
huffman
parents:
26962
diff
changeset

66 
"approx i\<cdot>(approx j\<cdot>x) = approx (min i j)\<cdot>x" 
25903  67 
apply (rule_tac x=i and y=j in linorder_le_cases) 
68 
apply (simp add: approx_approx1 min_def) 

69 
apply (simp add: approx_approx2 min_def) 

70 
done 

71 

27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

72 
lemma finite_image_approx: "finite ((\<lambda>x. approx n\<cdot>x) ` A)" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

73 
by (rule approx.finite_image) 
25903  74 

27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

75 
lemma finite_range_approx: "finite (range (\<lambda>x. approx i\<cdot>x))" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

76 
by (rule approx.finite_range) 
27186
416d66c36d8f
add lemma finite_image_approx; remove unnecessary sort annotations
huffman
parents:
26962
diff
changeset

77 

416d66c36d8f
add lemma finite_image_approx; remove unnecessary sort annotations
huffman
parents:
26962
diff
changeset

78 
lemma compact_approx [simp]: "compact (approx n\<cdot>x)" 
27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

79 
by (rule approx.compact) 
25903  80 

27309  81 
lemma profinite_compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x" 
27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

82 
by (rule admD2, simp_all) 
25903  83 

27309  84 
lemma profinite_compact_iff: "compact x \<longleftrightarrow> (\<exists>n. approx n\<cdot>x = x)" 
25903  85 
apply (rule iffI) 
27309  86 
apply (erule profinite_compact_eq_approx) 
25903  87 
apply (erule exE) 
88 
apply (erule subst) 

89 
apply (rule compact_approx) 

90 
done 

91 

92 
lemma approx_induct: 

93 
assumes adm: "adm P" and P: "\<And>n x. P (approx n\<cdot>x)" 

27186
416d66c36d8f
add lemma finite_image_approx; remove unnecessary sort annotations
huffman
parents:
26962
diff
changeset

94 
shows "P x" 
25903  95 
proof  
96 
have "P (\<Squnion>n. approx n\<cdot>x)" 

97 
by (rule admD [OF adm], simp, simp add: P) 

98 
thus "P x" by simp 

99 
qed 

100 

27309  101 
lemma profinite_less_ext: "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y" 
25903  102 
apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> (\<Squnion>i. approx i\<cdot>y)", simp) 
25923  103 
apply (rule lub_mono, simp, simp, simp) 
25903  104 
done 
105 

106 
subsection {* Instance for continuous function space *} 

107 

27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

108 
lemma finite_range_cfun_lemma: 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

109 
assumes a: "finite (range (\<lambda>x. a\<cdot>x))" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

110 
assumes b: "finite (range (\<lambda>y. b\<cdot>y))" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

111 
shows "finite (range (\<lambda>f. \<Lambda> x. b\<cdot>(f\<cdot>(a\<cdot>x))))" (is "finite (range ?h)") 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

112 
proof (rule finite_imageD) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

113 
let ?f = "\<lambda>g. range (\<lambda>x. (a\<cdot>x, g\<cdot>x))" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

114 
show "finite (?f ` range ?h)" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

115 
proof (rule finite_subset) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

116 
let ?B = "Pow (range (\<lambda>x. a\<cdot>x) \<times> range (\<lambda>y. b\<cdot>y))" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

117 
show "?f ` range ?h \<subseteq> ?B" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

118 
by clarsimp 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

119 
show "finite ?B" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

120 
by (simp add: a b) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

121 
qed 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

122 
show "inj_on ?f (range ?h)" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

123 
proof (rule inj_onI, rule ext_cfun, clarsimp) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

124 
fix x f g 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

125 
assume "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) = range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

126 
hence "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) \<subseteq> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

127 
by (rule equalityD1) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

128 
hence "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) \<in> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

129 
by (simp add: subset_eq) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

130 
then obtain y where "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) = (a\<cdot>y, b\<cdot>(g\<cdot>(a\<cdot>y)))" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

131 
by (rule rangeE) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

132 
thus "b\<cdot>(f\<cdot>(a\<cdot>x)) = b\<cdot>(g\<cdot>(a\<cdot>x))" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

133 
by clarsimp 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

134 
qed 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

135 
qed 
25903  136 

26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

137 
instantiation ">" :: (profinite, profinite) profinite 
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

138 
begin 
25903  139 

26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

140 
definition 
25903  141 
approx_cfun_def: 
26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

142 
"approx = (\<lambda>n. \<Lambda> f x. approx n\<cdot>(f\<cdot>(approx n\<cdot>x)))" 
25903  143 

27402
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

144 
instance proof 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

145 
show "chain (approx :: nat \<Rightarrow> ('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow> 'b))" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

146 
unfolding approx_cfun_def by simp 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

147 
next 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

148 
fix x :: "'a \<rightarrow> 'b" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

149 
show "(\<Squnion>i. approx i\<cdot>x) = x" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

150 
unfolding approx_cfun_def 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

151 
by (simp add: lub_distribs eta_cfun) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

152 
next 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

153 
fix i :: nat and x :: "'a \<rightarrow> 'b" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

154 
show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

155 
unfolding approx_cfun_def by simp 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

156 
next 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

157 
fix i :: nat 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

158 
show "finite {x::'a \<rightarrow> 'b. approx i\<cdot>x = x}" 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

159 
apply (rule finite_range_imp_finite_fixes) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

160 
apply (simp add: approx_cfun_def) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

161 
apply (intro finite_range_cfun_lemma finite_range_approx) 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

162 
done 
253a06dfadce
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
huffman
parents:
27310
diff
changeset

163 
qed 
25903  164 

26962
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

165 
end 
c8b20f615d6c
use new class package for classes profinite, bifinite; remove approx class
huffman
parents:
26407
diff
changeset

166 

26407
562a1d615336
rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite
huffman
parents:
25923
diff
changeset

167 
instance ">" :: (profinite, bifinite) bifinite .. 
25909
6b96b9392873
add class bifinite_cpo for possiblyunpointed bifinite domains
huffman
parents:
25903
diff
changeset

168 

25903  169 
lemma approx_cfun: "approx n\<cdot>f\<cdot>x = approx n\<cdot>(f\<cdot>(approx n\<cdot>x))" 
170 
by (simp add: approx_cfun_def) 

171 

172 
end 