Definition: treeco
`treeco(E) ==  corec(X.lbl:Atom × if lbl =a "leaf" then E if lbl =a "node" then left:X × X else Void fi )`

Lemma: treeco_wf
`∀[E:Type]. (treeco(E) ∈ Type)`

Lemma: treeco-ext
`∀[E:Type]. treeco(E) ≡ lbl:Atom × if lbl =a "leaf" then E if lbl =a "node" then left:treeco(E) × treeco(E) else Void fi `

Definition: treeco_size
`treeco_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "leaf" then 0`
`                   if lbl =a "node" then let left,right = x in (1 + (size left)) + (size right)`
`                   else 0`
`                   fi )) `
`  p`

Lemma: treeco_size_wf
`∀[E:Type]. ∀[p:treeco(E)].  (treeco_size(p) ∈ partial(ℕ))`

Definition: tree
`tree(E) ==  {p:treeco(E)| (treeco_size(p))↓} `

Lemma: tree_wf
`∀[E:Type]. (tree(E) ∈ Type)`

Definition: tree_size
`tree_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "leaf" then 0`
`                   if lbl =a "node" then let left,right = x in (1 + (size left)) + (size right)`
`                   else 0`
`                   fi )) `
`  p`

Lemma: tree_size_wf
`∀[E:Type]. ∀[p:tree(E)].  (tree_size(p) ∈ ℕ)`

Lemma: tree-ext
`∀[E:Type]. tree(E) ≡ lbl:Atom × if lbl =a "leaf" then E if lbl =a "node" then left:tree(E) × tree(E) else Void fi `

Definition: tree_leaf
`tree_leaf(value) ==  <"leaf", value>`

Lemma: tree_leaf_wf
`∀[E:Type]. ∀[value:E].  (tree_leaf(value) ∈ tree(E))`

Definition: tree_node
`tree_node(left;right) ==  <"node", left, right>`

Lemma: tree_node_wf
`∀[E:Type]. ∀[left,right:tree(E)].  (tree_node(left;right) ∈ tree(E))`

Definition: tree_leaf?
`tree_leaf?(v) ==  fst(v) =a "leaf"`

Lemma: tree_leaf?_wf
`∀[E:Type]. ∀[v:tree(E)].  (tree_leaf?(v) ∈ 𝔹)`

Definition: tree_leaf-value
`tree_leaf-value(v) ==  snd(v)`

Lemma: tree_leaf-value_wf
`∀[E:Type]. ∀[v:tree(E)].  tree_leaf-value(v) ∈ E supposing ↑tree_leaf?(v)`

Definition: tree_node?
`tree_node?(v) ==  fst(v) =a "node"`

Lemma: tree_node?_wf
`∀[E:Type]. ∀[v:tree(E)].  (tree_node?(v) ∈ 𝔹)`

Definition: tree_node-left
`tree_node-left(v) ==  fst(snd(v))`

Lemma: tree_node-left_wf
`∀[E:Type]. ∀[v:tree(E)].  tree_node-left(v) ∈ tree(E) supposing ↑tree_node?(v)`

Definition: tree_node-right
`tree_node-right(v) ==  snd(snd(v))`

Lemma: tree_node-right_wf
`∀[E:Type]. ∀[v:tree(E)].  tree_node-right(v) ∈ tree(E) supposing ↑tree_node?(v)`

Lemma: tree-induction
`∀[E:Type]. ∀[P:tree(E) ⟶ ℙ].`
`  ((∀value:E. P[tree_leaf(value)])`
`  `` (∀left,right:tree(E).  (P[left] `` P[right] `` P[tree_node(left;right)]))`
`  `` {∀v:tree(E). P[v]})`

Lemma: tree-definition
`∀[E,A:Type]. ∀[R:A ⟶ tree(E) ⟶ ℙ].`
`  ((∀value:E. {x:A| R[x;tree_leaf(value)]} )`
`  `` (∀left,right:tree(E).  ({x:A| R[x;left]}  `` {x:A| R[x;right]}  `` {x:A| R[x;tree_node(left;right)]} ))`
`  `` {∀v:tree(E). {x:A| R[x;v]} })`

Definition: tree_ind
`tree_ind(v;`
`         tree_leaf(value)`` leaf[value];`
`         tree_node(left,right)`` rec1,rec2.node[left;`
`                                                right;`
`                                                rec1;`
`                                                rec2])  ==`
`  fix((λtree_ind,v. let lbl,v1 = v `
`                    in if lbl="leaf" then leaf[v1]`
`                       if lbl="node"`
`                         then let left,v2 = v1 `
`                              in node[left;`
`                                      v2;`
`                                      tree_ind left;`
`                                      tree_ind v2]`
`                       else Ax`
`                       fi )) `
`  v`

Lemma: tree_ind_wf
`∀[E,A:Type]. ∀[R:A ⟶ tree(E) ⟶ ℙ]. ∀[v:tree(E)]. ∀[leaf:value:E ⟶ {x:A| R[x;tree_leaf(value)]} ].`
`∀[node:left:tree(E) ⟶ right:tree(E) ⟶ {x:A| R[x;left]}  ⟶ {x:A| R[x;right]}  ⟶ {x:A| R[x;tree_node(left;right)]} ].`
`  (tree_ind(v;`
`            tree_leaf(value)`` leaf[value];`
`            tree_node(left,right)`` rec1,rec2.node[left;right;rec1;rec2])  ∈ {x:A| R[x;v]} )`

Lemma: tree_ind_wf_simple
`∀[E,A:Type]. ∀[v:tree(E)]. ∀[leaf:value:E ⟶ A]. ∀[node:left:tree(E) ⟶ right:tree(E) ⟶ A ⟶ A ⟶ A].`
`  (tree_ind(v;`
`            tree_leaf(value)`` leaf[value];`
`            tree_node(left,right)`` rec1,rec2.node[left;right;rec1;rec2])  ∈ A)`

Lemma: tree_subtype_base
`∀[E:Type]. tree(E) ⊆r Base supposing E ⊆r Base`

Lemma: valuetype__tree
`∀[E:Type]. value-type(tree(E))`

Lemma: tree_subtype
`∀[A,B:Type].  tree(A) ⊆r tree(B) supposing A ⊆r B`

Definition: tree-height
`tree-height(t) ==  tree_ind(t; tree_leaf(x)`` 0; tree_node(l,r)`` lh,rh.imax(lh;rh) + 1) `

Lemma: tree-height_wf
`∀[x:Type]. ∀[t:tree(x)].  (tree-height(t) ∈ ℕ)`

Comment: tree_1_end
`********************************`

Definition: bs_treeco
`bs_treeco(E) ==`
`  corec(X.lbl:Atom × if lbl =a "null" then Unit`
`                     if lbl =a "leaf" then E`
`                     if lbl =a "node" then left:X × value:E × X`
`                     else Void`
`                     fi )`

Lemma: bs_treeco_wf
`∀[E:Type]. (bs_treeco(E) ∈ Type)`

