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