1

(* Generated by FramaC WP *)

2


3

Goal typed_f_reset_post.

4

Hint default,f_reset,property.

5

Proof.

6

(* auto with zarith. *)

7

Qed.

8


9

Goal typed_f_step_assert.

10

Hint f_step,property.

11

Proof.

12

auto with zarith.

13

Qed.

14


15

Goal typed_f_step_assert_2.

16

Hint f_step,property.

17

Proof.

18

(* 

19


20

From 'typed_f_step_post':

21

auto with zarith.

22

*)

23

(* 

24


25

From 'typed_f_step_assert':

26

auto with zarith.

27

*)

28

Qed.

29


30

Goal typed_f_step_assert_3.

31

Hint f_step,property.

32

Proof.

33

(* 

34


35

From 'typed_f_step_post':

36

auto with zarith.

37

*)

38

(* 

39


40

From 'typed_f_step_assert':

41

auto with zarith.

42

*)

43

Qed.

44


45

Goal typed_f_step_assert_4.

46

Hint f_step,property.

47

Proof.

48

(* 

49


50

From 'typed_f_step_post':

51

auto with zarith.

52

*)

53

(* 

54


55

From 'typed_f_step_assert':

56

auto with zarith.

57

*)

58

Qed.

59


60

Goal typed_f_step_assert_5.

61

Hint f_step,property.

62

Proof.

63

(* 

64


65

From 'typed_f_step_post':

66

auto with zarith.

67

*)

68

(* 

69


70

From 'typed_f_step_assert':

71

auto with zarith.

72

*)

73

Qed.

74


75

Goal typed_f_step_assert_6.

76

Hint f_step,property.

77

Proof.

78

(* 

79


80

From 'typed_f_step_post':

81

auto with zarith.

82

*)

83

(* 

84


85

From 'typed_f_step_assert':

86

auto with zarith.

87

*)

88

(* 

89


90

From 'typed_f_step_assert_4':

91

(* 

92


93

From 'typed_f_step_post':

94

auto with zarith.

95

*)

96

(* 

97


98

From 'typed_f_step_assert':

99

auto with zarith.

100

*)

101

*)

102

Qed.

103


104

Goal typed_f_step_post.

105

Hint default,f_step,property.

106

Proof.

107

auto with zarith.

108

Qed.

109


110

Goal typed_g_reset_call_f_reset_pre.

111

Hint g_reset,precondf_reset.

112

Proof.

113

(* auto with zarith. *)

114

Qed.

115


116

Goal typed_g_reset_post.

117

Hint default,g_reset,property.

118

Proof.

119

(* auto with zarith. *)

120

Qed.

121


122

Goal typed_g_step_assert.

123

Hint g_step,property.

124

Proof.

125

auto with zarith.

126

Qed.

127


128

Goal typed_g_step_assert_2.

129

Hint g_step,property.

130

Proof.

131

(* 

132


133

From 'typed_g_step_assert':

134

auto with zarith.

135

*)

136

(* 

137


138

From 'typed_g_step_post':

139

auto with zarith.

140

*)

141

Qed.

142


143

Goal typed_g_step_assert_3.

144

Hint g_step,property.

145

Proof.

146

(* 

147


148

From 'typed_g_step_assert':

149

auto with zarith.

150

*)

151

(* 

152


153

From 'typed_g_step_post':

154

auto with zarith.

155

*)

156

Qed.

157


158

Goal typed_g_step_assert_4.

159

Hint g_step,property.

160

Proof.

161

(* 

162


163

From 'typed_g_step_assert':

164

auto with zarith.

165

*)

166

(* 

167


168

From 'typed_g_step_assert_3':

169

(* 

170


171

From 'typed_g_step_assert':

172

auto with zarith.

173

*)

174

(* 

175


176

From 'typed_g_step_post':

177

auto with zarith.

178

*)

179

*)

180