Lemma: bs_treeco-ext
`∀[E:Type]`
`  bs_treeco(E) ≡ lbl:Atom × if lbl =a "null" then Unit`
`                            if lbl =a "leaf" then E`
`                            if lbl =a "node" then left:bs_treeco(E) × value:E × bs_treeco(E)`
`                            else Void`
`                            fi `

Definition: bs_treeco_size
`bs_treeco_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "null" then 0`
`                   if lbl =a "leaf" then 0`
`                   if lbl =a "node" then 1 + (size (fst(x))) + (size (snd(snd(x))))`
`                   else 0`
`                   fi )) `
`  p`

Lemma: bs_treeco_size_wf
`∀[E:Type]. ∀[p:bs_treeco(E)].  (bs_treeco_size(p) ∈ partial(ℕ))`

Definition: bs_tree
`bs_tree(E) ==  {p:bs_treeco(E)| (bs_treeco_size(p))↓} `

Lemma: bs_tree_wf
`∀[E:Type]. (bs_tree(E) ∈ Type)`

Definition: bs_tree_size
`bs_tree_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "null" then 0`
`                   if lbl =a "leaf" then 0`
`                   if lbl =a "node" then 1 + (size (fst(x))) + (size (snd(snd(x))))`
`                   else 0`
`                   fi )) `
`  p`

Lemma: bs_tree_size_wf
`∀[E:Type]. ∀[p:bs_tree(E)].  (bs_tree_size(p) ∈ ℕ)`

Lemma: bs_tree-ext
`∀[E:Type]`
`  bs_tree(E) ≡ lbl:Atom × if lbl =a "null" then Unit`
`                          if lbl =a "leaf" then E`
`                          if lbl =a "node" then left:bs_tree(E) × value:E × bs_tree(E)`
`                          else Void`
`                          fi `

Definition: bst_null
`bst_null() ==  <"null", ⋅>`

Lemma: bst_null_wf
`∀[E:Type]. (bst_null() ∈ bs_tree(E))`

Definition: bst_leaf
`bst_leaf(value) ==  <"leaf", value>`

Lemma: bst_leaf_wf
`∀[E:Type]. ∀[value:E].  (bst_leaf(value) ∈ bs_tree(E))`

Definition: bst_node
`bst_node(left;value;right) ==  <"node", left, value, right>`

Lemma: bst_node_wf
`∀[E:Type]. ∀[left:bs_tree(E)]. ∀[value:E]. ∀[right:bs_tree(E)].  (bst_node(left;value;right) ∈ bs_tree(E))`

Definition: bst_null?
`bst_null?(v) ==  fst(v) =a "null"`

Lemma: bst_null?_wf
`∀[E:Type]. ∀[v:bs_tree(E)].  (bst_null?(v) ∈ 𝔹)`

Definition: bst_leaf?
`bst_leaf?(v) ==  fst(v) =a "leaf"`

Lemma: bst_leaf?_wf
`∀[E:Type]. ∀[v:bs_tree(E)].  (bst_leaf?(v) ∈ 𝔹)`

Definition: bst_leaf-value
`bst_leaf-value(v) ==  snd(v)`

Lemma: bst_leaf-value_wf
`∀[E:Type]. ∀[v:bs_tree(E)].  bst_leaf-value(v) ∈ E supposing ↑bst_leaf?(v)`

Definition: bst_node?
`bst_node?(v) ==  fst(v) =a "node"`

Lemma: bst_node?_wf
`∀[E:Type]. ∀[v:bs_tree(E)].  (bst_node?(v) ∈ 𝔹)`

Definition: bst_node-left
`bst_node-left(v) ==  fst(snd(v))`

Lemma: bst_node-left_wf
`∀[E:Type]. ∀[v:bs_tree(E)].  bst_node-left(v) ∈ bs_tree(E) supposing ↑bst_node?(v)`

Definition: bst_node-value
`bst_node-value(v) ==  fst(snd(snd(v)))`

Lemma: bst_node-value_wf
`∀[E:Type]. ∀[v:bs_tree(E)].  bst_node-value(v) ∈ E supposing ↑bst_node?(v)`

Definition: bst_node-right
`bst_node-right(v) ==  snd(snd(snd(v)))`

Lemma: bst_node-right_wf
`∀[E:Type]. ∀[v:bs_tree(E)].  bst_node-right(v) ∈ bs_tree(E) supposing ↑bst_node?(v)`

Lemma: bs_tree-induction
`∀[E:Type]. ∀[P:bs_tree(E) ⟶ ℙ].`
`  (P[bst_null()]`
`  `` (∀value:E. P[bst_leaf(value)])`
`  `` (∀left:bs_tree(E). ∀value:E. ∀right:bs_tree(E).  (P[left] `` P[right] `` P[bst_node(left;value;right)]))`
`  `` {∀v:bs_tree(E). P[v]})`

Lemma: bs_tree-definition
`∀[E,A:Type]. ∀[R:A ⟶ bs_tree(E) ⟶ ℙ].`
`  ({x:A| R[x;bst_null()]} `
`  `` (∀value:E. {x:A| R[x;bst_leaf(value)]} )`
`  `` (∀left:bs_tree(E). ∀value:E. ∀right:bs_tree(E).`
`        ({x:A| R[x;left]}  `` {x:A| R[x;right]}  `` {x:A| R[x;bst_node(left;value;right)]} ))`
`  `` {∀v:bs_tree(E). {x:A| R[x;v]} })`

Definition: bs_tree_ind
`case(v)`
`null=>null`
`leaf(value)=>leaf[value]`
`node(left,value,right)=>rec1,rec2.node[left;`
`                                       value;`
`                                       right;`
`                                       rec1;`
`                                       rec2] ==`
`  fix((λbs_tree_ind,v. let lbl,v1 = v `
`                       in if lbl="null" then null`
`                          if lbl="leaf" then leaf[v1]`
`                          if lbl="node"`
`                            then let left,v2 = v1 `
`                                 in let value,v3 = v2 `
`                                    in node[left;`
`                                            value;`
`                                            v3;`
`                                            bs_tree_ind left;`
`                                            bs_tree_ind v3]`
`                          else Ax`
`                          fi )) `
`  v`

Lemma: bs_tree_ind_wf
`∀[E,A:Type]. ∀[R:A ⟶ bs_tree(E) ⟶ ℙ]. ∀[v:bs_tree(E)]. ∀[null:{x:A| R[x;bst_null()]} ].`
`∀[leaf:value:E ⟶ {x:A| R[x;bst_leaf(value)]} ]. ∀[node:left:bs_tree(E)`
`                                                       ⟶ value:E`
`                                                       ⟶ right:bs_tree(E)`
`                                                       ⟶ {x:A| R[x;left]} `
`                                                       ⟶ {x:A| R[x;right]} `
`                                                       ⟶ {x:A| R[x;bst_node(left;value;right)]} ].`
`  (case(v)`
`   null=>null`
`   leaf(value)=>leaf[value]`
`   node(left,value,right)=>rec1,rec2.node[left;value;right;rec1;rec2] ∈ {x:A| R[x;v]} )`

