Nuprl - Pf member st app1

(6steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc

s1,s2,s:SimpleType. s st_app1(s1;s2) st_eq(s1;s2s)

By: UnivCD THEN Unfold `st` 1 THEN TreeInd 1 THEN Unfolds [`st_app1`;`arrow`] 0 THEN Reduce 0

Generated subgoals:

1 1. s1: Tree(Label+Unit)
2. s2: SimpleType
3. s: SimpleType
4. u: Tree(Label+Unit)Type{i'}
5. w: s1:{v:Tree(Label+Unit)| u(v) }s st_app1(s1;s2) st_eq(s1;s2s)
6. x: Label+Unit
s < > st_eq(tree_leaf(x);tree_node( < s2, s > ))

2 1. s1: Tree(Label+Unit)
2. s2: SimpleType
3. s: SimpleType
4. u: Tree(Label+Unit)Type{i'}
5. w: s1:{v:Tree(Label+Unit)| u(v) }s st_app1(s1;s2) st_eq(s1;s2s)
6. y1: {v:Tree(Label+Unit)| u(v) }
7. y2: {v:Tree(Label+Unit)| u(v) }
s if st_eq(y1;s2) < y2 > else < > fi st_eq(tree_node( < y1, y2 > );tree_node( < s2, s > ))

About:

(6steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc

1	1. `s1:` `Tree(Label+Unit)` 2. `s2:` `SimpleType` 3. `s:` `SimpleType` 4. `u:` `Tree(Label+Unit)Type{i'}` 5. `w:` `s1:{v:Tree(Label+Unit)\| u(v) }s st_app1(s1;s2) st_eq(s1;s2s)` 6. `x:` `Label+Unit` `s < > st_eq(tree_leaf(x);tree_node( < s2, s > ))`
2	1. `s1:` `Tree(Label+Unit)` 2. `s2:` `SimpleType` 3. `s:` `SimpleType` 4. `u:` `Tree(Label+Unit)Type{i'}` 5. `w:` `s1:{v:Tree(Label+Unit)\| u(v) }s st_app1(s1;s2) st_eq(s1;s2s)` 6. `y1:` `{v:Tree(Label+Unit)\| u(v) }` 7. `y2:` `{v:Tree(Label+Unit)\| u(v) }` `s if st_eq(y1;s2) < y2 > else < > fi st_eq(tree_node( < y1, y2 > );tree_node( < s2, s > ))`