(* 

181


182

From 'typed_g_step_assert_2':

183

(* 

184


185

From 'typed_g_step_assert':

186

auto with zarith.

187

*)

188

(* 

189


190

From 'typed_g_step_post':

191

auto with zarith.

192

*)

193

*)

194

Qed.

195


196

Goal typed_g_step_assert_5.

197

Hint g_step,property.

198

Proof.

199

(* 

200


201

From 'typed_g_step_assert':

202

auto with zarith.

203

*)

204

(* 

205


206

From 'typed_g_step_assert_3':

207

(* 

208


209

From 'typed_g_step_assert':

210

auto with zarith.

211

*)

212

(* 

213


214

From 'typed_g_step_post':

215

auto with zarith.

216

*)

217

*)

218

(* 

219


220

From 'typed_g_step_assert_2':

221

(* 

222


223

From 'typed_g_step_assert':

224

auto with zarith.

225

*)

226

(* 

227


228

From 'typed_g_step_post':

229

auto with zarith.

230

*)

231

*)

232

Qed.

233


234

Goal typed_g_step_assert_6.

235

Hint g_step,property.

236

Proof.

237

(* 

238


239

From 'typed_g_step_assert':

240

auto with zarith.

241

*)

242

(* 

243


244

From 'typed_g_step_assert_4':

245

(* 

246


247

From 'typed_g_step_assert':

248

auto with zarith.

249

*)

250

(* 

251


252

From 'typed_g_step_assert_3':

253

(* 

254


255

From 'typed_g_step_assert':

256

auto with zarith.

257

*)

258

(* 

259


260

From 'typed_g_step_post':

261

auto with zarith.

262

*)

263

*)

264

(* 

265


266

From 'typed_g_step_assert_2':

267

(* 

268


269

From 'typed_g_step_assert':

270

auto with zarith.

271

*)

272

(* 

273


274

From 'typed_g_step_post':

275

auto with zarith.

276

*)

277

*)

278

*)

279

(* 

280


281

From 'typed_g_step_assert_3':

282

(* 

283


284

From 'typed_g_step_assert':

285

auto with zarith.

286

*)

287

(* 

288


289

From 'typed_g_step_post':

290

auto with zarith.

291

*)

292

*)

293

Qed.

294


295

Goal typed_g_step_assert_7.

296

Hint g_step,property.

297

Proof.

298

(* 

299


300

From 'typed_g_step_assert':

301

auto with zarith.

302

*)

303

(* 

304


305

From 'typed_g_step_assert_4':

306

(* 

307


308

From 'typed_g_step_assert':

309

auto with zarith.

310

*)

311

(* 

312


313

From 'typed_g_step_assert_3':

314

(* 

315


316

From 'typed_g_step_assert':

317

auto with zarith.

318

*)

319

(* 

320


321

From 'typed_g_step_post':

322

auto with zarith.

323

*)

324

*)

325

(* 

326


327

From 'typed_g_step_assert_2':

328

(* 

329


330

From 'typed_g_step_assert':

331

auto with zarith.

332

*)

333

(* 

334


335

From 'typed_g_step_post':

336

auto with zarith.

337

*)

338

*)

339

*)

340

(* 

341


342

From 'typed_g_step_assert_3':

343

(* 

344


345

From 'typed_g_step_assert':

346

auto with zarith.

347

*)

348

(* 

349


350

From 'typed_g_step_post':

351

auto with zarith.

352

*)

353

*)

354

Qed.

355


356

Goal typed_g_step_call_f_step_pre.

357

Hint g_step,precondf_step.

358

Proof.

359

(* auto with zarith. *)

360

Qed.

361


362

Goal typed_g_step_call_f_step_pre_4.

363

Hint g_step,precondf_step.

364

Proof.

365

(* auto with zarith. *)

366

Qed.

367


368

Goal typed_g_step_post.

369

Hint default,g_step,property.

370

Proof.

371

auto with zarith.

372

Qed.

373


374