Lemma: bs_tree_ind_wf_simple
`∀[E,A:Type]. ∀[v:bs_tree(E)]. ∀[null:A]. ∀[leaf:value:E ⟶ A]. ∀[node:left:bs_tree(E)`
`                                                                      ⟶ value:E`
`                                                                      ⟶ right:bs_tree(E)`
`                                                                      ⟶ A`
`                                                                      ⟶ A`
`                                                                      ⟶ A].`
`  (case(v)`
`   null=>null`
`   leaf(value)=>leaf[value]`
`   node(left,value,right)=>rec1,rec2.node[left;value;right;rec1;rec2] ∈ A)`

Definition: member_bs_tree
`x ∈ tr ==  case(tr)null=>Falseleaf(v)=>v = x ∈ Enode(a,v,b)=>mema,memb.(v = x ∈ E) ∨ mema ∨ memb`

Lemma: member_bs_tree_wf
`∀[E:Type]. ∀[x:E]. ∀[tr:bs_tree(E)].  (x ∈ tr ∈ ℙ)`

Definition: bs_tree_ordered
`bs_tree_ordered(E;cmp;tr) ==`
`  case(tr)`
`  null=>True`
`  leaf(v)=>True`
`  node(a,v,b)=>oa,ob.oa ∧ ob ∧ (∀x:E. (x ∈ a `` 0 < cmp x v)) ∧ (∀x:E. (x ∈ b `` 0 < cmp v x))`

Lemma: bs_tree_ordered_wf
`∀[E:Type]. ∀[cmp:comparison(E)]. ∀[tr:bs_tree(E)].  (bs_tree_ordered(E;cmp;tr) ∈ ℙ)`

Lemma: sq_stable__bs_tree_ordered
`∀[E:Type]. ∀cmp:comparison(E). ∀tr:bs_tree(E).  SqStable(bs_tree_ordered(E;cmp;tr))`

Definition: ordered_bs_tree
`ordered_bs_tree(E;cmp) ==  {tr:bs_tree(E)| bs_tree_ordered(E;cmp;tr)} `

Lemma: ordered_bs_tree_wf
`∀[E:Type]. ∀[cmp:comparison(E)].  (ordered_bs_tree(E;cmp) ∈ Type)`

Definition: bs_tree_insert
`bs_tree_insert(cmp;x;tr) ==`
`  case(tr)`
`  null=>bst_leaf(x)`
`  leaf(v)=>eval c = cmp v x in`
`           if (0) < (c)`
`              then bst_node(bst_leaf(v);x;bst_null())`
`              else if (c) < (0)  then bst_node(bst_null();x;bst_leaf(v))  else bst_leaf(x)`
`  node(l,v,r)=>a,b.eval c = cmp v x in`
`                   if (0) < (c)  then bst_node(l;v;b)  else if (c) < (0)  then bst_node(a;v;r)  else bst_node(l;x;r)`

Lemma: bs_tree_insert_wf1
`∀[E:Type]. ∀[cmp:comparison(E)]. ∀[x:E]. ∀[tr:bs_tree(E)].  (bs_tree_insert(cmp;x;tr) ∈ bs_tree(E))`

Lemma: member_bs_tree_insert
`∀[E:Type]`
`  ∀cmp:comparison(E). ∀x:E. ∀tr:ordered_bs_tree(E;cmp). ∀y:E.`
`    (y ∈ bs_tree_insert(cmp;x;tr) `⇐⇒` (y = x ∈ E) ∨ (y ∈ tr ∧ (¬((cmp x y) = 0 ∈ ℤ))))`

Lemma: bs_tree_insert_wf
`∀[E:Type]. ∀[cmp:comparison(E)]. ∀[x:E]. ∀[tr:ordered_bs_tree(E;cmp)].`
`  (bs_tree_insert(cmp;x;tr) ∈ ordered_bs_tree(E;cmp))`

Definition: bs_tree_max
`bs_tree_max(tr;d) ==`
`  case(tr)`
`  null=><d, bst_null()>`
`  leaf(v)=><v, bst_null()>`
`  node(a,v,b)=>ma,mb.if bst_null?(b) then <v, a> else let m,b' = mb in <m, bst_node(a;v;b')> fi `

Lemma: bs_tree_max_wf1
`∀[E:Type]. ∀[tr:bs_tree(E)]. ∀[d:E].  (bs_tree_max(tr;d) ∈ E × bs_tree(E))`

Lemma: member-bs_tree_max
`∀[E:Type]`
`  ∀tr:bs_tree(E). ∀d,z:E.`
`    ((z ∈ snd(bs_tree_max(tr;d)) ∨ (z = (fst(bs_tree_max(tr;d))) ∈ E)) `` (z ∈ tr ∨ ((↑bst_null?(tr)) ∧ (z = d ∈ E))))`

Lemma: bs_tree_max_wf
`∀[E:Type]. ∀[cmp:comparison(E)]. ∀[tr:ordered_bs_tree(E;cmp)]. ∀[d:E].`
`  (bs_tree_max(tr;d) ∈ {p:E × ordered_bs_tree(E;cmp)| `
`                        let m,t = p `
`                        in (∀x:E. (x ∈ tr `` (x ∈ t ∨ (x = m ∈ E))))`
`                           ∧ ((¬↑bst_null?(tr)) `` m ∈ tr)`
`                           ∧ (∀x:E. (x ∈ t `` (x ∈ tr ∧ 0 < cmp x m)))} )`

Definition: bs_tree_delete
`bs_tree_delete(cmp;x;tr) ==`
`  case(tr)`
`  null=>bst_null()`
`  leaf(v)=>if (cmp x v =z 0) then bst_null() else bst_leaf(v) fi `
`  node(a,v,b)=>da,db.if (0) < (cmp x v)`
`                        then bst_node(da;v;b)`
`                        else if (0) < (cmp v x)`
`                                then bst_node(a;v;db)`
`                                else if bst_null?(a) then b else let m,a' = bs_tree_max(a;v) in bst_node(a';m;b) fi `

Lemma: bs_tree_delete_wf1
`∀[E:Type]. ∀[cmp:comparison(E)]. ∀[x:E]. ∀[tr:bs_tree(E)].  (bs_tree_delete(cmp;x;tr) ∈ bs_tree(E))`

Lemma: member-bs_tree_delete-implies
`∀[E:Type]. ∀cmp:comparison(E). ∀x:E. ∀tr:bs_tree(E). ∀z:E.  (z ∈ bs_tree_delete(cmp;x;tr) `` z ∈ tr)`

Lemma: bs_tree_delete_wf
`∀[E:Type]. ∀[cmp:comparison(E)]. ∀[x:E]. ∀[tr:ordered_bs_tree(E;cmp)].`
`  (bs_tree_delete(cmp;x;tr) ∈ ordered_bs_tree(E;cmp))`

Lemma: sq_stable__member_bs_tree
`∀[E:Type]. ∀cmp:comparison(E). ∀x:E. ∀tr:ordered_bs_tree(E;cmp).  SqStable(x ∈ tr)`

Lemma: member-bs_tree_delete
`∀[E:Type]`
`  ∀cmp:comparison(E). ∀x:E. ∀tr:ordered_bs_tree(E;cmp). ∀z:E.`
`    (z ∈ bs_tree_delete(cmp;x;tr) `⇐⇒` z ∈ tr ∧ (¬((cmp z x) = 0 ∈ ℤ)))`

Definition: bs_tree_lookup
`bs_tree_lookup(cmp;x;tr) ==`
`  case(tr)`
`  null=>inr ⋅ `
`  leaf(v)=>if (cmp v x =z 0) then inl v else inr ⋅  fi `
`  node(a,v,b)=>la,lb.eval c = cmp v x in`
`                     if (c) < (0)  then la  else if (0) < (c)  then lb  else (inl v)`

Lemma: bs_tree_lookup_wf1
`∀[E:Type]. ∀[cmp:comparison(E)]. ∀[x:E]. ∀[tr:bs_tree(E)].  (bs_tree_lookup(cmp;x;tr) ∈ E?)`

Lemma: bs_tree_lookup_wf
`∀[E:Type]. ∀[cmp:comparison(E)]. ∀[x:E]. ∀[tr:ordered_bs_tree(E;cmp)].`
`  (bs_tree_lookup(cmp;x;tr) ∈ (∃z:E [(((cmp z x) = 0 ∈ ℤ) ∧ z ∈ tr)]) ∨ (↓∀z:E. (z ∈ tr `` (¬((cmp z x) = 0 ∈ ℤ)))))`

Definition: test-Spec
`test-Spec() ==`
`  [<"prog", [<"aprog", [inr Atom ]>; <"iterate", [inl inl "foo"]>; <"test", [inl inl "prop"]>]>;`
`   <"foo", [<"afoo", [inr Atom ]>; <"bar", [inl inl "foo"]>; <"xx", [inl inl "prop"; inl inl "prog"]>]>;`
`   <"prop", [<"aprop", [inr Atom ]>; <"false", [inr Unit ]>; <"implies", [inl inl "prop"; inl inl "prop"]>; <"box", [inl\000C inl "prog"; inl inl "prop"]>; <"diamond", [inl inl "foo"; inl inl "prop"]>]>]`

Lemma: test-Spec_wf
`test-Spec() ∈ MutualRectypeSpec`

Definition: test-Obj
`test-Obj() ==  mobj(test-Spec())`

Lemma: test-Obj_wf
`test-Obj() ∈ Type`

Definition: test-prog
`test-prog() ==  mrec(test-Spec();"prog")`

Lemma: test-prog_wf
`test-prog() ∈ Type`

Definition: test-foo
`test-foo() ==  mrec(test-Spec();"foo")`

Lemma: test-foo_wf
`test-foo() ∈ Type`

Definition: test-prop
`test-prop() ==  mrec(test-Spec();"prop")`

Lemma: test-prop_wf
`test-prop() ∈ Type`

Definition: test-prog-obj
`test-prog-obj(x) ==  <"prog", x>`

Lemma: test-prog-obj_wf
`∀x:test-prog(). (test-prog-obj(x) ∈ test-Obj())`

Definition: test-foo-obj
`test-foo-obj(x) ==  <"foo", x>`

Lemma: test-foo-obj_wf
`∀x:test-foo(). (test-foo-obj(x) ∈ test-Obj())`

Definition: test-prop-obj
`test-prop-obj(x) ==  <"prop", x>`

Lemma: test-prop-obj_wf
`∀x:test-prop(). (test-prop-obj(x) ∈ test-Obj())`

Definition: test-aprog
`test-aprog(x) ==  mk-prec("aprog";x)`

Lemma: test-aprog_wf
`∀[x:Atom]. (test-aprog(x) ∈ test-prog())`

Definition: test-iterate
`test-iterate(x) ==  mk-prec("iterate";x)`

Lemma: test-iterate_wf
`∀[x:test-foo()]. (test-iterate(x) ∈ test-prog())`

Definition: test-test
`test-test(x) ==  mk-prec("test";x)`

Lemma: test-test_wf
`∀[x:test-prop()]. (test-test(x) ∈ test-prog())`

Definition: test-afoo
`test-afoo(x) ==  mk-prec("afoo";x)`

Lemma: test-afoo_wf
`∀[x:Atom]. (test-afoo(x) ∈ test-foo())`

Definition: test-bar
`test-bar(x) ==  mk-prec("bar";x)`

Lemma: test-bar_wf
`∀[x:test-foo()]. (test-bar(x) ∈ test-foo())`

Definition: test-xx
`test-xx(x1;x) ==  mk-prec("xx";<x1, x>)`

Lemma: test-xx_wf
`∀[x1:test-prop()]. ∀[x:test-prog()].  (test-xx(x1;x) ∈ test-foo())`

Definition: test-aprop
`test-aprop(x) ==  mk-prec("aprop";x)`

Lemma: test-aprop_wf
`∀[x:Atom]. (test-aprop(x) ∈ test-prop())`

Definition: test-false
`test-false() ==  mk-prec("false";Ax)`

Lemma: test-false_wf
`test-false() ∈ test-prop()`

Definition: test-implies
`test-implies(x1;x) ==  mk-prec("implies";<x1, x>)`

Lemma: test-implies_wf
`∀[x1,x:test-prop()].  (test-implies(x1;x) ∈ test-prop())`

Definition: test-box
`test-box(x1;x) ==  mk-prec("box";<x1, x>)`

Lemma: test-box_wf
`∀[x1:test-prog()]. ∀[x:test-prop()].  (test-box(x1;x) ∈ test-prop())`

Definition: test-diamond
`test-diamond(x1;x) ==  mk-prec("diamond";<x1, x>)`

Lemma: test-diamond_wf
`∀[x1:test-foo()]. ∀[x:test-prop()].  (test-diamond(x1;x) ∈ test-prop())`

Definition: test-kind
`test-kind(d) ==  mobj-kind(d)`

Lemma: test-kind_wf
`∀[d:test-Obj()]. (test-kind(d) ∈ {a:Atom| (a ∈ ``prog foo prop``)} )`

Definition: test-label
`test-label(d) ==  mobj-label(d)`

Lemma: test-label_wf
`∀[d:test-Obj()]. (test-label(d) ∈ Atom)`

Definition: test-aprog?
`test-aprog?(x) ==  test-label(test-prog-obj(x)) =a "aprog"`

Lemma: test-aprog?_wf
`∀[x:test-prog()]. (test-aprog?(x) ∈ 𝔹)`

Definition: test-iterate?
`test-iterate?(x) ==  test-label(test-prog-obj(x)) =a "iterate"`

Lemma: test-iterate?_wf
`∀[x:test-prog()]. (test-iterate?(x) ∈ 𝔹)`

Definition: test-test?
`test-test?(x) ==  test-label(test-prog-obj(x)) =a "test"`

Lemma: test-test?_wf
`∀[x:test-prog()]. (test-test?(x) ∈ 𝔹)`

Definition: test-afoo?
`test-afoo?(x) ==  test-label(test-foo-obj(x)) =a "afoo"`

Lemma: test-afoo?_wf
`∀[x:test-foo()]. (test-afoo?(x) ∈ 𝔹)`

Definition: test-bar?
`test-bar?(x) ==  test-label(test-foo-obj(x)) =a "bar"`

Lemma: test-bar?_wf
`∀[x:test-foo()]. (test-bar?(x) ∈ 𝔹)`

Definition: test-xx?
`test-xx?(x) ==  test-label(test-foo-obj(x)) =a "xx"`

Lemma: test-xx?_wf
`∀[x:test-foo()]. (test-xx?(x) ∈ 𝔹)`

Definition: test-aprop?
`test-aprop?(x) ==  test-label(test-prop-obj(x)) =a "aprop"`

Lemma: test-aprop?_wf
`∀[x:test-prop()]. (test-aprop?(x) ∈ 𝔹)`

Definition: test-false?
`test-false?(x) ==  test-label(test-prop-obj(x)) =a "false"`

Lemma: test-false?_wf
`∀[x:test-prop()]. (test-false?(x) ∈ 𝔹)`

Definition: test-implies?
`test-implies?(x) ==  test-label(test-prop-obj(x)) =a "implies"`

Lemma: test-implies?_wf
`∀[x:test-prop()]. (test-implies?(x) ∈ 𝔹)`

Definition: test-box?
`test-box?(x) ==  test-label(test-prop-obj(x)) =a "box"`

Lemma: test-box?_wf
`∀[x:test-prop()]. (test-box?(x) ∈ 𝔹)`

Definition: test-diamond?
`test-diamond?(x) ==  test-label(test-prop-obj(x)) =a "diamond"`

Lemma: test-diamond?_wf
`∀[x:test-prop()]. (test-diamond?(x) ∈ 𝔹)`

Definition: test-aprog-1
`test-aprog-1(x) ==  snd(x).0`

Lemma: test-aprog-1_wf
`∀[x:test-prog()]. test-aprog-1(x) ∈ Atom supposing ↑test-aprog?(x)`

Definition: test-iterate-1
`test-iterate-1(x) ==  snd(x).0`

Lemma: test-iterate-1_wf
`∀[x:test-prog()]. test-iterate-1(x) ∈ test-foo() supposing ↑test-iterate?(x)`

Definition: test-test-1
`test-test-1(x) ==  snd(x).0`

Lemma: test-test-1_wf
`∀[x:test-prog()]. test-test-1(x) ∈ test-prop() supposing ↑test-test?(x)`

Definition: test-afoo-1
`test-afoo-1(x) ==  snd(x).0`

Lemma: test-afoo-1_wf
`∀[x:test-foo()]. test-afoo-1(x) ∈ Atom supposing ↑test-afoo?(x)`

Definition: test-bar-1
`test-bar-1(x) ==  snd(x).0`

Lemma: test-bar-1_wf
`∀[x:test-foo()]. test-bar-1(x) ∈ test-foo() supposing ↑test-bar?(x)`

Definition: test-xx-1
`test-xx-1(x) ==  snd(x).0`

Lemma: test-xx-1_wf
`∀[x:test-foo()]. test-xx-1(x) ∈ test-prop() supposing ↑test-xx?(x)`

Definition: test-xx-2
`test-xx-2(x) ==  snd(x).1`

Lemma: test-xx-2_wf
`∀[x:test-foo()]. test-xx-2(x) ∈ test-prog() supposing ↑test-xx?(x)`

Definition: test-aprop-1
`test-aprop-1(x) ==  snd(x).0`

Lemma: test-aprop-1_wf
`∀[x:test-prop()]. test-aprop-1(x) ∈ Atom supposing ↑test-aprop?(x)`

Definition: test-implies-1
`test-implies-1(x) ==  snd(x).0`

Lemma: test-implies-1_wf
`∀[x:test-prop()]. test-implies-1(x) ∈ test-prop() supposing ↑test-implies?(x)`

Definition: test-implies-2
`test-implies-2(x) ==  snd(x).1`

Lemma: test-implies-2_wf
`∀[x:test-prop()]. test-implies-2(x) ∈ test-prop() supposing ↑test-implies?(x)`

Definition: test-box-1
`test-box-1(x) ==  snd(x).0`

Lemma: test-box-1_wf
`∀[x:test-prop()]. test-box-1(x) ∈ test-prog() supposing ↑test-box?(x)`

Definition: test-box-2
`test-box-2(x) ==  snd(x).1`

Lemma: test-box-2_wf
`∀[x:test-prop()]. test-box-2(x) ∈ test-prop() supposing ↑test-box?(x)`

Definition: test-diamond-1
`test-diamond-1(x) ==  snd(x).0`

Lemma: test-diamond-1_wf
`∀[x:test-prop()]. test-diamond-1(x) ∈ test-foo() supposing ↑test-diamond?(x)`

Definition: test-diamond-2
`test-diamond-2(x) ==  snd(x).1`

Lemma: test-diamond-2_wf
`∀[x:test-prop()]. test-diamond-2(x) ∈ test-prop() supposing ↑test-diamond?(x)`

Lemma: test-induction
`∀[T:test-Obj() ⟶ TYPE]`
`  ((∀x:Atom. T[test-prog-obj(test-aprog(x))])`
`  `` (∀x:test-foo(). (T[test-foo-obj(x)] `` T[test-prog-obj(test-iterate(x))]))`
`  `` (∀x:test-prop(). (T[test-prop-obj(x)] `` T[test-prog-obj(test-test(x))]))`
`  `` (∀x:Atom. T[test-foo-obj(test-afoo(x))])`
`  `` (∀x:test-foo(). (T[test-foo-obj(x)] `` T[test-foo-obj(test-bar(x))]))`
`  `` (∀x:test-prop(). ∀x1:test-prog().  (T[test-prop-obj(x)] `` T[test-prog-obj(x1)] `` T[test-foo-obj(test-xx(x;x1))]))`
`  `` (∀x:Atom. T[test-prop-obj(test-aprop(x))])`
`  `` T[test-prop-obj(test-false())]`
`  `` (∀x,x1:test-prop().  (T[test-prop-obj(x)] `` T[test-prop-obj(x1)] `` T[test-prop-obj(test-implies(x;x1))]))`
`  `` (∀x:test-prog(). ∀x1:test-prop().`
`        (T[test-prog-obj(x)] `` T[test-prop-obj(x1)] `` T[test-prop-obj(test-box(x;x1))]))`
`  `` (∀x:test-foo(). ∀x1:test-prop().`
`        (T[test-foo-obj(x)] `` T[test-prop-obj(x1)] `` T[test-prop-obj(test-diamond(x;x1))]))`
`  `` (∀x:test-Obj(). T[x]))`

Definition: test-ind
`test-ind(`
`         test-aprog(x0)`` aprog[x0];`
`         test-iterate(x1)`` x2.iterate[x1; x2];`
`         test-test(x3)`` x4.test[x3; x4];`
`         test-afoo(x5)`` afoo[x5];`
`         test-bar(x6)`` x7.bar[x6; x7];`
`         test-xx(x8,x9)`` x10,x11.xx[x8;`
`                                     x9;`
`                                     x10;`
`                                     x11];`
`         test-aprop(x12)`` aprop[x12];`
`         test-false`` false;`
`         test-implies(x13,x14)`` x15,x16.implies[x13;`
`                                                 x14;`
`                                                 x15;`
`                                                 x16];`
`         test-box(x17,x18)`` x19,x20.box[x17;`
`                                         x18;`
`                                         x19;`
`                                         x20];`
`         test-diamond(x21,x22)`` x23,x24.diamond[x21;`
`                                                 x22;`
`                                                 x23;`
`                                                 x24])  ==`
`  TERMOF{test-induction:o, 1:l} (λx0.aprog[x0]) (λx1,x2. iterate[x1; x2]) (λx3,x4. test[x3; x4]) (λx5.afoo[x5]) (λx6,x7.\000C bar[x6; x7]) `
`  (λx8,x9,x10,x11. xx[x8;`
`                      x9;`
`                      x10;`
`                      x11]) `
`  (λx12.aprop[x12]) `
`  false `
`  (λx13,x14,x15,x16. implies[x13;`
`                             x14;`
`                             x15;`
`                             x16]) `
`  (λx17,x18,x19,x20. box[x17;`
`                         x18;`
`                         x19;`
`                         x20]) `
`  (λx21,x22,x23,x24. diamond[x21;`
`                             x22;`
`                             x23;`
`                             x24])`

Lemma: test-ind_wf
`∀[T:test-Obj() ⟶ TYPE]. ∀[aprog:x:Atom ⟶ T[test-prog-obj(test-aprog(x))]].`
`∀[iterate:x:test-foo() ⟶ T[test-foo-obj(x)] ⟶ T[test-prog-obj(test-iterate(x))]].`
`∀[test:x:test-prop() ⟶ T[test-prop-obj(x)] ⟶ T[test-prog-obj(test-test(x))]].`
`∀[afoo:x:Atom ⟶ T[test-foo-obj(test-afoo(x))]]. ∀[bar:x:test-foo()`
`                                                       ⟶ T[test-foo-obj(x)]`
`                                                       ⟶ T[test-foo-obj(test-bar(x))]].`
`∀[xx:x:test-prop() ⟶ x1:test-prog() ⟶ T[test-prop-obj(x)] ⟶ T[test-prog-obj(x1)] ⟶ T[test-foo-obj(test-xx(x;x1))]].`
`∀[aprop:x:Atom ⟶ T[test-prop-obj(test-aprop(x))]]. ∀[false:T[test-prop-obj(test-false())]].`
`∀[implies:x:test-prop()`
`          ⟶ x1:test-prop()`
`          ⟶ T[test-prop-obj(x)]`
`          ⟶ T[test-prop-obj(x1)]`
`          ⟶ T[test-prop-obj(test-implies(x;x1))]]. ∀[box:x:test-prog()`
`                                                          ⟶ x1:test-prop()`
`                                                          ⟶ T[test-prog-obj(x)]`
`                                                          ⟶ T[test-prop-obj(x1)]`
`                                                          ⟶ T[test-prop-obj(test-box(x;x1))]].`
`∀[diamond:x:test-foo()`
`          ⟶ x1:test-prop()`
`          ⟶ T[test-foo-obj(x)]`
`          ⟶ T[test-prop-obj(x1)]`
`          ⟶ T[test-prop-obj(test-diamond(x;x1))]].`
`  (test-ind(`
`            test-aprog(x0)`` aprog[x0];`
`            test-iterate(x1)`` x2.iterate[x1;x2];`
`            test-test(x3)`` x4.test[x3;x4];`
`            test-afoo(x5)`` afoo[x5];`
`            test-bar(x6)`` x7.bar[x6;x7];`
`            test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`            test-aprop(x12)`` aprop[x12];`
`            test-false`` false;`
`            test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;x16];`
`            test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`            test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;x24])  ∈ ∀x:test-Obj(). T[x])`

Lemma: test-ind_wf_definition
`∀[A,B,C:TYPE]. ∀[aprog:x:Atom ⟶ A]. ∀[iterate:x:test-foo() ⟶ B ⟶ A]. ∀[test:x:test-prop() ⟶ C ⟶ A].`
`∀[afoo:x:Atom ⟶ B]. ∀[bar:x:test-foo() ⟶ B ⟶ B]. ∀[xx:x:test-prop() ⟶ x1:test-prog() ⟶ C ⟶ A ⟶ B]. ∀[aprop:x:Atom`
`                                                                                                                  ⟶ C].`
`∀[false:C]. ∀[implies:x:test-prop() ⟶ x1:test-prop() ⟶ C ⟶ C ⟶ C]. ∀[box:x:test-prog()`
`                                                                             ⟶ x1:test-prop()`
`                                                                             ⟶ A`
`                                                                             ⟶ C`
`                                                                             ⟶ C]. ∀[diamond:x:test-foo()`
`                                                                                              ⟶ x1:test-prop()`
`                                                                                              ⟶ B`
`                                                                                              ⟶ C`
`                                                                                              ⟶ C].`
`  (test-ind(`
`            test-aprog(x0)`` aprog[x0];`
`            test-iterate(x1)`` x2.iterate[x1;x2];`
`            test-test(x3)`` x4.test[x3;x4];`
`            test-afoo(x5)`` afoo[x5];`
`            test-bar(x6)`` x7.bar[x6;x7];`
`            test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`            test-aprop(x12)`` aprop[x12];`
`            test-false`` false;`
`            test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;x16];`
`            test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`            test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;x24])  ∈ d:test-Obj() ⟶ if test-kind(d) =a "prog"`
`                                                                                           then A`
`                                                                                         if test-kind(d) =a "foo" then B`
`                                                                                         else C`
`                                                                                         fi )`

Lemma: test-ind-test-aprog
`∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x:Top].`
`  (test-ind(`
`            test-aprog(x0)`` aprog[x0];`
`            test-iterate(x1)`` x2.iterate[x1;x2];`
`            test-test(x3)`` x4.test[x3;x4];`
`            test-afoo(x5)`` afoo[x5];`
`            test-bar(x6)`` x7.bar[x6;x7];`
`            test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`            test-aprop(x12)`` aprop[x12];`
`            test-false`` false;`
`            test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;x16];`
`            test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`            test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;x24])  `
`   test-prog-obj(test-aprog(x)) ~ aprog[x])`

Lemma: test-ind-test-iterate
`∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x:Top].`
`  (test-ind(`
`            test-aprog(x0)`` aprog[x0];`
`            test-iterate(x1)`` x2.iterate[x1;x2];`
`            test-test(x3)`` x4.test[x3;x4];`
`            test-afoo(x5)`` afoo[x5];`
`            test-bar(x6)`` x7.bar[x6;x7];`
`            test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`            test-aprop(x12)`` aprop[x12];`
`            test-false`` false;`
`            test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;x16];`
`            test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`            test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;x24])  `
`   test-prog-obj(test-iterate(x)) ~ iterate[x;test-ind(`
`                                                       test-aprog(x0)`` aprog[x0];`
`                                                       test-iterate(x1)`` x2.iterate[x1;x2];`
`                                                       test-test(x3)`` x4.test[x3;x4];`
`                                                       test-afoo(x5)`` afoo[x5];`
`                                                       test-bar(x6)`` x7.bar[x6;x7];`
`                                                       test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`                                                       test-aprop(x12)`` aprop[x12];`
`                                                       test-false`` false;`
`                                                       test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;x16];`
`                                                       test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`                                                       test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;x24])  `
`                                              test-foo-obj(x)])`

Lemma: test-ind-test-test
`∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x:Top].`
`  (test-ind(`
`            test-aprog(x0)`` aprog[x0];`
`            test-iterate(x1)`` x2.iterate[x1;x2];`
`            test-test(x3)`` x4.test[x3;x4];`
`            test-afoo(x5)`` afoo[x5];`
`            test-bar(x6)`` x7.bar[x6;x7];`
`            test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`            test-aprop(x12)`` aprop[x12];`
`            test-false`` false;`
`            test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;x16];`
`            test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`            test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;x24])  `
`   test-prog-obj(test-test(x)) ~ test[x;test-ind(`
`                                                 test-aprog(x0)`` aprog[x0];`
`                                                 test-iterate(x1)`` x2.iterate[x1;x2];`
`                                                 test-test(x3)`` x4.test[x3;x4];`
`                                                 test-afoo(x5)`` afoo[x5];`
`                                                 test-bar(x6)`` x7.bar[x6;x7];`
`                                                 test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`                                                 test-aprop(x12)`` aprop[x12];`
`                                                 test-false`` false;`
`                                                 test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;x16];`
`                                                 test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`                                                 test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;x24])  `
`                                        test-prop-obj(x)])`

Lemma: test-ind-test-afoo
`∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x:Top].`
`  (test-ind(`
`            test-aprog(x0)`` aprog[x0];`
`            test-iterate(x1)`` x2.iterate[x1;x2];`
`            test-test(x3)`` x4.test[x3;x4];`
`            test-afoo(x5)`` afoo[x5];`
`            test-bar(x6)`` x7.bar[x6;x7];`
`            test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`            test-aprop(x12)`` aprop[x12];`
`            test-false`` false;`
`            test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;x16];`
`            test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`            test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;x24])  `
`   test-foo-obj(test-afoo(x)) ~ afoo[x])`

Lemma: test-ind-test-bar
`∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x:Top].`
`  (test-ind(`
`            test-aprog(x0)`` aprog[x0];`
`            test-iterate(x1)`` x2.iterate[x1;x2];`
`            test-test(x3)`` x4.test[x3;x4];`
`            test-afoo(x5)`` afoo[x5];`
`            test-bar(x6)`` x7.bar[x6;x7];`
`            test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`            test-aprop(x12)`` aprop[x12];`
`            test-false`` false;`
`            test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;x16];`
`            test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`            test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;x24])  `
`   test-foo-obj(test-bar(x)) ~ bar[x;test-ind(`
`                                              test-aprog(x0)`` aprog[x0];`
`                                              test-iterate(x1)`` x2.iterate[x1;x2];`
`                                              test-test(x3)`` x4.test[x3;x4];`
`                                              test-afoo(x5)`` afoo[x5];`
`                                              test-bar(x6)`` x7.bar[x6;x7];`
`                                              test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`                                              test-aprop(x12)`` aprop[x12];`
`                                              test-false`` false;`
`                                              test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;x16];`
`                                              test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`                                              test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;x24])  `
`                                     test-foo-obj(x)])`

Lemma: test-ind-test-xx
`∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x,x1:Top].`
`  (test-ind(`
`            test-aprog(x0)`` aprog[x0];`
`            test-iterate(x1)`` x2.iterate[x1;x2];`
`            test-test(x3)`` x4.test[x3;x4];`
`            test-afoo(x5)`` afoo[x5];`
`            test-bar(x6)`` x7.bar[x6;x7];`
`            test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`            test-aprop(x12)`` aprop[x12];`
`            test-false`` false;`
`            test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;x16];`
`            test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`            test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;x24])  `
`   test-foo-obj(test-xx(x;x1)) ~ xx[x;x1;test-ind(`
`                                                  test-aprog(x0)`` aprog[x0];`
`                                                  test-iterate(x1)`` x2.iterate[x1;x2];`
`                                                  test-test(x3)`` x4.test[x3;x4];`
`                                                  test-afoo(x5)`` afoo[x5];`
`                                                  test-bar(x6)`` x7.bar[x6;x7];`
`                                                  test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`                                                  test-aprop(x12)`` aprop[x12];`
`                                                  test-false`` false;`
`                                                  test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;x16];`
`                                                  test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`                                                  test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;x24])  `
`                                         test-prop-obj(x);test-ind(`
`                                                                   test-aprog(x0)`` aprog[x0];`
`                                                                   test-iterate(x1)`` x2.iterate[x1;x2];`
`                                                                   test-test(x3)`` x4.test[x3;x4];`
`                                                                   test-afoo(x5)`` afoo[x5];`
`                                                                   test-bar(x6)`` x7.bar[x6;x7];`
`                                                                   test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`                                                                   test-aprop(x12)`` aprop[x12];`
`                                                                   test-false`` false;`
`                                                                   test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;`
`                                                                                                          x16];`
`                                                                   test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`                                                                   test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;`
`                                                                                                          x24])  `
`                                                          test-prog-obj(x1)])`

Lemma: test-ind-test-aprop
`∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x:Top].`
`  (test-ind(`
`            test-aprog(x0)`` aprog[x0];`
`            test-iterate(x1)`` x2.iterate[x1;x2];`
`            test-test(x3)`` x4.test[x3;x4];`
`            test-afoo(x5)`` afoo[x5];`
`            test-bar(x6)`` x7.bar[x6;x7];`
`            test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`            test-aprop(x12)`` aprop[x12];`
`            test-false`` false;`
`            test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;x16];`
`            test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`            test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;x24])  `
`   test-prop-obj(test-aprop(x)) ~ aprop[x])`

Lemma: test-ind-test-false
`∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond:Top].`
`  (test-ind(`
`            test-aprog(x0)`` aprog[x0];`
`            test-iterate(x1)`` x2.iterate[x1;x2];`
`            test-test(x3)`` x4.test[x3;x4];`
`            test-afoo(x5)`` afoo[x5];`
`            test-bar(x6)`` x7.bar[x6;x7];`
`            test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`            test-aprop(x12)`` aprop[x12];`
`            test-false`` false;`
`            test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;x16];`
`            test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`            test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;x24])  `
`   test-prop-obj(test-false()) ~ false)`

Lemma: test-ind-test-implies
`∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x,x1:Top].`
`  (test-ind(`
`            test-aprog(x0)`` aprog[x0];`
`            test-iterate(x1)`` x2.iterate[x1;x2];`
`            test-test(x3)`` x4.test[x3;x4];`
`            test-afoo(x5)`` afoo[x5];`
`            test-bar(x6)`` x7.bar[x6;x7];`
`            test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`            test-aprop(x12)`` aprop[x12];`
`            test-false`` false;`
`            test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;x16];`
`            test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`            test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;x24])  `
`   test-prop-obj(test-implies(x;x1)) `
`  ~ implies[x;x1;test-ind(`
`                          test-aprog(x0)`` aprog[x0];`
`                          test-iterate(x1)`` x2.iterate[x1;x2];`
`                          test-test(x3)`` x4.test[x3;x4];`
`                          test-afoo(x5)`` afoo[x5];`
`                          test-bar(x6)`` x7.bar[x6;x7];`
`                          test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`                          test-aprop(x12)`` aprop[x12];`
`                          test-false`` false;`
`                          test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;x16];`
`                          test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`                          test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;x24])  `
`                 test-prop-obj(x);test-ind(`
`                                           test-aprog(x0)`` aprog[x0];`
`                                           test-iterate(x1)`` x2.iterate[x1;x2];`
`                                           test-test(x3)`` x4.test[x3;x4];`
`                                           test-afoo(x5)`` afoo[x5];`
`                                           test-bar(x6)`` x7.bar[x6;x7];`
`                                           test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`                                           test-aprop(x12)`` aprop[x12];`
`                                           test-false`` false;`
`                                           test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;x16];`
`                                           test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`                                           test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;x24])  `
`                                  test-prop-obj(x1)])`

Lemma: test-ind-test-box
`∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x,x1:Top].`
`  (test-ind(`
`            test-aprog(x0)`` aprog[x0];`
`            test-iterate(x1)`` x2.iterate[x1;x2];`
`            test-test(x3)`` x4.test[x3;x4];`
`            test-afoo(x5)`` afoo[x5];`
`            test-bar(x6)`` x7.bar[x6;x7];`
`            test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`            test-aprop(x12)`` aprop[x12];`
`            test-false`` false;`
`            test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;x16];`
`            test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`            test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;x24])  `
`   test-prop-obj(test-box(x;x1)) ~ box[x;x1;test-ind(`
`                                                     test-aprog(x0)`` aprog[x0];`
`                                                     test-iterate(x1)`` x2.iterate[x1;x2];`
`                                                     test-test(x3)`` x4.test[x3;x4];`
`                                                     test-afoo(x5)`` afoo[x5];`
`                                                     test-bar(x6)`` x7.bar[x6;x7];`
`                                                     test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`                                                     test-aprop(x12)`` aprop[x12];`
`                                                     test-false`` false;`
`                                                     test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;x16];`
`                                                     test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`                                                     test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;x24])  `
`                                            test-prog-obj(x);test-ind(`
`                                                                      test-aprog(x0)`` aprog[x0];`
`                                                                      test-iterate(x1)`` x2.iterate[x1;x2];`
`                                                                      test-test(x3)`` x4.test[x3;x4];`
`                                                                      test-afoo(x5)`` afoo[x5];`
`                                                                      test-bar(x6)`` x7.bar[x6;x7];`
`                                                                      test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`                                                                      test-aprop(x12)`` aprop[x12];`
`                                                                      test-false`` false;`
`                                                                      test-implies(x13,x14)`` x15,x16.implies[x13;x14;`
`                                                                                                             x15;x16];`
`                                                                      test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`                                                                      test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;`
`                                                                                                             x23;x24])  `
`                                                             test-prop-obj(x1)])`

Lemma: test-ind-test-diamond
`∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x,x1:Top].`
`  (test-ind(`
`            test-aprog(x0)`` aprog[x0];`
`            test-iterate(x1)`` x2.iterate[x1;x2];`
`            test-test(x3)`` x4.test[x3;x4];`
`            test-afoo(x5)`` afoo[x5];`
`            test-bar(x6)`` x7.bar[x6;x7];`
`            test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`            test-aprop(x12)`` aprop[x12];`
`            test-false`` false;`
`            test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;x16];`
`            test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`            test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;x24])  `
`   test-prop-obj(test-diamond(x;x1)) `
`  ~ diamond[x;x1;test-ind(`
`                          test-aprog(x0)`` aprog[x0];`
`                          test-iterate(x1)`` x2.iterate[x1;x2];`
`                          test-test(x3)`` x4.test[x3;x4];`
`                          test-afoo(x5)`` afoo[x5];`
`                          test-bar(x6)`` x7.bar[x6;x7];`
`                          test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`                          test-aprop(x12)`` aprop[x12];`
`                          test-false`` false;`
`                          test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;x16];`
`                          test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`                          test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;x24])  `
`                 test-foo-obj(x);test-ind(`
`                                          test-aprog(x0)`` aprog[x0];`
`                                          test-iterate(x1)`` x2.iterate[x1;x2];`
`                                          test-test(x3)`` x4.test[x3;x4];`
`                                          test-afoo(x5)`` afoo[x5];`
`                                          test-bar(x6)`` x7.bar[x6;x7];`
`                                          test-xx(x8,x9)`` x10,x11.xx[x8;x9;x10;x11];`
`                                          test-aprop(x12)`` aprop[x12];`
`                                          test-false`` false;`
`                                          test-implies(x13,x14)`` x15,x16.implies[x13;x14;x15;x16];`
`                                          test-box(x17,x18)`` x19,x20.box[x17;x18;x19;x20];`
`                                          test-diamond(x21,x22)`` x23,x24.diamond[x21;x22;x23;x24])  `
`                                 test-prop-obj(x1)])`

Lemma: test-mrec-reduce
`test-ind(`
`         test-aprog(x)`` 1;`
`         test-iterate(x)`` x.2;`
`         test-test(x)`` x.3;`
`         test-afoo(x)`` 4;`
`         test-bar(x)`` x.5;`
`         test-xx(x,x)`` x,x.6;`
`         test-aprop(x)`` 7;`
`         test-false`` 99;`
`         test-implies(a,b)`` x,c.c;`
`         test-box(x,x)`` x,x.9;`
`         test-diamond(x,x)`` x,x.10)  `
`test-prop-obj(test-implies(22;33)) ~ test-ind(`
`                                              test-aprog(x)`` 1;`
`                                              test-iterate(x)`` x.2;`
`                                              test-test(x)`` x.3;`
`                                              test-afoo(x)`` 4;`
`                                              test-bar(x)`` x.5;`
`                                              test-xx(x,x)`` x,x.6;`
`                                              test-aprop(x)`` 7;`
`                                              test-false`` 99;`
`                                              test-implies(a,b)`` x,c.c;`
`                                              test-box(x,x)`` x,x.9;`
`                                              test-diamond(x,x)`` x,x.10)  `
`                                     test-prop-obj(33)`

Home Index